-----------------------------------------------------------------------------
-- |
-- 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 { Nat -> Nat
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 :: Integer -> Nat
fromInteger Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = Nat
Zero
                | Bool
True   = Nat -> Nat
Succ (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

  Nat
a + :: Nat -> Nat -> Nat
+ Nat
Zero   = Nat
a
  Nat
a + Succ Nat
b = Nat -> Nat
Succ (Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
b)

  (-) = String -> Nat -> Nat -> Nat
forall a. HasCallStack => String -> a
error String
"Nat: No support for subtraction"

  Nat
_ * :: Nat -> Nat -> Nat
* Nat
Zero   = Nat
Zero
  Nat
a * Succ Nat
b = Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
b

  abs :: Nat -> Nat
abs = Nat -> Nat
forall a. a -> a
id

  signum :: Nat -> Nat
signum Nat
Zero = Nat
0
  signum Nat
_    = Nat
1

  negate :: Nat -> Nat
negate = Nat -> Nat
forall a. a -> a
id

-- Symbolic numeric instance, mirroring the above
instance Num SNat where
  fromInteger :: Integer -> SBV Nat
fromInteger = Nat -> SBV Nat
forall a. SymVal a => a -> SBV a
literal (Nat -> SBV Nat) -> (Integer -> Nat) -> Integer -> SBV Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
forall a. Num a => Integer -> a
fromInteger

  + :: SBV Nat -> SBV Nat -> SBV Nat
(+) = SBV Nat -> SBV Nat -> SBV Nat
plus
      where plus :: SBV Nat -> SBV Nat -> SBV Nat
plus = String
-> (SBV Nat -> SBV Nat -> SBV Nat) -> SBV Nat -> SBV Nat -> SBV Nat
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sNatPlus" ((SBV Nat -> SBV Nat -> SBV Nat) -> SBV Nat -> SBV Nat -> SBV Nat)
-> (SBV Nat -> SBV Nat -> SBV Nat) -> SBV Nat -> SBV Nat -> SBV Nat
forall a b. (a -> b) -> a -> b
$
                     \SBV Nat
m SBV Nat
n -> [sCase|Nat m of
                               Zero   -> n
                               Succ p -> sSucc (p + n)
                             |]

  (-) = String -> SBV Nat -> SBV Nat -> SBV Nat
forall a. HasCallStack => String -> a
error String
"SNat: No support for subtraction"

  * :: SBV Nat -> SBV Nat -> SBV Nat
(*) = SBV Nat -> SBV Nat -> SBV Nat
times
      where times :: SBV Nat -> SBV Nat -> SBV Nat
times = String
-> (SBV Nat -> SBV Nat -> SBV Nat) -> SBV Nat -> SBV Nat -> SBV Nat
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sNatTimes" ((SBV Nat -> SBV Nat -> SBV Nat) -> SBV Nat -> SBV Nat -> SBV Nat)
-> (SBV Nat -> SBV Nat -> SBV Nat) -> SBV Nat -> SBV Nat -> SBV Nat
forall a b. (a -> b) -> a -> b
$
                      \SBV Nat
m SBV Nat
n -> [sCase|Nat m of
                                Zero   -> 0
                                Succ p -> n + p * n
                              |]

  abs :: SBV Nat -> SBV Nat
abs = SBV Nat -> SBV Nat
forall a. a -> a
id

  signum :: SBV Nat -> SBV Nat
signum SBV Nat
m = [sCase|Nat m of
               Zero -> 0
               _    -> 1
             |]

-- | Symbolic ordering. We only define less-than, other methods use the defaults.
instance OrdSymbolic SNat where
   SBV Nat
m .< :: SBV Nat -> SBV Nat -> SBool
.< SBV Nat
n = (Exists Any Nat -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Exists SBV Nat
k) -> SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
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 :: SBV Nat -> SInteger
n2i = String -> (SBV Nat -> SInteger) -> SBV Nat -> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"n2i" ((SBV Nat -> SInteger) -> SBV Nat -> SInteger)
-> (SBV Nat -> SInteger) -> SBV Nat -> SInteger
forall a b. (a -> b) -> a -> b
$ \SBV Nat
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 :: SInteger -> SBV Nat
i2n = String -> (SInteger -> SBV Nat) -> SInteger -> SBV Nat
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"i2n" ((SInteger -> SBV Nat) -> SInteger -> SBV Nat)
-> (SInteger -> SBV Nat) -> SInteger -> SBV Nat
forall a b. (a -> b) -> a -> b
$ \SInteger
i -> SBool -> SBV Nat -> SBV Nat -> SBV Nat
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SBV Nat
0 (SBV Nat -> SBV Nat
sSucc (SInteger -> SBV Nat
i2n (SInteger
i SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
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 :: TP (Proof (Forall "n" Nat -> SBool))
n2iNonNeg = String
-> (Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"n2iNonNeg" (\(Forall SBV Nat
n) -> SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
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 :: TP (Proof (Forall "i" Integer -> SBool))
i2n2i = String
-> (Forall "i" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "i" Integer -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"i2n2i" (\(Forall SInteger
i) -> SBV Nat -> SInteger
n2i (SInteger -> SBV Nat
i2n SInteger
i) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
i SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
`smax` SInteger
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 :: TP (Proof (Forall "n" Nat -> SBool))
n2i2n = String
-> (Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"n2i2n" (\(Forall SBV Nat
n) -> SInteger -> SBV Nat
i2n (SBV Nat -> SInteger
n2i SBV Nat
n) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
n2iAdd = String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"n2iAdd" (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> SBV Nat -> SInteger
n2i (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i SBV Nat
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addCorrect = String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
               String
"addCorrect"
               (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> SBV Nat -> SInteger
n2i (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i SBV Nat
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 :: TP (Proof (Forall "m" Nat -> SBool))
addLeftUnit = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"addLeftUnit" (\(Forall SBV Nat
m) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m) []

-- | \(m + 0 = m\)
--
-- >>> runTP addRightUnit
-- Lemma: addRightUnit                     Q.E.D.
-- [Proven] addRightUnit :: Ɐm ∷ Nat → Bool
addRightUnit :: TP (Proof (Forall "m" Nat -> SBool))
addRightUnit :: TP (Proof (Forall "m" Nat -> SBool))
addRightUnit = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"addRightUnit" (\(Forall SBV Nat
m) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addSucc = do
   Proof (Forall "n" Nat -> SBool)
caseZero <- String
-> (Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero"
                      (\(Forall @"n" SBV Nat
n) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc (SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n))
                      []

   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                    (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) ->
                        SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBool -> SBool -> SBool
.=> SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n)) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \SBV Nat
m SBV Nat
n -> let ih :: SBool
ih = SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n)
                         in [SBool
ih] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n
                                 SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n)
                                 SBV Nat -> SBool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                                 TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n))
                                 SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n)
                                 SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
qed

   String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
      String
"addSucc"
      (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n))
      [Proof (Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "n" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
addAssoc = String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
             String
"addAssoc"
             (\(Forall SBV Nat
m) (Forall SBV Nat
n) (Forall SBV Nat
o) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addComm = do
    Proof (Forall "m" Nat -> SBool)
alu <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addLeftUnit"  TP (Proof (Forall "m" Nat -> SBool))
addLeftUnit
    Proof (Forall "m" Nat -> SBool)
aru <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addRightUnit" TP (Proof (Forall "m" Nat -> SBool))
addRightUnit

    Proof (Forall "n" Nat -> SBool)
caseZero <- String
-> (Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero"
                      (\(Forall @"n" (SBV Nat
n :: SNat)) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
0)
                      [Proof (Forall "m" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> SBool)
alu, Proof (Forall "m" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> SBool)
aru]

    Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
as <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addSucc" TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addSucc

    Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                     (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBool -> SBool -> SBool
.=> SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
                     \SBV Nat
m SBV Nat
n -> let ih :: SBool
ih = SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m
                          in [SBool
ih] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n
                                  SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n)
                                  SBV Nat -> SBool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                                  TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m)
                                  SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
as Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
m)
                                  TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m
                                  SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
qed

    String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"addComm"
                   (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m)
                   [Proof (Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "n" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
mulCorrect = do
   Proof (Forall "n" Nat -> SBool)
caseZero <- String
-> (Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero"
                     (\(Forall @"n" SBV Nat
n) -> SBV Nat -> SInteger
n2i (SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
0 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i SBV Nat
n)
                     []

   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
addC <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addCorrect" TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addCorrect

   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Integer
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                    (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) ->
                          SBV Nat -> SInteger
n2i (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i SBV Nat
n SBool -> SBool -> SBool
.=> SBV Nat -> SInteger
n2i (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i (SBV Nat -> SBV Nat
sSucc SBV Nat
m) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i SBV Nat
n) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Integer
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Integer
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \SBV Nat
m SBV Nat
n -> let ih :: SBool
ih = SBV Nat -> SInteger
n2i (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i SBV Nat
n
                         in [SBool
ih] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SInteger
n2i (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n)
                                 SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
addC Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n))
                                 TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n)
                                 SInteger -> SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                                 TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i SBV Nat
n
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i SBV Nat
m)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i (SBV Nat -> SBV Nat
sSucc SBV Nat
m)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed

   String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
       String
"mullCorrect"
       (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat -> SInteger
n2i (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Nat -> SInteger
n2i SBV Nat
n)
       [Proof (Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "n" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
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 :: TP (Proof (Forall "m" Nat -> SBool))
mulLeftAbsorb = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"mulLeftAbsorb" (\(Forall SBV Nat
m) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
0) []

-- | \(m * 0 = 0\)
--
-- >>> runTP mulRightAbsorb
-- Lemma: mulRightAbsorb                   Q.E.D.
-- [Proven] mulRightAbsorb :: Ɐm ∷ Nat → Bool
mulRightAbsorb :: TP (Proof (Forall "m" Nat -> SBool))
mulRightAbsorb :: TP (Proof (Forall "m" Nat -> SBool))
mulRightAbsorb = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"mulRightAbsorb" (\(Forall SBV Nat
m) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
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 :: TP (Proof (Forall "m" Nat -> SBool))
mulLeftUnit = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"mulLeftUnit" (\(Forall SBV Nat
m) -> SBV Nat -> SBV Nat
sSucc SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
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 :: TP (Proof (Forall "m" Nat -> SBool))
mulRightUnit = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"mulRightUnit" (\(Forall SBV Nat
m) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
distribLeft = do
   Proof (Forall "n" Nat -> Forall "o" Nat -> SBool)
caseZero <- String
-> (Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero" (\(Forall @"n" SBV Nat
n) (Forall @"o" (SBV Nat
o :: SNat)) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) []

   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
addAsc <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addAssoc" TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
addAssoc
   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
addCom <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addComm"  TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addComm

   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall t.
(Proposition
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) t
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                    (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) (Forall @"o" SBV Nat
o) ->
                        SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBool -> SBool -> SBool
.=> SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) (StepArgs
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
 -> TP
      (Proof
         (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)))
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
               \SBV Nat
m SBV Nat
n SBV Nat
o -> let ih :: SBool
ih = SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                      in [SBool
ih] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o)
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o)
                              SBV Nat -> SBool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
addAsc Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
o, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o))
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o))
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
addCom Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o))
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n))
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
addAsc Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
o, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n))
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ ((SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n)
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n)
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
addCom Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n))
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
addAsc Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o))
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
qed

   String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
     String
"distribLeft"
     (\(Forall SBV Nat
m) (Forall SBV Nat
n) (Forall SBV Nat
o) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
     [Proof (Forall "n" Nat -> Forall "o" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "n" Nat -> Forall "o" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
distribRight = do
   Proof (Forall "n" Nat -> Forall "o" Nat -> SBool)
caseZero <- String
-> (Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero" (\(Forall @"n" SBV Nat
n) (Forall @"o" (SBV Nat
o :: SNat)) -> (SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) []

   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pAddAssoc <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addAssoc" TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
addAssoc
   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddCom   <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addComm"  TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addComm
   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddSucc  <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addSucc"  TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addSucc

   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall t.
(Proposition
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) t
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                    (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) (Forall @"o" SBV Nat
o) ->
                        (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBool -> SBool -> SBool
.=> (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) (StepArgs
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
 -> TP
      (Proof
         (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)))
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
               \SBV Nat
m SBV Nat
n SBV Nat
o -> let ih :: SBool
ih = (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                      in [SBool
ih] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddCom Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SBV Nat -> SBV Nat
sSucc SBV Nat
m), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
n)
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
m) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddSucc Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
m)
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddCom Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
m)
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> SBool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
*SBV Nat
o)
                              SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pAddAssoc Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
o, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o))
                              TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
qed

   String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
     String
"distribRight"
     (\(Forall SBV Nat
m) (Forall SBV Nat
n) (Forall SBV Nat
o) -> (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
     [Proof (Forall "n" Nat -> Forall "o" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "n" Nat -> Forall "o" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
mulSucc = do
   Proof (Forall "m" Nat -> SBool)
alu <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addLeftUnit"    TP (Proof (Forall "m" Nat -> SBool))
addLeftUnit
   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
dL  <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"distribLeft"    TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
distribLeft
   Proof (Forall "m" Nat -> SBool)
mru <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"mulRightUnit"   TP (Proof (Forall "m" Nat -> SBool))
mulRightUnit
   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
ac  <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addComm"        TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addComm

   String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"mulSucc"
        (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV Nat
m SBV Nat
n -> [] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
n
                   SBV Nat -> Proof (Forall "m" Nat -> SBool) -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> SBool)
alu
                   TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc (SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n)
                   SBV Nat -> String -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"defn of +"
                   TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat -> SBV Nat
sSucc SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n)
                   SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
dL Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
0), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" SBV Nat
n)
                   TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n
                   SBV Nat -> Proof (Forall "m" Nat -> SBool) -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> SBool)
mru
                   TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n
                   SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
ac Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n))
                   TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m
                   SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
