From d9d847e887ba42121219a574e201edc62e30e278 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Fri, 6 Dec 2024 18:13:29 -0800
Subject: [PATCH] Simplifying induction. WIP

---
 Data/SBV/Tools/KDKernel.hs                    | 61 -------------------
 .../SBV/Examples/KnuckleDragger/AppendRev.hs  |  8 +--
 .../KnuckleDragger/EquationalReasoning.hs     |  7 +--
 .../SBV/Examples/KnuckleDragger/Induction.hs  |  6 +-
 .../SBV/Examples/KnuckleDragger/Lists.hs      | 52 +++++++---------
 .../SBV/Examples/KnuckleDragger/RevLen.hs     |  8 +--
 6 files changed, 33 insertions(+), 109 deletions(-)

diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs
index 383698338..6849b5eb5 100644
--- a/Data/SBV/Tools/KDKernel.hs
+++ b/Data/SBV/Tools/KDKernel.hs
@@ -233,37 +233,6 @@ instance Induction (SInteger -> SBool) where
                      .=> qb -----------------------------------------------------
                                  (\(Forall i) -> p i)
 
--- | Induction over two argument predicates, with the last argument SInteger.
-instance SymVal a => Induction (SBV a -> SInteger -> SBool) where
-  induct p = internalAxiom "Nat.induct2" principle
-     where qb a = quantifiedBool a
-
-           principle =           qb (\(Forall a) -> p a 0)
-                             .&& qb (\(Forall a) (Forall n) -> (n .>= 0 .&& p a n) .=> p a (n+1))
-                     .=> qb ----------------------------------------------------------------------
-                                 (\(Forall a) (Forall n) -> n .>= 0 .=> p a n)
-
--- | Induction over three argument predicates, with last argument SInteger.
-instance (SymVal a, SymVal b) => Induction (SBV a -> SBV b -> SInteger -> SBool) where
-  induct p = internalAxiom "Nat.induct3" principle
-     where qb a = quantifiedBool a
-
-           principle =           qb (\(Forall a) (Forall b) -> p a b 0)
-                             .&& qb (\(Forall a) (Forall b) (Forall n) -> (n .>= 0 .&& p a b n) .=> p a b (n+1))
-                     .=> qb -------------------------------------------------------------------------------------
-                                 (\(Forall a) (Forall b) (Forall n) -> n .>= 0 .=> p a b n)
-
--- | Induction over four argument predicates, with last argument SInteger.
-instance (SymVal a, SymVal b, SymVal c) => Induction (SBV a -> SBV b -> SBV c -> SInteger -> SBool) where
-  induct p = internalAxiom "Nat.induct4" principle
-     where qb a = quantifiedBool a
-
-           principle =           qb (\(Forall a) (Forall b) (Forall c) -> p a b c 0)
-                             .&& qb (\(Forall a) (Forall b) (Forall c) (Forall n) -> (n .>= 0 .&& p a b c n) .=> p a b c (n+1))
-                     .=> qb ----------------------------------------------------------------------------------------------------
-                                 (\(Forall a) (Forall b) (Forall c) (Forall n) -> n .>= 0 .=> p a b c n)
-
-
 -- | Induction over lists
 instance SymVal a => Induction (SList a -> SBool) where
   induct p = internalAxiom "List(a).induct" principle
@@ -274,34 +243,4 @@ instance SymVal a => Induction (SList a -> SBool) where
                     .=> qb -------------------------------------------------------------
                                 (\(Forall xs) -> p xs)
 
