KnuckleDragger: Fix the induction principle and examples

LeventErkok · Aug 30, 2024 · ceb4957 · ceb4957
1 parent aa2e2ec
commit ceb4957
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Data/SBV/Tools/KnuckleDragger/Induction.hs b/Data/SBV/Tools/KnuckleDragger/Induction.hs
@@ -28,9 +28,9 @@ inductionPrinciple :: String -> (SInteger -> SBool) -> IO (SInteger -> SBool, Pr
 inductionPrinciple nm p = do
     let qb = quantifiedBool
 
-        principle =       p 0 .&& qb (\(Forall n) -> p n .=> p (n+1))
-                  .=> qb --------------------------------------------
-                                (\(Forall n) -> (p n))
+        principle =       p 0 .&& qb (\(Forall n) -> (n .>= 0 .&& p n) .=> p (n+1))
+                  .=> qb -----------------------------------------------------------
+                                    (\(Forall n) -> n .>= 0 .=> p n)
 
     induction <- axiom (nm ++ "_induction") principle
 

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
@@ -37,7 +37,7 @@ sumProof = do
 
    (p, induct) <- inductionPrinciple "sum" (\n -> sum n .== spec n)
 
-   lemma "sum_correct" (\(Forall n) -> p n) [induct]
+   lemma "sum_correct" (\(Forall n) -> n .>= 0 .=> p n) [induct]
 
 -- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.
 --
@@ -56,4 +56,4 @@ sumSquareProof = do
 
    (p, induct) <- inductionPrinciple "sumSquare" (\n -> sumSquare n .== spec n)
 
-   lemma "sumSquare_correct" (\(Forall n) -> p n) [induct]
+   lemma "sumSquare_correct" (\(Forall n) -> n .>= 0 .=> p n) [induct]