mulAssoc = do
   Proof (Forall "n" Nat -> Forall "o" Nat -> SBool)
caseZero <- String
-> (Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero"
                     (\(Forall @"n" SBV Nat
n) (Forall @"o" (SBV Nat
o :: SNat)) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
                     []

   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
distR <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"distribRight" TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
distribRight

   Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall t.
(Proposition
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) t
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                    (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) (Forall @"o" SBV Nat
o) ->
                       SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBool -> SBool -> SBool
.=> SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) (StepArgs
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
 -> TP
      (Proof
         (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)))
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Nat
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \SBV Nat
m SBV Nat
n SBV Nat
o -> let ih :: SBool
ih = SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                              in [SBool
ih] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
                                      SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
                                      SBV Nat -> SBool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                                      TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                                      SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
distR Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" SBV Nat
o)
                                      TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                                      SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
                                      SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
qed

   String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
     String
"mulAssoc"
     (\(Forall SBV Nat
m) (Forall SBV Nat
n) (Forall SBV Nat
o) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o)
     [Proof (Forall "n" Nat -> Forall "o" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "n" Nat -> Forall "o" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
mulComm = do
  Proof (Forall "m" Nat -> SBool)
mra <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"mulRightAbsorb" TP (Proof (Forall "m" Nat -> SBool))
mulRightAbsorb

  Proof (Forall "m" Nat -> SBool)
caseZero <- String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"caseZero"
                    (\(Forall @"m" (SBV Nat
m :: SNat)) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
0)
                    [Proof (Forall "m" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> SBool)
mra]

  Proof (Forall "m" Nat -> SBool)
mru <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"mulRightUnit" TP (Proof (Forall "m" Nat -> SBool))
mulRightUnit
  Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
dL  <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"distribLeft"  TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
distribLeft

  Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
caseSucc <- String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"caseSucc"
                   (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m SBool -> SBool -> SBool
.=> SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
m) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Nat
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \SBV Nat
m SBV Nat
n -> let ih :: SBool
ih = SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m
                        in [SBool
ih] [SBool] -> TPProofRaw (SBV Nat) -> (SBool, TPProofRaw (SBV Nat))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SBV Nat
sSucc SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n
                                SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n
                                SBV Nat -> SBool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBool
ih
                                TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m
                                SBV Nat -> Proof (Forall "m" Nat -> SBool) -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> SBool)
mru
                                TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m
                                SBV Nat -> Proof Bool -> Hinted (SBV Nat)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
dL Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
0), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" SBV Nat
m)
                                TPProofRaw (SBV Nat)