--- | Induction over two argument predicates, with last argument a list.
-instance (SymVal a, SymVal e) => Induction (SBV a -> SList e -> SBool) where
-  induct p = internalAxiom "List(a).induct2" principle
-    where qb a = quantifiedBool a
-
-          principle =           qb (\(Forall a) -> p a SL.nil)
-                            .&& qb (\(Forall a) (Forall e) (Forall es) -> p a es .=> p a (e SL..: es))
-                    .=> qb ------------------------------------------------------------------------------
-                                (\(Forall a) (Forall es) -> p a es)
-
--- | Induction over three argument predicates, with last argument a list.
-instance (SymVal a, SymVal b, SymVal e) => Induction (SBV a -> SBV b -> SList e -> SBool) where
-  induct p = internalAxiom "List(a).induct3" principle
-    where qb a = quantifiedBool a
-
-          principle =           qb (\(Forall a) (Forall b) -> p a b SL.nil)
-                            .&& qb (\(Forall a) (Forall b) (Forall e) (Forall es) -> p a b es .=> p a b (e SL..: es))
-                    .=> qb -------------------------------------------------------------------------------------------
-                                (\(Forall a) (Forall b) (Forall xs) -> p a b xs)
-
--- | Induction over four argument predicates, with last argument a list.
-instance (SymVal a, SymVal b, SymVal c, SymVal e) => Induction (SBV a -> SBV b -> SBV c -> SList e -> SBool) where
-  induct p = internalAxiom "List(a).induct4" principle
-    where qb a = quantifiedBool a
-
-          principle =           qb (\(Forall a) (Forall b) (Forall c) -> p a b c SL.nil)
-                            .&& qb (\(Forall a) (Forall b) (Forall c) (Forall e) (Forall es) -> p a b c es .=> p a b c (e SL..: es))
-                    .=> qb ----------------------------------------------------------------------------------------------------------
-                                (\(Forall a) (Forall b) (Forall c) (Forall xs) -> p a b c xs)
-
 {- HLint ignore module "Eta reduce" -}
diff --git a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
index d4b210e2d..ab6c1ef9b 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
@@ -86,12 +86,10 @@ reverseReverse :: IO Proof
 reverseReverse = runKD $ do
 
    -- Helper lemma: @reverse (xs ++ ys) .== reverse ys ++ reverse xs@
