-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Numeric
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Example use of inductive TP proofs, over integers.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE QuasiQuotes         #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Numeric where

import Prelude hiding (sum, map, product, length, (^), replicate, elem)

import Data.SBV
import Data.SBV.TP
import Data.SBV.List

#ifdef DOCTEST
-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> import Data.SBV
-- >>> import Data.SBV.TP
-- >>> import Control.Exception
#endif

-- * Sum of constants

-- | \(\sum_{i=1}^{n} c = c \cdot n\)
--
-- >>> runTP $ sumConstProof (uninterpret "c")
-- Inductive lemma: sumConst_correct
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] sumConst_correct :: Ɐn ∷ Integer → Bool
sumConstProof :: SInteger -> TP (Proof (Forall "n" Integer -> SBool))
sumConstProof :: SInteger -> TP (Proof (Forall "n" Integer -> SBool))
sumConstProof SInteger
c = String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sumConst_correct"
                         (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger -> SInteger -> SList Integer
forall a. SymVal a => SInteger -> SBV a -> SList a
replicate SInteger
n SInteger
c) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                         \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger -> SInteger -> SList Integer
forall a. SymVal a => SInteger -> SBV a -> SList a
replicate (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
c)
                                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger
c SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SInteger -> SList Integer
forall a. SymVal a => SInteger -> SBV a -> SList a
replicate SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger
c)
                                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger -> SInteger -> SList Integer
forall a. SymVal a => SInteger -> SBV a -> SList a
replicate SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger
c)
                                            SInteger -> Proof SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
cSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
IHArg (Forall "n" Integer -> SBool)
n
                                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
cSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                            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

-- * Sum of numbers

-- | \(\sum_{i=0}^{n} i = \frac{n(n+1)}{2}\)
--
-- NB. We define the sum of numbers from @0@ to @n@ as @sum [sEnum|n, n-1 .. 0|]@, i.e., we
-- construct the list starting from @n@ going down to @0@. Contrast this to the perhaps more natural
-- definition of @sum [sEnum|0 .. n]@, i.e., going up. While the latter is equivalent functionality, the former
-- works much better with the proof-structure: Since we induct on @n@, in each step we strip of one
-- layer, and the recursion in the down-to construction matches the inductive schema.
--
-- >>> runTP sumProof
-- Inductive lemma: sum_correct
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] sum_correct :: Ɐn ∷ Integer → Bool
sumProof :: TP (Proof (Forall "n" Integer -> SBool))
sumProof :: TP (Proof (Forall "n" Integer -> SBool))
sumProof = String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sum_correct"
                  (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n, n-1 .. 0|] SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n+1, n .. 0|]
                                     SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n, n-1 .. 0|]
                                     SInteger -> Proof SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                                     TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                                     SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                                     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

-- * Sum of squares of numbers
--
-- | \(\sum_{i=0}^{n} i^2 = \frac{n(n+1)(2n+1)}{6}\)
--
-- >>> runTP sumSquareProof
-- Inductive lemma: sumSquare_correct
--   Step: Base                            Q.E.D.
--   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] sumSquare_correct :: Ɐn ∷ Integer → Bool
sumSquareProof :: TP (Proof (Forall "n" Integer -> SBool))
sumSquareProof :: TP (Proof (Forall "n" Integer -> SBool))
sumSquareProof = do
   let sq :: SInteger -> SInteger
       sq :: SInteger -> SInteger
sq SInteger
k = SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
k

       sumSquare :: SInteger -> SInteger
sumSquare SInteger
n = SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ (SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SInteger
sq [sEnum|n, n-1 .. 0|]

   String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sumSquare_correct"
          (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger
sumSquare SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
6) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
sumSquare (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SInteger
sq [sEnum|n+1, n .. 0|])
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SInteger
sq (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: [sEnum|n, n-1 .. 0|]))
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SInteger
sq [sEnum|n, n-1 .. 0|])
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map SInteger -> SInteger
sq [sEnum|n, n-1 .. 0|])
                             SInteger -> Proof SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                             TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
