From ceb4957fa89c978391b47d948784a1090704844a Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Fri, 30 Aug 2024 04:25:51 -0700 Subject: [PATCH] KnuckleDragger: Fix the induction principle and examples --- Data/SBV/Tools/KnuckleDragger/Induction.hs | 6 +++--- Documentation/SBV/Examples/KnuckleDragger/Induction.hs | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Data/SBV/Tools/KnuckleDragger/Induction.hs b/Data/SBV/Tools/KnuckleDragger/Induction.hs index 67c499ba6..8d3ad02a4 100644 --- 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 index 9072f415a..71c330dfb 100644 --- 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]