content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Documentation.SBV.Examples.TP.Peano
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Modeling Peano arithmetic in SBV and proving various properties using TP.
  -- Most of the properties we prove come from <https://en.wikipedia.org/wiki/Peano_axioms>.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE CPP                 #-}
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE FlexibleInstances   #-}
  {-# LANGUAGE QuasiQuotes         #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell     #-}
  {-# LANGUAGE TypeAbstractions    #-}
  {-# LANGUAGE TypeApplications    #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Documentation.SBV.Examples.TP.Peano where
  
  import Data.SBV
  import Data.SBV.TP
  
  #ifdef DOCTEST
  -- $setup
  -- >>> import Data.SBV
  -- >>> import Data.SBV.TP
  #endif
  
  -- | Natural numbers. (If you are looking at the haddock documents, note the plethora of definitions
  -- the call to 'mkSymbolic' generates. You can mostly ignore these, except for the case analyzer,
  -- the testers and accessors.)
  data Nat = Zero
           | Succ { prev :: Nat }
  
  -- | Create a symbolic version of naturals.
  mkSymbolic [''Nat]
  
  -- | Numeric instance. Choices: We clamp everything at 'Zero'. Negation is identity.
  instance Num Nat where
    fromInteger i | i <= 0 = Zero
                  | True   = Succ (fromInteger (i - 1))
  
    a + Zero   = a
    a + Succ b = Succ (a + b)
  
    (-) = error "Nat: No support for subtraction"
  
    _ * Zero   = Zero
    a * Succ b = a + a * b
  
    abs = id
  
    signum Zero = 0
    signum _    = 1
  
    negate = id
  
  -- Symbolic numeric instance, mirroring the above
  instance Num SNat where
    fromInteger = literal . fromInteger
  
    (+) = plus
        where plus = smtFunction "sNatPlus" $
                       \m n -> [sCase|Nat m of
                                 Zero   -> n
                                 Succ p -> sSucc (p + n)
                               |]
  
    (-) = error "SNat: No support for subtraction"
  
    (*) = times
        where times = smtFunction "sNatTimes" $
                        \m n -> [sCase|Nat m of
                                  Zero   -> 0
                                  Succ p -> n + p * n
                                |]
  
    abs = id
  
    signum m = [sCase|Nat m of
                 Zero -> 0
                 _    -> 1
               |]
  
  -- | Symbolic ordering. We only define less-than, other methods use the defaults.
  instance OrdSymbolic SNat where
     m .< n = quantifiedBool (\(Exists k) -> n .== m + sSucc k)
  
  -- * Conversion to and from integers
  
  -- | Convert from 'Nat' to 'Integer'.
  --
  -- NB. When writing the properties below, we use the notation \(\overline{n}\) to mean @n2i n@.
  n2i :: SNat -> SInteger
  n2i = smtFunction "n2i" $ \n -> [sCase|Nat n of
                                     Zero   -> 0
                                     Succ p -> 1 + n2i p
                                  |]
  
  -- | Convert Non-negative integers to 'Nat'. Negative numbers become 'Zero'.
  --
  -- NB. When writing the properties below, we use the notation \(\underline{i}\) to mean @i2n i@.
  i2n :: SInteger -> SNat
  i2n = smtFunction "i2n" $ \i -> ite (i .<= 0) 0 (sSucc (i2n (i - 1)))
  
  -- | \(\overline{n} \geq 0\)
  --
  -- >>> runTP n2iNonNeg
  -- Lemma: n2iNonNeg                        Q.E.D.
  -- [Proven] n2iNonNeg :: Ɐn ∷ Nat → Bool
  n2iNonNeg  :: TP (Proof (Forall "n" Nat -> SBool))
  n2iNonNeg = inductiveLemma "n2iNonNeg" (\(Forall n) -> n2i n .>= 0) []
  
  -- | \(\overline{\underline{i}} = \max(i, 0)\).
  --
  -- >>> runTP i2n2i
  -- Lemma: i2n2i                            Q.E.D.
  -- [Proven] i2n2i :: Ɐi ∷ Integer → Bool
  i2n2i :: TP (Proof (Forall "i" Integer -> SBool))
  i2n2i = inductiveLemma "i2n2i" (\(Forall i) -> n2i (i2n i) .== i `smax` 0) []
  
  -- | \(\underline{\overline{n}} = n\)
  --
  -- >>> runTP n2i2n
  -- Lemma: n2i2n                            Q.E.D.
  -- [Proven] n2i2n :: Ɐn ∷ Nat → Bool
  n2i2n :: TP (Proof (Forall "n" Nat -> SBool))
  n2i2n = inductiveLemma "n2i2n" (\(Forall n) -> i2n (n2i n) .== n) []
  
  -- | \(\overline{m + n} = \overline{m} + \overline{n}\)
  --
  -- >>> runTP n2iAdd
  -- Lemma: n2iAdd                           Q.E.D.
  -- [Proven] n2iAdd :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  n2iAdd :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  n2iAdd = inductiveLemma "n2iAdd" (\(Forall m) (Forall n) -> n2i (m + n) .== n2i m + n2i n) []
  
  -- * Addition
  
  -- ** Correctness
  
  -- | \(\overline{m + n} = \overline{m} + \overline{n}\)
  --
  -- >>> runTP addCorrect
  -- Lemma: addCorrect                       Q.E.D.
  -- [Proven] addCorrect :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  addCorrect :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  addCorrect = inductiveLemma
                 "addCorrect"
                 (\(Forall m) (Forall n) -> n2i (m + n) .== n2i m + n2i n)
                 []
  
  -- ** Left and right unit
  
  -- | \(0 + m = m\)
  --
  -- >>> runTP addLeftUnit
  -- Lemma: addLeftUnit                      Q.E.D.
  -- [Proven] addLeftUnit :: Ɐm ∷ Nat → Bool
  addLeftUnit :: TP (Proof (Forall "m" Nat -> SBool))
  addLeftUnit = lemma "addLeftUnit" (\(Forall m) -> 0 + m .== m) []
  
  -- | \(m + 0 = m\)
  --
  -- >>> runTP addRightUnit
  -- Lemma: addRightUnit                     Q.E.D.
  -- [Proven] addRightUnit :: Ɐm ∷ Nat → Bool
  addRightUnit :: TP (Proof (Forall "m" Nat -> SBool))
  addRightUnit = inductiveLemma "addRightUnit" (\(Forall m) -> m + 0 .== m) []
  
  -- ** Addition with non-zero values
  
  -- | \(m + \mathrm{Succ}\,n = \mathrm{Succ}\,(m + n)\)
  --
  -- >>> runTP addSucc
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: addSucc                          Q.E.D.
  -- [Proven] addSucc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  addSucc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  addSucc = do
     caseZero <- lemma "caseZero"
                        (\(Forall @"n" n) -> 0 + sSucc n .== sSucc (0 + n))
                        []
  
     caseSucc <- calc "caseSucc"
                      (\(Forall @"m" m) (Forall @"n" n) ->
                          m + sSucc n .== sSucc (m + n) .=> sSucc m + sSucc n .== sSucc (sSucc m + n)) $
                      \m n -> let ih = m + sSucc n .== sSucc (m + n)
                           in [ih] |- sSucc m + sSucc n
                                   =: sSucc (m + sSucc n)
                                   ?? ih
                                   =: sSucc (sSucc (m + n))
                                   =: sSucc (sSucc m + n)
                                   =: qed
  
     inductiveLemma
        "addSucc"
        (\(Forall @"m" m) (Forall @"n" n) -> m + sSucc n .== sSucc (m + n))
        [proofOf caseZero, proofOf caseSucc]
  
  -- ** Associativity
  
  -- | \(m + (n + o) = (m + n) + o\)
  --
  -- >>> runTP addAssoc
  -- Lemma: addAssoc                         Q.E.D.
  -- [Proven] addAssoc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  addAssoc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  addAssoc = inductiveLemma
               "addAssoc"
               (\(Forall m) (Forall n) (Forall o) -> m + (n + o) .== (m + n) + o)
               []
  
  -- ** Commutativity
  
  -- | \(m + n = n + m\)
  --
  -- >>> runTP addComm
  -- Lemma: addLeftUnit                      Q.E.D.
  -- Lemma: addRightUnit                     Q.E.D.
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: addSucc                          Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: addComm                          Q.E.D.
  -- [Proven] addComm :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  addComm :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  addComm = do
      alu <- recall "addLeftUnit"  addLeftUnit
      aru <- recall "addRightUnit" addRightUnit
  
      caseZero <- lemma "caseZero"
                        (\(Forall @"n" (n :: SNat)) -> 0 + n .== n + 0)
                        [proofOf alu, proofOf aru]
  
      as <- recall "addSucc" addSucc
  
      caseSucc <- calc "caseSucc"
                       (\(Forall @"m" m) (Forall @"n" n) -> m + n .== n + m .=> sSucc m + n .== n + sSucc m) $
                       \m n -> let ih = m + n .== n + m
                            in [ih] |- sSucc m + n
                                    =: sSucc (m + n)
                                    ?? ih
                                    =: sSucc (n + m)
                                    ?? as `at` (Inst @"m" n, Inst @"n" m)
                                    =: n + sSucc m
                                    =: qed
  
      inductiveLemma "addComm"
                     (\(Forall m) (Forall n) -> m + n .== n + m)
                     [proofOf caseZero, proofOf caseSucc]
  
  -- * Multiplication
  
  -- ** Correctness
  
  -- | \(\overline{m * n} = \overline{m} * \overline{n}\)
  --
  -- >>> runTP mulCorrect
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: addCorrect                       Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: mullCorrect                      Q.E.D.
  -- [Proven] mullCorrect :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  mulCorrect :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  mulCorrect = do
     caseZero <- lemma "caseZero"
                       (\(Forall @"n" n) -> n2i (0 * n) .== n2i 0 * n2i n)
                       []
  
     addC <- recall "addCorrect" addCorrect
  
     caseSucc <- calc "caseSucc"
                      (\(Forall @"m" m) (Forall @"n" n) ->
                            n2i (m * n) .== n2i m * n2i n .=> n2i (sSucc m * n) .== n2i (sSucc m) * n2i n) $
                      \m n -> let ih = n2i (m * n) .== n2i m * n2i n
                           in [ih] |- n2i (sSucc m * n)
                                   =: n2i (n + m * n)
                                   ?? addC `at` (Inst @"m" n, Inst @"n" (m * n))
                                   =: n2i n + n2i (m * n)
                                   ?? ih
                                   =: n2i n + n2i m * n2i n
                                   =: n2i n * (1 + n2i m)
                                   =: n2i n * n2i (sSucc m)
                                   =: qed
  
     inductiveLemma
         "mullCorrect"
         (\(Forall @"m" m) (Forall @"n" n) -> n2i (m * n) .== n2i m * n2i n)
         [proofOf caseZero, proofOf caseSucc]
  
  -- ** Left and right absorption
  
  -- | \(0 * m = 0\)
  --
  -- >>> runTP mulLeftAbsorb
  -- Lemma: mulLeftAbsorb                    Q.E.D.
  -- [Proven] mulLeftAbsorb :: Ɐm ∷ Nat → Bool
  mulLeftAbsorb :: TP (Proof (Forall "m" Nat -> SBool))
  mulLeftAbsorb = lemma "mulLeftAbsorb" (\(Forall m) -> 0 * m .== 0) []
  
  -- | \(m * 0 = 0\)
  --
  -- >>> runTP mulRightAbsorb
  -- Lemma: mulRightAbsorb                   Q.E.D.
  -- [Proven] mulRightAbsorb :: Ɐm ∷ Nat → Bool
  mulRightAbsorb :: TP (Proof (Forall "m" Nat -> SBool))
  mulRightAbsorb = inductiveLemma "mulRightAbsorb" (\(Forall m) -> m * 0 .== 0) []
  
  -- ** Left and right unit
  
  -- | \(\mathrm{Succ\,0} * m = m\)
  --
  -- >>> runTP mulLeftUnit
  -- Lemma: mulLeftUnit                      Q.E.D.
  -- [Proven] mulLeftUnit :: Ɐm ∷ Nat → Bool
  mulLeftUnit :: TP (Proof (Forall "m" Nat -> SBool))
  mulLeftUnit = inductiveLemma "mulLeftUnit" (\(Forall m) -> sSucc 0 * m .== m) []
  
  -- | \(m * \mathrm{Succ\,0} = m\)
  --
  -- >>> runTP mulRightUnit
  -- Lemma: mulRightUnit                     Q.E.D.
  -- [Proven] mulRightUnit :: Ɐm ∷ Nat → Bool
  mulRightUnit :: TP (Proof (Forall "m" Nat -> SBool))
  mulRightUnit = inductiveLemma "mulRightUnit" (\(Forall m) -> m * sSucc 0 .== m) []
  
  -- ** Distribution over addition
  
  -- | \(m * (n + o) = m * n + m * o\)
  --
  -- >>> runTP distribLeft
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: addAssoc                         Q.E.D.
  -- Lemma: addComm                          Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Step: 7                               Q.E.D.
  --   Step: 8                               Q.E.D.
  --   Step: 9                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: distribLeft                      Q.E.D.
  -- [Proven] distribLeft :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  distribLeft :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  distribLeft = do
     caseZero <- lemma "caseZero" (\(Forall @"n" n) (Forall @"o" (o :: SNat)) -> 0 * (n + o) .== 0 * n + 0 * o) []
  
     addAsc <- recall "addAssoc" addAssoc
     addCom <- recall "addComm"  addComm
  
     caseSucc <- calc "caseSucc"
                      (\(Forall @"m" m) (Forall @"n" n) (Forall @"o" o) ->
                          m * (n + o) .== m * n + m * o .=> sSucc m * (n + o) .== sSucc m * n + sSucc m * o) $
                 \m n o -> let ih = m * (n + o) .== m * n + m * o
                        in [ih] |- sSucc m * (n + o)
                                =: (n + o) + m * (n + o)
                                ?? ih
                                =: (n + o) + (m * n + m * o)
                                ?? addAsc `at` (Inst @"m" n, Inst @"n" o, Inst @"o" (m * n + m * o))
                                =: n + (o + (m * n + m * o))
                                ?? addCom `at` (Inst @"m" (m * n), Inst @"n" (m * o))
                                =: n + (o + (m * o + m * n))
                                ?? addAsc `at` (Inst @"m" o, Inst @"n" (m * o), Inst @"o" (m * n))
                                =: n + ((o + m * o) + m * n)
                                =: n + (sSucc m * o + m * n)
                                ?? addCom `at` (Inst @"m" (sSucc m * o), Inst @"n" (m * n))
                                =: n + (m * n + sSucc m * o)
                                ?? addAsc `at` (Inst @"m" n, Inst @"n" (m * n), Inst @"o" (sSucc m * o))
                                =: (n + m * n) + sSucc m * o
                                =: sSucc m * n + sSucc m * o
                                =: qed
  
     inductiveLemma
       "distribLeft"
       (\(Forall m) (Forall n) (Forall o) -> m * (n + o) .== m * n + m * o)
       [proofOf caseZero, proofOf caseSucc]
  
  -- | \((m + n) * o = m * o + n * o\)
  --
  -- >>> runTP distribRight
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: addAssoc                         Q.E.D.
  -- Lemma: addComm                          Q.E.D.
  -- Lemma: addSucc                          Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Step: 7                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: distribRight                     Q.E.D.
  -- [Proven] distribRight :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  distribRight :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  distribRight = do
     caseZero <- lemma "caseZero" (\(Forall @"n" n) (Forall @"o" (o :: SNat)) -> (0 + n) * o .== 0 * o + n * o) []
  
     pAddAssoc <- recall "addAssoc" addAssoc
     pAddCom   <- recall "addComm"  addComm
     pAddSucc  <- recall "addSucc"  addSucc
  
     caseSucc <- calc "caseSucc"
                      (\(Forall @"m" m) (Forall @"n" n) (Forall @"o" o) ->
                          (m + n) * o .== m * o + n * o .=> (sSucc m + n) * o .== sSucc m * o + n * o) $
                 \m n o -> let ih = (m + n) * o .== m * o + n * o
                        in [ih] |- (sSucc m + n) * o
                                ?? pAddCom `at` (Inst @"m" (sSucc m), Inst @"n" n)
                                =: (n + sSucc m) * o
                                ?? pAddSucc `at` (Inst @"m" n, Inst @"n" m)
                                =: sSucc (n + m) * o
                                ?? pAddCom `at` (Inst @"m" n, Inst @"n" m)
                                =: sSucc (m + n) * o
                                =: o + (m + n) * o
                                ?? ih
                                =: o + (m * o + n *o)
                                ?? pAddAssoc `at` (Inst @"m" o, Inst @"n" (m * o), Inst @"o" (n * o))
                                =: (o + m * o) + n * o
                                =: sSucc m * o + n * o
                                =: qed
  
     inductiveLemma
       "distribRight"
       (\(Forall m) (Forall n) (Forall o) -> (m + n) * o .== m * o + n * o)
       [proofOf caseZero, proofOf caseSucc]
  
  -- ** Multiplication with non-zero values
  
  -- | \(m * \mathrm{Succ}\,n = m * n + m\)
  --
  -- >>> runTP mulSucc
  -- Lemma: addLeftUnit                      Q.E.D.
  -- Lemma: distribLeft                      Q.E.D.
  -- Lemma: mulRightUnit                     Q.E.D.
  -- Lemma: addComm                          Q.E.D.
  -- Lemma: mulSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2 (defn of +)                   Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] mulSucc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  mulSucc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  mulSucc = do
     alu <- recall "addLeftUnit"    addLeftUnit
     dL  <- recall "distribLeft"    distribLeft
     mru <- recall "mulRightUnit"   mulRightUnit
     ac  <- recall "addComm"        addComm
  
     calc "mulSucc"
          (\(Forall @"m" m) (Forall @"n" n) -> m * sSucc n .== m * n + m) $
          \m n -> [] |- m * sSucc n
                     ?? alu
                     =: m * sSucc (0 + n)
                     ?? "defn of +"
                     =: m * (sSucc 0 + n)
                     ?? dL `at` (Inst @"m" m, Inst @"n" (sSucc 0), Inst @"o" n)
                     =: m * sSucc 0 + m * n
                     ?? mru
                     =: m + m * n
                     ?? ac `at` (Inst @"m" m, Inst @"n" (m * n))
                     =: m * n + m
                     =: qed
  
  -- ** Associativity
  
  -- | \(m * (n * o) = (m * n) * o\)
  --
  -- >>> runTP mulAssoc
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: distribRight                     Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: mulAssoc                         Q.E.D.
  -- [Proven] mulAssoc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  mulAssoc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  mulAssoc = do
     caseZero <- lemma "caseZero"
                       (\(Forall @"n" n) (Forall @"o" (o :: SNat)) -> 0 * (n * o) .== (0 * n) * o)
                       []
  
     distR <- recall "distribRight" distribRight
  
     caseSucc <- calc "caseSucc"
                      (\(Forall @"m" m) (Forall @"n" n) (Forall @"o" o) ->
                         m * (n * o) .== (m * n) * o .=> sSucc m * (n * o) .== (sSucc m * n) * o) $
                      \m n o -> let ih = m * (n * o) .== (m * n) * o
                                in [ih] |- sSucc m * (n * o)
                                        =: (n * o) + m * (n * o)
                                        ?? ih
                                        =: (n * o) + (m * n) * o
                                        ?? distR `at` (Inst @"m" n, Inst @"n" (m * n), Inst @"o" o)
                                        =: (n + m * n) * o
                                        =: (sSucc m * n) * o
                                        =: qed
  
     inductiveLemma
       "mulAssoc"
       (\(Forall m) (Forall n) (Forall o) -> m * (n * o) .== (m * n) * o)
       [proofOf caseZero, proofOf caseSucc]
  
  -- ** Commutativity
  
  -- | \(m * n = n * m\)
  --
  -- >>> runTP mulComm
  -- Lemma: mulRightAbsorb                   Q.E.D.
  -- Lemma: caseZero                         Q.E.D.
  -- Lemma: mulRightUnit                     Q.E.D.
  -- Lemma: distribLeft                      Q.E.D.
  -- Lemma: caseSucc
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: mulComm                          Q.E.D.
  -- [Proven] mulComm :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  mulComm :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  mulComm = do
    mra <- recall "mulRightAbsorb" mulRightAbsorb
  
    caseZero <- lemma "caseZero"
                      (\(Forall @"m" (m :: SNat)) -> 0 * m .== m * 0)
                      [proofOf mra]
  
    mru <- recall "mulRightUnit" mulRightUnit
    dL  <- recall "distribLeft"  distribLeft
  
    caseSucc <- calc "caseSucc"
                     (\(Forall @"m" m) (Forall @"n" n) -> m * n .== n * m .=> sSucc m * n .== n * sSucc m) $
                     \m n -> let ih = m * n .== n * m
                          in [ih] |- sSucc m * n
                                  =: n + m * n
                                  ?? ih
                                  =: n + n * m
                                  ?? mru
                                  =: n * sSucc 0 + n * m
                                  ?? dL `at` (Inst @"m" n, Inst @"n" (sSucc 0), Inst @"o" m)
                                  =: n * (sSucc 0 + m)
                                  =: n * sSucc (0 + m)
                                  =: n * sSucc m
                                  =: qed
  
    inductiveLemma
      "mulComm"
      (\(Forall @"m" m) (Forall @"n" n) -> m * n .== n * m)
      [proofOf caseZero, proofOf caseSucc]
  
  -- * Ordering
  
  -- ** Transitivity of @<@
  
  -- | \(m < n \;\wedge\; n < o \;\rightarrow\; m < o\)
  --
  -- >>> runTP ltTrans
  -- Lemma: addAssoc                         Q.E.D.
  -- Lemma: ltTrans
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] ltTrans :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  ltTrans :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  ltTrans = do
    aa <- recall "addAssoc" addAssoc
  
    calc "ltTrans"
         (\(Forall @"m" m) (Forall @"n" n) (Forall @"o" o) -> m .< n .&& n .< o .=> m .< o) $
         \m n o ->  [m .< n, n .< o]
                |-> let k1 = some "k1" (\k -> n .== m + sSucc k)
                        k2 = some "k2" (\k -> o .== n + sSucc k)
                 in n .== m + sSucc k1
                 =: o .== n + sSucc k2
                 =: o .== (m + sSucc k1) + sSucc k2
                 ?? aa `at` (Inst @"m" m, Inst @"n" (sSucc k1), Inst @"o" (sSucc k2))
                 =: o .== m + (sSucc k1 + sSucc k2)
                 =: o .== m + sSucc (k1 + sSucc k2)
                 =: m .< o
                 =: sTrue
                 =: qed
  
  -- ** Irreflexivity of @<@
  
  -- | \(\neg(m < m)\)
  --
  -- >>> runTP ltIrreflexive
  -- Lemma: cancel                           Q.E.D.
  -- Lemma: ltIrreflexive
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] ltIrreflexive :: Ɐm ∷ Nat → Bool
  ltIrreflexive :: TP (Proof (Forall "m" Nat -> SBool))
  ltIrreflexive = do
    cancel <- inductiveLemma
                "cancel"
                (\(Forall @"m" m) (Forall @"n" n) -> m + n .== m .=> n .== 0)
                []
  
    calc "ltIrreflexive"
         (\(Forall @"m" m) -> sNot (m .< m)) $
         \m -> [m .< m] |-> let k = some "k" (\d -> m .== m + sSucc d)
                        in m .== m + sSucc k
                        ?? cancel `at` (Inst @"m" m, Inst @"n" (sSucc k))
                        =: sSucc k .== 0
                        =: contradiction
  
  -- ** Trichotomy
  
  -- | \(m \geq n = \overline{m} \geq \overline{n}\)
  --
  -- >>> runTP lteEquiv
  -- Lemma: n2iAdd                           Q.E.D.
  -- Lemma: n2iNonNeg                        Q.E.D.
  -- Lemma: n2i2n                            Q.E.D.
  -- Lemma: i2n2i                            Q.E.D.
  -- Lemma: addRightUnit                     Q.E.D.
  -- Lemma: lteEquiv_ltr
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.2.4                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: lteEquiv_rtl
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Step: 7 (2 way case split)
  --     Step: 7.1                           Q.E.D.
  --     Step: 7.2.1                         Q.E.D.
  --     Step: 7.2.2                         Q.E.D.
  --     Step: 7.2.3                         Q.E.D.
  --     Step: 7.2.4                         Q.E.D.
  --     Step: 7.2.5                         Q.E.D.
  --     Step: 7.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: lteEquiv                         Q.E.D.
  -- [Proven] lteEquiv :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  lteEquiv :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  lteEquiv = do
      n2ia    <- recall "n2iAdd"       n2iAdd
      nn      <- recall "n2iNonNeg"    n2iNonNeg
      n2i2nId <- recall "n2i2n"        n2i2n
      i2n2iId <- recall "i2n2i"        i2n2i
      aru     <- recall "addRightUnit" addRightUnit
  
      ltr <- calcWith cvc5 "lteEquiv_ltr"
                (\(Forall @"m" m) (Forall @"n" n) -> (m .>= n) .=> (n2i m .>= n2i n)) $
                \m n -> [m .>= n]
                     |- n2i m .>= n2i n
                      =: cases [ m .== n ==> trivial
                               , m .>  n ==> let k = some "k" (\d -> m .== n + sSucc d)
                                          in n2i m .>= n2i n
                                          ?? m .> n
                                          =: n2i (n + sSucc k) .>= n2i n
                                          ?? n2ia `at` (Inst @"m" n, Inst @"n" (sSucc k))
                                          =: n2i n + n2i (sSucc k) .>= n2i n
                                          ?? nn `at` Inst @"n" (sSucc k)
                                          =: sTrue
                                          =: qed
                               ]
  
      rtl <- calc "lteEquiv_rtl"
                  (\(Forall @"m" m) (Forall @"n" n) -> (n2i m .>= n2i n) .=> (m .>= n)) $
                  \m n -> [n2i m .>= n2i n]
                       |-> let k = n2i m - n2i n
                       in k .>= 0
                       =: n2i m .== n2i n + k
                       ?? i2n2iId `at` Inst @"i" k
                       =: n2i m .== n2i n + n2i (i2n k)
                       ?? n2ia `at` (Inst @"m" n, Inst @"n" (i2n k))
                       =: n2i m .== n2i (n + i2n k)
                       =: i2n (n2i m) .== i2n (n2i (n + i2n k))
                       ?? n2i2nId `at` Inst @"n" m
                       =: m .== i2n (n2i (n + i2n k))
                       ?? n2i2nId `at` Inst @"n" (n + i2n k)
                       =: m .== n + i2n k
                       =: cases [ k .>  0 ==> trivial
                                , k .<= 0 ==> m .== n + i2n k
                                           ?? i2n k .== 0
                                           =: m .== n + 0
                                           ?? aru
                                           =: m .== n
                                           =: m .== n .|| m .> n
                                           =: m .>= n
                                           =: qed
                                ]
  
      lemma "lteEquiv"
            (\(Forall m) (Forall n) -> (n2i m .>= n2i n) .== (m .>= n))
            [proofOf ltr, proofOf rtl]
  
  -- | \(m \geq n \;\lor\; n \geq m\)
  --
  -- >>> runTP ordered
  -- Lemma: lteEquiv                         Q.E.D.
  -- Lemma: ordered
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] ordered :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  ordered :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  ordered = do
     lteEq <- recall "lteEquiv" lteEquiv
  
     calcWith cvc5 "ordered"
          (\(Forall m) (Forall n) -> m .>= n .|| n .>= m) $
          \m n -> [] |- (m .>= n .|| n .>= m)
                     ?? lteEq `at` (Inst @"m" m, Inst @"n" n)
                     =: (n2i m .>= n2i n .|| n .>= m)
                     ?? lteEq `at` (Inst @"m" n, Inst @"n" m)
                     =: (n2i m .>= n2i n .|| n2i n .>= n2i m)
                     =: qed
  
  -- | \(m < n \;\lor\; m = n \;\lor\; n < m\)
  --
  -- >>> runTP trichotomy
  -- Lemma: ordered                          Q.E.D.
  -- Lemma: trichotomy                       Q.E.D.
  -- [Proven] trichotomy :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  trichotomy :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  trichotomy = do
     pOrdered <- recall "ordered" ordered
  
     lemma "trichotomy"
           (\(Forall m) (Forall n) -> m .< n .|| m .== n .|| n .< m)
           [proofOf pOrdered]
  
  -- ** Addition and ordering
  
  -- | \(m < n \;\rightarrow\; m + o < n + o\)
  --
  -- >>> runTP addOrder
  -- Lemma: addAssoc                         Q.E.D.
  -- Lemma: addComm                          Q.E.D.
  -- Lemma: addOrder
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] addOrder :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  addOrder :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  addOrder = do
    pAddAssoc <- recall "addAssoc" addAssoc
    pAddComm  <- recall "addComm"  addComm
  
    calc "addOrder"
         (\(Forall m) (Forall n) (Forall o) -> m .< n .=> m + o .< n + o) $
         \m n o -> [m .< n]
                |-> let k = some "k" (\d -> n .== m + sSucc d)
                 in n .== m + sSucc k
                 =: n + o .== (m + sSucc k) + o
                 ?? pAddAssoc `at` (Inst @"m" m, Inst @"n" (sSucc k), Inst @"o" o)
                 =: n + o .== m + (sSucc k + o)
                 ?? pAddComm `at` (Inst @"m" (sSucc k), Inst @"n" o)
                 =: n + o .== m + (o + sSucc k)
                 ?? pAddAssoc `at` (Inst @"m" m, Inst @"n" o, Inst @"o" (sSucc k))
                 =: n + o .== (m + o) + sSucc k
                 =: m + o .<= n + o
                 =: qed
  
  -- ** Multiplication and ordering
  
  -- | \(o > 0 \;\wedge\; m < n \;\rightarrow\; m * o < n * o\)
  --
  -- >>> runTP mulOrder
  -- Lemma: distribRight                     Q.E.D.
  -- Lemma: mulOrder
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] mulOrder :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool
  mulOrder :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
  mulOrder = do
    pDistribRight <- recall "distribRight" distribRight
  
    calc "mulOrder"
         (\(Forall m) (Forall n) (Forall o) -> 0 .< o .&& m .< n .=> m * o .< n * o) $
         \m n o -> [0 .< o, m .< n]
                |-> let k = some "k" (\d -> n .== m + sSucc d)
                 in n .== m + sSucc k
                 =: n * o .== (m + sSucc k) * o
                 ?? pDistribRight `at` (Inst @"m" m, Inst @"n" (sSucc k), Inst @"o" o)
                 =: n * o .== m * o + sSucc k * o
                 ?? 0 .< o
                 =: n * o .== m * o + sSucc k * sSucc (sprev o)
                 =: n * o .== m * o + (sSucc (sprev o) + k * sSucc (sprev o))
                 =: n * o .== m * o + sSucc (sprev o + k * sSucc (sprev o))
                 =: m * o .< n * o
                 =: qed
  
  -- ** Order and sum
  
  -- | \(m < n \;\rightarrow\; \exists o.\; m + o = n\)
  --
  -- >>> runTP orderSum
  -- Lemma: orderSum                         Q.E.D.
  -- [Proven] orderSum :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool
  orderSum :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
  orderSum = lemma "orderSum"
                   (\(Forall m) (Forall n) -> m .< n .=> quantifiedBool (\(Exists o) -> m + o .== n))
                   []
  
  -- ** 0 and 1 relationship
  
  -- | \(0 < 1\)
  --
  -- >>> runTP zeroLtOne
  -- Lemma: zeroLtOne                        Q.E.D.
  -- [Proven] zeroLtOne :: Bool
  zeroLtOne :: TP (Proof SBool)
  zeroLtOne = lemma "zeroLtOne" (0 .< (1 :: SNat)) []
  
  -- | \(m > 0 \;\rightarrow\; m \geq 1\)
  --
  -- >>> runTP nothingBetweenZeroAndOne
  -- Lemma: nothingBetweenZeroAndOne         Q.E.D.
  -- [Proven] nothingBetweenZeroAndOne :: Ɐm ∷ Nat → Bool
  nothingBetweenZeroAndOne :: TP (Proof (Forall "m" Nat -> SBool))
  nothingBetweenZeroAndOne = lemma "nothingBetweenZeroAndOne"
                                   (\(Forall m) -> m .> 0 .=> m .>= 1)
                                   []
  
  -- ** 0 is the minimum
  
  -- | \(m \geq 0\)
  --
  -- >>> runTP minimumElt
  -- Lemma: minimumElt                       Q.E.D.
  -- [Proven] minimumElt :: Ɐm ∷ Nat → Bool
  minimumElt :: TP (Proof (Forall "m" Nat -> SBool))
  minimumElt = lemma "minimumElt" (\(Forall m) -> m .>= 0) []
  
  -- ** There is no maximum element
  
  -- | \(\forall m \;\exists n \;.\; m < n\)
  --
  -- >>> runTP noMaximumElt
  -- Lemma: noMaximumElt                     Q.E.D.
  -- [Proven] noMaximumElt :: Ɐm ∷ Nat → ∃n ∷ Nat → Bool
  noMaximumElt :: TP (Proof (Forall "m" Nat -> Exists "n" Nat -> SBool))
  noMaximumElt = lemma "noMaximumElt" (\(Forall m) (Exists n) -> m .< n) []
  