6
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
3)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
6
                             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

-- * Sum of cubes of numbers

-- | \(\sum_{i=0}^{n} i^3 = \left( \sum_{i=0}^{n} i \right)^2 = \left( \frac{n(n+1)}{2} \right)^2\)
--
-- This is attributed to Nicomachus, hence the name.
--
-- >>> runTP nicomachus
-- Inductive lemma: sum_correct
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: evenHalfSquared                  Q.E.D.
-- Inductive lemma: nn1IsEven
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: sum_squared
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: nicomachus
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] nicomachus :: Ɐn ∷ Integer → Bool
nicomachus :: TP (Proof (Forall "n" Integer -> SBool))
nicomachus :: TP (Proof (Forall "n" Integer -> SBool))
nicomachus = do
   let (^) :: SInteger -> Integer -> SInteger
       SInteger
_ ^ :: SInteger -> Integer -> SInteger
^ Integer
0 = SInteger
1
       SInteger
b ^ Integer
n = SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b SInteger -> Integer -> SInteger
^ (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
       infixr 8 ^

       sumCubed :: SInteger -> SInteger
       sumCubed :: SInteger -> SInteger
sumCubed = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"sumCubed" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
0 (SInteger
nSInteger -> Integer -> SInteger
^Integer
3 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sumCubed (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

   -- Grab the proof of regular summation formula
   Proof (Forall "n" Integer -> SBool)
sp <- TP (Proof (Forall "n" Integer -> SBool))
sumProof

   -- Square of the summation result. This is a trivial lemma for humans, but there are lots
   -- of multiplications involved making the problem non-linear and we need to spell it out.
   Proof (Forall "n" Integer -> SBool)
ssp <- do
        -- Squaring half of an even number? You can square the number and divide by 4 instead:
        -- z3 can prove this out of the box, but without it being explicitly expressed, the
        -- following proof doesn't go through.
        Proof (Forall "n" Integer -> SBool)
evenHalfSquared <- String
-> (Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"evenHalfSquared"
                                 (\(Forall SInteger
n) -> Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger
n SBool -> SBool -> SBool
.=> (SInteger
n SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) SInteger -> Integer -> SInteger
^ Integer
2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
n SInteger -> Integer -> SInteger
^ Integer
2) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
4)
                                 []

        -- The multiplication @n * (n+1)@ is always even. It's surprising that I had to use induction here
        -- but neither z3 nor cvc5 can converge on this out-of-the-box.
        Proof (Forall "n" Integer -> SBool)
nn1IsEven <- String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"nn1IsEven"
                            (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> Integer
2 Integer -> SInteger -> SBool
`sDivides` (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                            \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n 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)
|- Integer
2 Integer -> SInteger -> SBool
`sDivides` ((SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2))
                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
2 Integer -> SInteger -> SBool
`sDivides` (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
2 Integer -> SInteger -> SBool
`sDivides` (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                                               SBool -> Proof SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                                               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

        String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"sum_squared"
               (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n, n-1 .. 0|] SInteger -> Integer -> SInteger
^ Integer
2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
nSInteger -> Integer -> SInteger
^Integer
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> Integer -> SInteger
^Integer
2) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
4) (StepArgs (Forall "n" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
               \SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n, n-1 .. 0|] SInteger -> Integer -> SInteger
^ Integer
2
                               SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
sp Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" 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 @"n" SInteger
n
                               TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2)SInteger -> Integer -> SInteger
^Integer
2
                               SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
nn1IsEven Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" 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 @"n" SInteger
n
                               TPProofRaw SInteger -> Proof Bool -> Hinted (TPProofRaw SInteger)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
evenHalfSquared Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" 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 @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                               Hinted (TPProofRaw SInteger)
-> ChainsTo (Hinted (TPProofRaw SInteger))
-> ChainsTo (Hinted (TPProofRaw SInteger))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))SInteger -> Integer -> SInteger
^Integer
2) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
4
                               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

   -- We can finally put it together:
   String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"nicomachus"
          (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger
sumCubed SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n, n-1 .. 0|] SInteger -> Integer -> SInteger
^ Integer
2) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
sumCubed (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> Integer -> SInteger
^Integer
3 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sumCubed SInteger
IHArg (Forall "n" Integer -> SBool)
n
                SInteger -> Proof SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                TPProofRaw SInteger
-> Proof (Forall "n" Integer -> SBool)
-> Hinted (TPProofRaw SInteger)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ssp
                Hinted (TPProofRaw SInteger)
-> ChainsTo (Hinted (TPProofRaw SInteger))
-> ChainsTo (Hinted (TPProofRaw SInteger))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [sEnum|n+1, n .. 0|] SInteger -> Integer -> SInteger
^ Integer
2
                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

-- * Exponents and divisibility by 7

-- | \(7 \mid \left(11^n - 4^n\right)\)
--
-- NB. As of Feb 2025, z3 struggles with the inductive step in this proof, but cvc5 performs just fine.
--
-- >>> runTP elevenMinusFour
-- Lemma: powN                             Q.E.D.
-- Inductive lemma: elevenMinusFour
--   Step: Base                            Q.E.D.
--   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.
--   Result:                               Q.E.D.
-- [Proven] elevenMinusFour :: Ɐn ∷ Integer → Bool
elevenMinusFour :: TP (Proof (Forall "n" Integer -> SBool))
elevenMinusFour :: TP (Proof (Forall "n" Integer -> SBool))
elevenMinusFour = do
   let pow :: SInteger -> SInteger -> SInteger
       pow :: SInteger -> SInteger -> SInteger
pow = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"pow" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
x SInteger
y -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
1 (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
pow SInteger
x (SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

       emf :: SInteger -> SBool
       emf :: SInteger -> SBool
emf SInteger
n = Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
n)

   -- helper
   Proof (Forall "x" Integer -> Forall "n" Integer -> SBool)
powN <- String
-> (Forall "x" Integer -> Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Integer -> Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"powN" (\(Forall SInteger
x) (Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SInteger
`pow` (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x SInteger -> SInteger -> SInteger
`pow` SInteger
n) []

   SMTConfig
-> String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"elevenMinusFour"
          (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SBool
emf SInteger
n) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n 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)
|- SInteger -> SBool
emf (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
`pow` (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" Integer -> Forall "n" Integer -> SBool)
powN Proof (Forall "x" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "x" Integer -> Forall "n" 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 @"x" SInteger
11, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
IHArg (Forall "n" Integer -> SBool)
n)
                TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" Integer -> Forall "n" Integer -> SBool)
powN Proof (Forall "x" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "x" Integer -> Forall "n" 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 @"x" SInteger
4, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
IHArg (Forall "n" Integer -> SBool)
n)
                TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n))
                SBool -> Proof SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let x :: SInteger
x = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"x" (\SInteger
v -> SInteger
7SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n)   -- Apply the IH and grab the witness for it
                in Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x))
                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

-- * A proof about factorials

-- | \(\sum_{k=0}^{n} k \cdot k! = (n+1)! - 1\)
--
-- >>> runTP sumMulFactorial
-- Lemma: fact (n+1)
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: sumMulFactorial
--   Step: Base                            Q.E.D.
--   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.
-- [Proven] sumMulFactorial :: Ɐn ∷ Integer → Bool
sumMulFactorial :: TP (Proof (Forall "n" Integer -> SBool))
sumMulFactorial :: TP (Proof (Forall "n" Integer -> SBool))
sumMulFactorial = do
  let fact :: SInteger -> SInteger
      fact :: SInteger -> SInteger
fact SInteger
n = SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product [sEnum|n, n-1 .. 1|]

  -- This is pure expansion, but without it z3 struggles in the next lemma.
  Proof (Forall "n" Integer -> SBool)
helper <- String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"fact (n+1)"
                 (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger
fact (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
n) (StepArgs (Forall "n" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
fact (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product [sEnum|n+1, n .. 1|]
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: [sEnum|n, n-1 .. 1|])
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product [sEnum|n, n-1 .. 1|]
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
n
                                 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 "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sumMulFactorial"
         (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map (\SInteger
k -> SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
k) [sEnum|n, n-1 .. 0|]) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fact (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map (\SInteger
k -> SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
k) [sEnum|n+1, n .. 0|])
                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map (\SInteger
k -> SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
k) (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: [sEnum|n, n-1 .. 0|]))
                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map (\SInteger
k -> SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
k) [sEnum|n, n-1 .. 0|])
                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SInteger -> SInteger) -> SList Integer -> SList Integer
forall func a b. SMap func a b => func -> SList a -> SList b
map (\SInteger
k -> SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
k) [sEnum|n, n-1 .. 0|])
                            SInteger -> Proof SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1
                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1
                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1
                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
helper Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" 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 @"n" (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1
                            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

-- * Product with 0

-- | \(\prod_{x \in xs} x = 0 \iff 0 \in xs\)
--
-- >>> runTP product0
-- Inductive lemma: product0
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2 (2 way case split)
--     Step: 2.1                           Q.E.D.
--     Step: 2.2.1                         Q.E.D.
--     Step: 2.2.2                         Q.E.D.
--     Step: 2.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] product0 :: Ɐxs ∷ [Integer] → Bool
product0 :: TP (Proof (Forall "xs" [Integer] -> SBool))
product0 :: TP (Proof (Forall "xs" [Integer] -> SBool))
product0 =
  String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof (IHType (Forall "xs" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> SBool)
    -> IStepArgs (Forall "xs" [Integer] -> SBool) Bool)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall t.