-> ChainsTo (TPProofRaw (SBV Nat))
-> ChainsTo (TPProofRaw (SBV Nat))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* (SBV Nat -> SBV Nat
sSucc SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m)
                                SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc (SBV Nat
0 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
m)
                                SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc SBV Nat
m
                                SBV Nat -> ChainsTo (SBV Nat) -> ChainsTo (SBV Nat)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Nat)
TPProofRaw (SBV Nat)
forall a. TPProofRaw a
qed

  String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
    String
"mulComm"
    (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
m)
    [Proof (Forall "m" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> SBool)
caseZero, Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
ltTrans = do
  Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
aa <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addAssoc" TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
addAssoc

  String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall t.
(Proposition
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) t
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"ltTrans"
       (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) (Forall @"o" SBV Nat
o) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBool -> SBool -> SBool
.&& SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o SBool -> SBool -> SBool
.=> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o) (StepArgs
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
 -> TP
      (Proof
         (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)))
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SBV Nat
m SBV Nat
n SBV Nat
o ->  [SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n, SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o]
              [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let k1 :: SBV Nat
k1 = String -> (SBV Nat -> SBool) -> SBV Nat
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k1" (\SBV Nat
k -> SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k)
                      k2 :: SBV Nat
k2 = String -> (SBV Nat -> SBool) -> SBV Nat
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k2" (\SBV Nat
k -> SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k)
               in SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k1
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k2
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k1) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k2
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
aa Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
k1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" (SBV Nat -> SBV Nat
sSucc SBV Nat
k2))
               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat -> SBV Nat
