KD Induction: Induct over the last element. Easier to use

LeventErkok · Oct 9, 2024 · becf846 · becf846
1 parent fe6b69e
commit becf846
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 39 deletions.
diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs
@@ -233,35 +233,35 @@ instance Induction (SInteger -> SBool) where
                      .=> qb -----------------------------------------------------
                                  (\(Forall i) -> p i)
 
--- | Induction over two argument predicates, with first argument SInteger.
-instance SymVal a => Induction (SInteger -> SBV a -> SBool) where
+-- | 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 0 a)
-                             .&& qb (\(Forall n) (Forall a) -> (n .>= 0 .&& p n a) .=> p (n+1) a)
+           principle =           qb (\(Forall a) -> p a 0)
+                             .&& qb (\(Forall a) (Forall n) -> (n .>= 0 .&& p a n) .=> p a (n+1))
                      .=> qb ----------------------------------------------------------------------
-                                 (\(Forall n) (Forall a) -> n .>= 0 .=> p n a)
+                                 (\(Forall a) (Forall n) -> n .>= 0 .=> p a n)
 
--- | Induction over three argument predicates, with first argument SInteger.
-instance (SymVal a, SymVal b) => Induction (SInteger -> SBV a -> SBV b -> SBool) where
+-- | 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 0 a b)
-                             .&& qb (\(Forall n) (Forall a) (Forall b) -> (n .>= 0 .&& p n a b) .=> p (n+1) a b)
+           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 n) (Forall a) (Forall b) -> n .>= 0 .=> p n a b)
+                                 (\(Forall a) (Forall b) (Forall n) -> n .>= 0 .=> p a b n)
 
--- | Induction over four argument predicates, with first argument SInteger.
-instance (SymVal a, SymVal b, SymVal c) => Induction (SInteger -> SBV a -> SBV b -> SBV c -> SBool) where
+-- | 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 0 a b c)
-                             .&& qb (\(Forall n) (Forall a) (Forall b) (Forall c) -> (n .>= 0 .&& p n a b c) .=> p (n+1) a b c)
+           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 n) (Forall a) (Forall b) (Forall c) -> n .>= 0 .=> p n a b c)
+                                 (\(Forall a) (Forall b) (Forall c) (Forall n) -> n .>= 0 .=> p a b c n)
 
 
 -- | Induction over lists
@@ -274,34 +274,34 @@ instance SymVal a => Induction (SList a -> SBool) where
                     .=> qb -------------------------------------------------------------
                                 (\(Forall xs) -> p xs)
 
--- | Induction over two argument predicates, with first argument a list.
-instance (SymVal a, SymVal b) => Induction (SList a -> SBV b -> SBool) where
+-- | 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 SL.nil a)
-                            .&& qb (\(Forall x) (Forall xs) (Forall a) -> p xs a .=> p (x SL..: xs) a)
-                    .=> qb ----------------------------------------------------------------------------
-                                (\(Forall xs) (Forall a) -> p xs 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 first argument a list.
-instance (SymVal a, SymVal b, SymVal c) => Induction (SList a -> SBV b -> SBV c -> SBool) where
+-- | 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 SL.nil a b)
-                            .&& qb (\(Forall x) (Forall xs) (Forall a) (Forall b) -> p xs a b .=> p (x SL..: xs) a b)
+          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 xs) (Forall a) (Forall b) -> p xs a b)
+                                (\(Forall a) (Forall b) (Forall xs) -> p a b xs)
 
--- | Induction over four argument predicates, with first argument a list.
-instance (SymVal a, SymVal b, SymVal c, SymVal d) => Induction (SList a -> SBV b -> SBV c -> SBV d -> SBool) where
+-- | 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 SL.nil a b c)
-                            .&& qb (\(Forall x) (Forall xs) (Forall a) (Forall b) (Forall c) -> p xs a b c .=> p (x SL..: xs) a b c)
+          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 xs) (Forall a) (Forall b) (Forall c) -> p xs a b c)
+                                (\(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
@@ -67,7 +67,6 @@ consApp = runKD $ lemma "consApp"
 -- [Proven] appendAssoc
 appendAssoc :: IO Proof
 appendAssoc = runKD $ do
-   -- The classic proof by induction on xs
    let p :: SymVal a => SList a -> SList a -> SList a -> SBool
        p xs ys zs = xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs
 
@@ -91,7 +90,8 @@ reverseReverse = runKD $ do
        ra xs ys = reverse (xs ++ ys) .== reverse ys ++ reverse xs
 
    revApp <- lemma "revApp" (\(Forall @"xs" (xs :: SList Elt)) (Forall @"ys" ys) -> ra xs ys)
-                   [induct (ra @Elt)]
+                   -- induction is always done on the last argument, so flip to make sure we induct on xs
+                   [induct (flip (ra @Elt))]
 
    let p :: SymVal a => SList a -> SBool
        p xs = reverse (reverse xs) .== xs

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
@@ -31,15 +31,15 @@ import Data.SBV.Tools.KnuckleDragger
 sumConstProof :: IO Proof
 sumConstProof = runKD $ do
    let sum :: SInteger -> SInteger -> SInteger
-       sum = smtFunction "sum" $ \n c -> ite (n .== 0) 0 (c + sum (n-1) c)
+       sum = smtFunction "sum" $ \c n -> ite (n .== 0) 0 (c + sum c (n-1))
 
        spec :: SInteger -> SInteger -> SInteger
-       spec n c = n * c
+       spec c n = c * n
 
        p :: SInteger -> SInteger -> SBool
-       p n c = observe "imp" (sum n c) .== observe "spec" (spec n c)
+       p c n = observe "imp" (sum c n) .== observe "spec" (spec c n)
 
-   lemma "sumConst_correct" (\(Forall @"n" n) (Forall @"c" c) -> n .>= 0 .=> p n c) [induct p]
+   lemma "sumConst_correct" (\(Forall @"c" c) (Forall @"n" n) -> n .>= 0 .=> p c n) [induct p]
 
 -- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.
 --
@@ -88,8 +88,8 @@ sumSquareProof = runKD $ do
 -- We have:
 --
 -- >>> elevenMinusFour
--- Axiom: pow0                             Axiom.
--- Axiom: powN                             Axiom.
+-- Lemma: pow0                             Q.E.D.
+-- Lemma: powN                             Q.E.D.
 -- Lemma: elevenMinusFour                  Q.E.D.
 -- [Proven] elevenMinusFour
 elevenMinusFour :: IO Proof