(Proposition (Forall "xs" [Integer] -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof (IHType (Forall "xs" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> SBool)
    -> IStepArgs (Forall "xs" [Integer] -> SBool) t)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"product0"
         (\(Forall @"xs" (SList Integer
xs :: SList Integer)) -> SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.<=> SInteger
0 SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs) ((Proof (IHType (Forall "xs" [Integer] -> SBool))
  -> IHArg (Forall "xs" [Integer] -> SBool)
  -> IStepArgs (Forall "xs" [Integer] -> SBool) Bool)
 -> TP (Proof (Forall "xs" [Integer] -> SBool)))
-> (Proof (IHType (Forall "xs" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> SBool)
    -> IStepArgs (Forall "xs" [Integer] -> SBool) Bool)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$
         \Proof (IHType (Forall "xs" [Integer] -> SBool))
ih (SInteger
x, SList Integer
xs) -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.<=> SInteger
0 SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.<=> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.|| SInteger
0 SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs)
                           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
x SInteger -> SInteger -> SBool
forall a. EqSymbolic 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
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
product SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.<=> SInteger
0 SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs)
                                               SBool -> Proof SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "xs" [Integer] -> SBool))
ih
                                               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
                                    ]

-- * A negative example

-- | The regular inductive proof on integers (i.e., proving at @0@, assuming at @n@ and proving at
-- @n+1@ will not allow you to conclude things when @n < 0@. The following example demonstrates this with the most
-- obvious example:
--
-- >>> badNonNegative `catch` (\(_ :: SomeException) -> pure ())
-- Inductive lemma: badNonNegative
--   Step: Base                            Q.E.D.
--   Step: 1
-- *** Failed to prove badNonNegative.1.
-- Falsifiable. Counter-example:
--   n = -2 :: Integer
badNonNegative :: IO ()
badNonNegative :: IO ()
badNonNegative = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Proof (Forall "n" Integer -> SBool)
_ <- String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"badNonNegative"
                (\(Forall @"n" (SInteger
n :: SInteger)) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
IHArg (Forall "n" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                            SBool -> Proof SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                            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
    () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()