sSucc SBV Nat
k1 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k2)
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc (SBV Nat
k1 SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k2)
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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 :: TP (Proof (Forall "m" Nat -> SBool))
ltIrreflexive = do
  Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
cancel <- String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma
              String
"cancel"
              (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBool -> SBool -> SBool
.=> SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
0)
              []

  String
-> (Forall "m" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"ltIrreflexive"
       (\(Forall @"m" SBV Nat
m) -> SBool -> SBool
sNot (SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
m)) (StepArgs (Forall "m" Nat -> SBool) Bool
 -> TP (Proof (Forall "m" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SBV Nat
m -> [SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
m] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let k :: SBV Nat
k = String -> (SBV Nat -> SBool) -> SBV Nat
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Nat
d -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
d)
                      in SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k
                      SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
cancel Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
k))
                      TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SBV Nat
sSucc SBV Nat
k SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
0
                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. Contradiction a => a
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
lteEquiv = do
    Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
n2ia    <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"n2iAdd"       TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
n2iAdd
    Proof (Forall "n" Nat -> SBool)
nn      <- String
-> TP (Proof (Forall "n" Nat -> SBool))
-> TP (Proof (Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"n2iNonNeg"    TP (Proof (Forall "n" Nat -> SBool))
n2iNonNeg
    Proof (Forall "n" Nat -> SBool)
n2i2nId <- String
-> TP (Proof (Forall "n" Nat -> SBool))
-> TP (Proof (Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"n2i2n"        TP (Proof (Forall "n" Nat -> SBool))
n2i2n
    Proof (Forall "i" Integer -> SBool)
i2n2iId <- String
-> TP (Proof (Forall "i" Integer -> SBool))
-> TP (Proof (Forall "i" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"i2n2i"        TP (Proof (Forall "i" Integer -> SBool))
i2n2i
    Proof (Forall "m" Nat -> SBool)
aru     <- String
-> TP (Proof (Forall "m" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addRightUnit" TP (Proof (Forall "m" Nat -> SBool))
addRightUnit

    Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
ltr <- SMTConfig
-> String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcWith SMTConfig
cvc5 String
"lteEquiv_ltr"
              (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> (SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n) SBool -> SBool -> SBool
.=> (SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n)) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
              \SBV Nat
m SBV Nat
n -> [SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n]
                   [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n
                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                             , SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SBV Nat
n SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let k :: SBV Nat
k = String -> (SBV Nat -> SBool) -> SBV Nat
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Nat
d -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
d)
                                        in SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n
                                        SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Nat
n
                                        TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n
                                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
n2ia Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
k))
                                        TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i (SBV Nat -> SBV Nat
sSucc SBV Nat
k) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n
                                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Nat -> SBool)
nn Proof (Forall "n" Nat -> SBool)
-> IArgs (Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
k)
                                        TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                             ]

    Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
rtl <- String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"lteEquiv_rtl"
                (\(Forall @"m" SBV Nat
m) (Forall @"n" SBV Nat
n) -> (SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n) SBool -> SBool -> SBool
.=> (SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n)) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
                \SBV Nat
m SBV Nat
n -> [SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n]
                     [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let k :: SInteger
k = SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SBV Nat -> SInteger
n2i SBV Nat
n
                     in SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
k
                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "i" Integer -> SBool)
i2n2iId Proof (Forall "i" Integer -> SBool)
-> IArgs (Forall "i" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SInteger
k
                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV Nat -> SInteger
n2i (SInteger -> SBV Nat
i2n SInteger
k)
                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
n2ia Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger -> SBV Nat
i2n SInteger
k))
                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat -> SInteger
n2i (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SInteger -> SBV Nat
i2n SInteger
k)
                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SBV Nat
i2n (SBV Nat -> SInteger
n2i SBV Nat
m) SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SBV Nat
i2n (SBV Nat -> SInteger
n2i (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SInteger -> SBV Nat
i2n SInteger
k))
                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Nat -> SBool)
n2i2nId Proof (Forall "n" Nat -> SBool)
-> IArgs (Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
m
                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SBV Nat
i2n (SBV Nat -> SInteger
n2i (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SInteger -> SBV Nat
i2n SInteger
k))
                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Nat -> SBool)
n2i2nId Proof (Forall "n" Nat -> SBool)
-> IArgs (Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SInteger -> SBV Nat
i2n SInteger
k)
                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SInteger -> SBV Nat
i2n SInteger
k
                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                              , SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SInteger -> SBV Nat
i2n SInteger
k
                                         SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger -> SBV Nat
i2n SInteger
k SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
0
                                         TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
0
                                         SBool -> Proof (Forall "m" Nat -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> SBool)
aru
                                         TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n
                                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Nat
n
                                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n
                                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                              ]

    String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"lteEquiv"
          (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> (SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n))
          [Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
ltr, Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
ordered = do
   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
lteEq <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"lteEquiv" TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
lteEquiv

   SMTConfig
-> String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall t.
(Proposition (Forall "m" Nat -> Forall "n" Nat -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) t
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcWith SMTConfig
cvc5 String
"ordered"
        (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
m) (StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
 -> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)))
-> StepArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) Bool
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV Nat
m SBV Nat
n -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
m)
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
lteEq Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
n)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
m)
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
lteEq Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
m)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Nat -> SInteger
n2i SBV Nat
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat -> SInteger
n2i SBV Nat
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat -> SInteger
n2i SBV Nat
m)
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
trichotomy = do
   Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pOrdered <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"ordered" TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
