From aa2e2ec0afcf55567889ed0ec725c5e31e9c55d9 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Thu, 29 Aug 2024 15:26:09 -0700
Subject: [PATCH] Add KnuckleDragger induction examples

---
 CHANGES.md                                    |  4 +-
 .../SBV/Examples/KnuckleDragger/Induction.hs  | 59 +++++++++++++++++++
 sbv.cabal                                     |  1 +
 3 files changed, 62 insertions(+), 2 deletions(-)
 create mode 100644 Documentation/SBV/Examples/KnuckleDragger/Induction.hs

diff --git a/CHANGES.md b/CHANGES.md
index f47059491..8f99cf5e2 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -8,8 +8,8 @@
   * Add Data.SBV.Tools.KnuckleDragger, modeled after Philip Zucker's tool by the same
     name: https://github.com/philzook58/knuckledragger.
 
-  * Add Documentation.SBV.Examples.KnuckleDragger.Kleene, as an example of the Knuckle-dragger
-    proofs.
+  * Add Documentation.SBV.Examples.KnuckleDragger.{Kleene|Induction}, as examples
+    of some KnuckleDragger style proofs.
 
 ### Version 10.12, 2024-08-11
 
diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
new file mode 100644
index 000000000..9072f415a
--- /dev/null
+++ b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs
@@ -0,0 +1,59 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.Induction
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: erkokl@gmail.com
+-- Stability : experimental
+--
+-- Example use of the KnuckleDragger, for some inductive proofs
+--
+-----------------------------------------------------------------------------
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.Induction where
+
+import Prelude hiding (sum)
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+import Data.SBV.Tools.KnuckleDragger.Induction
+
+-- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.
+--
+-- We have:
+--
+-- >>> sumProof
+-- Axiom: sum_induction                           Admitted.
+-- Lemma: sum_correct                             Q.E.D.
+sumProof :: IO Proven
+sumProof = do
+   let sum :: SInteger -> SInteger
+       sum = smtFunction "sum" $ \n -> ite (n .== 0) 0 (n + sum (n - 1))
+
+       spec :: SInteger -> SInteger
+       spec n = (n * (n+1)) `sDiv` 2
+
+   (p, induct) <- inductionPrinciple "sum" (\n -> sum n .== spec n)
+
+   lemma "sum_correct" (\(Forall n) -> p n) [induct]
+
+-- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.
+--
+-- We have:
+--
+-- >>> sumSquareProof
+-- Axiom: sumSquare_induction                     Admitted.
+-- Lemma: sumSquare_correct                       Q.E.D.
+sumSquareProof :: IO Proven
+sumSquareProof = do
+   let sumSquare :: SInteger -> SInteger
+       sumSquare = smtFunction "sumSquare" $ \n -> ite (n .== 0) 0 (n * n + sumSquare (n - 1))
+
+       spec :: SInteger -> SInteger
+       spec n = (n * (n+1) * (2*n+1)) `sDiv` 6
+
+   (p, induct) <- inductionPrinciple "sumSquare" (\n -> sumSquare n .== spec n)
+
+   lemma "sumSquare_correct" (\(Forall n) -> p n) [induct]
diff --git a/sbv.cabal b/sbv.cabal
index f6b8f4abe..37fda807f 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -154,6 +154,7 @@ Library
                   , Documentation.SBV.Examples.Lists.BoundedMutex
                   , Documentation.SBV.Examples.Lists.CountOutAndTransfer
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
+                  , Documentation.SBV.Examples.KnuckleDragger.Induction
                   , Documentation.SBV.Examples.Misc.Definitions
                   , Documentation.SBV.Examples.Misc.Enumerate
                   , Documentation.SBV.Examples.Misc.FirstOrderLogic