-   let ra :: SymVal a => SList a -> SList a -> SBool
-       ra xs ys = reverse (xs ++ ys) .== reverse ys ++ reverse xs
+   let ra :: SymVal a => SList a -> SBool
+       ra xs = quantifiedBool $ \(Forall @"ys" ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs
 
-   revApp <- lemma "revApp" (\(Forall @"xs" (xs :: SList Elt)) (Forall @"ys" ys) -> ra xs ys)
-                   -- induction is always done on the last argument, so flip to make sure we induct on xs
-                   [induct (flip (ra @Elt))]
+   revApp <- lemma "revApp" (\(Forall @"xs" (xs :: SList Elt)) -> ra xs) [induct (ra @Elt)]
 
    let p :: SymVal a => SList a -> SBool
        p xs = reverse (reverse xs) .== xs
diff --git a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
index 0a5ff4d37..57300d87e 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/EquationalReasoning.hs
@@ -126,12 +126,9 @@ foldrOverAppend = runKD $ do
        f :: SA -> SA -> SA
        f = uninterpret "f"
 
-       p xs ys = foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs
+       p xs = quantifiedBool $ \(Forall @"ys" ys) -> foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs
 
-   lemma "foldrOverAppend"
-          (\(Forall @"xs" xs) (Forall @"ys" ys) -> p xs ys)
-          -- Induction is done on the last element. Here we want to induct on xs, hence the flip below.
-          [induct (flip p)]
+   lemma "foldrOverAppend" (\(Forall @"xs" xs) -> p xs) [induct p]
 
 {- Can't converge
 -- * Foldl over append
diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
index 0751d34a7..779ad7a09 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
@@ -36,10 +36,10 @@ sumConstProof = runKD $ do
        spec :: SInteger -> SInteger -> SInteger
        spec c n = c * n
 
-       p :: SInteger -> SInteger -> SBool
-       p c n = observe "imp" (sum c n) .== observe "spec" (spec c n)
+       p :: SInteger -> SBool
+       p n = quantifiedBool $ \(Forall @"c" c) -> observe "imp" (sum c n) .== observe "spec" (spec c n)
 
-   lemma "sumConst_correct" (\(Forall @"c" c) (Forall @"n" n) -> n .>= 0 .=> p c n) [induct p]
+   lemma "sumConst_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct p]
 
 -- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.
 --
diff --git a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
index c6554647f..dd029625c 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
@@ -32,7 +32,6 @@ import Prelude hiding(reverse, (++), any, all, notElem, filter, map)
 -- >>> -- For doctest purposes only:
 -- >>> :set -XScopedTypeVariables
 -- >>> import Control.Exception
--- >>> import Data.SBV.Tools.KnuckleDragger
 #endif
 
 -- | A list of booleans is not all true, if any of them is false. We have:
@@ -81,11 +80,11 @@ mkUninterpretedSort ''B
 
 -- | @reverse (x:xs) == reverse xs ++ [x]@
 --
--- >>> runKD revCons
+-- >>> revCons
 -- Lemma: revCons                          Q.E.D.
 -- [Proven] revCons
-revCons :: KD Proof
-revCons = do
+revCons :: IO Proof
+revCons = runKD $ do
     let p :: SA -> SList A -> SBool
         p x xs = reverse (x .: xs) .== reverse xs ++ singleton x
 
@@ -93,26 +92,19 @@ revCons = do
 
 -- | @map f (xs ++ ys) == map f xs ++ map f ys@
 --
--- >>> runKD mapAppend
+-- >>> mapAppend (uninterpret "f")
 -- Lemma: mapAppend                        Q.E.D.
 -- [Proven] mapAppend
-mapAppend :: KD Proof
-mapAppend = do
-   let p :: (SA -> SB) -> SList A -> SList A -> SBool
-       p g xs ys = map g (xs ++ ys) .== map g xs ++ map g ys
+mapAppend :: (SA -> SB) -> IO Proof
+mapAppend f = runKD $ do
+   let p :: SList A -> SBool
+       p xs = quantifiedBool $ \(Forall @"ys" ys) -> map f (xs ++ ys) .== map f xs ++ map f ys
 
-       -- For an arbitrary uninterpreted function 'f':
-       f :: SA -> SB
-       f = uninterpret "f"
-
-   lemma "mapAppend"
-         (\(Forall @"xs" xs) (Forall @"ys" ys) -> p f xs ys)
-         -- induction is done on the last argument, so flip to do it on xs
-         [induct (flip (p f))]
+   lemma "mapAppend" (\(Forall @"xs" xs) -> p xs) [induct p]
 
 -- | @map f . reverse == reverse . map f@
 --
--- >>> runKD mapReverse
+-- >>> mapReverse
 -- Lemma: revCons                          Q.E.D.
 -- Lemma: mapAppend                        Q.E.D.
 -- Chain: mapReverse
@@ -124,20 +116,22 @@ mapAppend = do
 --   Lemma: mapReverse.6                   Q.E.D.
 -- Lemma: mapReverse                       Q.E.D.
 -- [Proven] mapReverse
-mapReverse :: KD Proof
-mapReverse = do
-     let p :: (SA -> SB) -> SList A -> SBool
-         p g xs = reverse (map g xs) .== map g (reverse xs)
-
-         -- For an arbitrary uninterpreted function 'f':
-         f :: SA -> SB
+mapReverse :: IO Proof
+mapReverse = runKD $ do
+     let f :: SA -> SB
          f = uninterpret "f"
 
-     rCons <- revCons
-     mApp  <- mapAppend
+the problem here is that the mapAppend now has a nested quantifier, which messes things up..
+hmm.
+
+         p :: SList A -> SBool
+         p xs = reverse (map f xs) .== map f (reverse xs)
+
+     rCons <- use revCons
+     mApp  <- use (mapAppend f)
 
      chainLemma "mapReverse"
-                (\(Forall @"xs" xs) -> p f xs)
+                (\(Forall @"xs" xs) -> p xs)
                 (\x xs -> [ reverse (map f (x .: xs))
                           , reverse (f x .: map f xs)
                           , reverse (map f xs) ++ singleton (f x)
@@ -146,4 +140,4 @@ mapReverse = do
                           , map f (reverse xs ++ singleton x)
                           , map f (reverse (x .: xs))
                           ])
-                [induct (p f), rCons, mApp]
+                [induct p, rCons, mApp]
diff --git a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
index c4b494487..810d59834 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
@@ -51,9 +51,7 @@ revLen = runKD $ do
    let p :: SList Elt -> SBool
        p xs = length (reverse xs) .== length xs
 
-   lemma "revLen"
-         (\(Forall @"xs" xs) -> p xs)
-         [induct p]
+   lemma "revLen" (\(Forall @"xs" xs) -> p xs) [induct p]
 
 -- | An example where we attempt to prove a non-theorem. Notice the counter-example
 -- generated for:
@@ -72,8 +70,6 @@ badRevLen = runKD $ do
    let p :: SList Elt -> SBool
        p xs = length (reverse xs) .== ite (length xs .== 3) 5 (length xs)
 
-   lemma "badRevLen"
-         (\(Forall @"xs" xs) -> p xs)
-         [induct p]
+   lemma "badRevLen" (\(Forall @"xs" xs) -> p xs) [induct p]
 
    pure ()