ordered

   String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"trichotomy"
         (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n SBool -> SBool -> SBool
.|| SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
m)
         [Proof (Forall "m" Nat -> Forall "n" Nat -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
addOrder = do
  Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pAddAssoc <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addAssoc" TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
addAssoc
  Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddComm  <- String
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"addComm"  TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
addComm

  String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall t.
(Proposition
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) t
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"addOrder"
       (\(Forall SBV Nat
m) (Forall SBV Nat
n) (Forall SBV Nat
o) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBool -> SBool -> SBool
.=> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) (StepArgs
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
 -> TP
      (Proof
         (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)))
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SBV Nat
m SBV Nat
n SBV Nat
o -> [SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n]
              [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let k :: SBV Nat
k = String -> (SBV Nat -> SBool) -> SBV Nat
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Nat
d -> SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
d)
               in SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pAddAssoc Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
k), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" SBV Nat
o)
               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat -> SBV Nat
sSucc SBV Nat
k SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o)
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
pAddComm Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> IArgs (Forall "m" Nat -> Forall "n" Nat -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SBV Nat -> SBV Nat
sSucc SBV Nat
k), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
o)
               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k)
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pAddAssoc Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Nat
o, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" (SBV Nat -> SBV Nat
sSucc SBV Nat
k))
               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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 :: TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
mulOrder = do
  Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pDistribRight <- String
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"distribRight" TP
  (Proof
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
distribRight

  String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall t.
(Proposition
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) t
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"mulOrder"
       (\(Forall SBV Nat
m) (Forall SBV Nat
n) (Forall SBV Nat
o) -> SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o SBool -> SBool -> SBool
.&& SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBool -> SBool -> SBool
.=> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o) (StepArgs
   (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
 -> TP
      (Proof
         (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)))
-> StepArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool) Bool
-> TP
     (Proof
        (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SBV Nat
m SBV Nat
n SBV Nat
o -> [SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o, SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n]
              [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let k :: SBV Nat
k = String -> (SBV Nat -> SBool) -> SBV Nat
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Nat
d -> SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
d)
               in SBV Nat
n SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
pDistribRight Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> IArgs
     (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Nat
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Nat -> SBV Nat
sSucc SBV Nat
k), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"o" SBV Nat
o)
               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
               SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
o
               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc SBV Nat
k SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sprev SBV Nat
o)
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ (SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sprev SBV Nat
o) SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
k SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sprev SBV Nat
o))
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sprev SBV Nat
o SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
k SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat -> SBV Nat
sSucc (SBV Nat -> SBV Nat
sprev SBV Nat
o))
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
* SBV Nat
o
               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
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 :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
orderSum = String
-> (Forall "m" Nat -> Forall "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"orderSum"
                 (\(Forall SBV Nat
m) (Forall SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n SBool -> SBool -> SBool
.=> (Exists Any Nat -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Exists SBV Nat
o) -> SBV Nat
m SBV Nat -> SBV Nat -> SBV Nat
forall a. Num a => a -> a -> a
+ SBV Nat
o SBV Nat -> SBV Nat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nat
n))
                 []

-- ** 0 and 1 relationship

-- | \(0 < 1\)
--
-- >>> runTP zeroLtOne
-- Lemma: zeroLtOne                        Q.E.D.
-- [Proven] zeroLtOne :: Bool
zeroLtOne :: TP (Proof SBool)
zeroLtOne :: TP (Proof SBool)
zeroLtOne = String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"zeroLtOne" (SBV Nat
0 SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< (SBV Nat
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 :: TP (Proof (Forall "m" Nat -> SBool))
nothingBetweenZeroAndOne = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"nothingBetweenZeroAndOne"
                                 (\(Forall SBV Nat
m) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Nat
0 SBool -> SBool -> SBool
.=> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
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 :: TP (Proof (Forall "m" Nat -> SBool))
minimumElt = String
-> (Forall "m" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"minimumElt" (\(Forall SBV Nat
m) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Nat
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 :: TP (Proof (Forall "m" Nat -> Exists "n" Nat -> SBool))
noMaximumElt = String
-> (Forall "m" Nat -> Exists "n" Nat -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "m" Nat -> Exists "n" Nat -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"noMaximumElt" (\(Forall SBV Nat
m) (Exists SBV Nat
n) -> SBV Nat
m SBV Nat -> SBV Nat -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Nat
n) []