-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Primes
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Prove that there are an infinite number of primes. Along the way we formalize
-- and prove a number of properties about divisibility as well. Our proof is inspired by
-- the ACL2 proof in <https://github.com/acl2/acl2/blob/master/books/projects/numbers/euclid.lisp>.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Primes where

import Data.SBV
import Data.SBV.TP

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV.TP
#endif

-- * Divisibility

-- | Divides relation. By definition @0@ only divides @0@. (But every number divides @0@).
dvd :: SInteger -> SInteger -> SBool
SInteger
x dvd :: SInteger -> SInteger -> SBool
`dvd` SInteger
y = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) (SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) (SInteger
y SInteger -> SInteger -> SInteger
`sEMod` SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)

-- | \(x \mid y \implies x \mid y * z\)
--
-- === __Proof__
-- >>> runTP dividesProduct
-- Lemma: dividesProduct
--   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.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] dividesProduct :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool
dividesProduct :: TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesProduct :: TP
  (Proof
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesProduct = String
-> (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall t.
(Proposition
   (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"dividesProduct"
                      (\(Forall SInteger
x) (Forall SInteger
y) (Forall SInteger
z) -> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
y SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
ySInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
z)) (StepArgs
   (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "x" Integer
          -> Forall "y" Integer -> Forall "z" Integer -> SBool)))
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                      \SInteger
x SInteger
y SInteger
z -> [SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
y]
                             [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw 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)
==> SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
ySInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
z)
                                                 SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
                                                 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
                                      , 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 -> SBool
`dvd` (SInteger
ySInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
z)
                                                 SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x
                                                 TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
`dvd` ((SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
z)
                                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* ((SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
z))
                                                 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
                                      ]
-- | \(x \mid y \land y \mid z \implies x \mid z\)
--
-- === __Proof__
-- >>> runTP dividesTransitive
-- Lemma: dividesProduct                   Q.E.D.
-- Lemma: dividesTransitive
--   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 (hard)                  Q.E.D.
--     Step: 1.2.4                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] dividesTransitive :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool
dividesTransitive :: TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesTransitive :: TP
  (Proof
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesTransitive = do
    Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dp <- String
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dividesProduct" TP
  (Proof
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesProduct

    String
-> (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall t.
(Proposition
   (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"dividesTransitive"
         (\(Forall SInteger
x) (Forall SInteger
y) (Forall SInteger
z) -> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
y SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
`dvd` SInteger
z SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
z) (StepArgs
   (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "x" Integer
          -> Forall "y" Integer -> Forall "z" Integer -> SBool)))
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SInteger
x SInteger
y SInteger
z -> [SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
y, SInteger
y SInteger -> SInteger -> SBool
`dvd` SInteger
z]
                [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw 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 -> SBool -> SBool
.|| SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.|| SInteger
z 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 -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
z 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 -> SBool
`dvd` SInteger
z
                             SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
z SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
z SInteger -> SInteger -> SInteger
`sEDiv` SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
z SInteger -> SInteger -> SInteger
`sEDiv` SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y)
                             SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
`dvd` ((SInteger
z SInteger -> SInteger -> SInteger
`sEDiv` SInteger
y) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x))
                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"hard"
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* ((SInteger
z SInteger -> SInteger -> SInteger
`sEDiv` SInteger
y) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x)))
                             SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dp Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> IArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" 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
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"z" ((SInteger
z SInteger -> SInteger -> SInteger
`sEDiv` SInteger
y) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
y SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x)))
                             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
                         ]

-- * The least divisor

-- | The definition of primality will depend on the notion of least divisor. Given @k@ and @n@, the least-divisor of
-- @n@ that is at least @k@ is the number that is at least @k@ and divides @n@ evenly. The idea is that a number is
-- prime if the least divisor starting from @2@ is itself.
ld :: SInteger -> SInteger -> SInteger
ld :: SInteger -> SInteger -> SInteger
ld = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"ld" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
k SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
k SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
k (SInteger -> SInteger -> SInteger
ld (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
n)

-- | \(1 < k \leq n \implies \mathit{ld}\,k\,n \mid n \land k \leq \mathit{ld}\,k\,n \leq n\)
--
-- === __Proof__
-- >>> runTP leastDivisorDivides
-- Inductive lemma (strong): leastDivisorDivides
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] leastDivisorDivides :: Ɐk ∷ Integer → Ɐn ∷ Integer → Bool
leastDivisorDivides :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorDivides :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorDivides =
   String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> (MeasureArgs
      (Forall "k" Integer -> Forall "n" Integer -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs
         (Forall "k" Integer -> Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "k" Integer -> Forall "n" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> (MeasureArgs
      (Forall "k" Integer -> Forall "n" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs (Forall "k" Integer -> Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
sInduct String
"leastDivisorDivides"
           (\(Forall SInteger
k) (Forall SInteger
n) -> SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.=> let d :: SInteger
d = SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n in SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
n SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n)
           (\SInteger
k SInteger
n -> SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
k, []) ((Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
  -> StepArgs
       (Forall "k" Integer -> Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)))
-> (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs
         (Forall "k" Integer -> Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
           \Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ih SInteger
k SInteger
n -> [SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
k, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n]
                  [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- let d :: SInteger
d = SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n
                  in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
k 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
d SInteger -> SInteger -> SBool
`dvd` SInteger
n SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n
                                                SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
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
                           , SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
k 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
d SInteger -> SInteger -> SBool
`dvd` SInteger
n SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n
                                                SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
ld (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
n
                                                TPProofRaw SBool
-> Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ih
                                                Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (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
                           ]

-- | \(1 < k \leq n \land d \mid n \land k \leq d \implies \mathit{ld}\,k\,n \leq d\)
--
-- === __Proof__
-- >>> runTP leastDivisorIsLeast
-- Inductive lemma (strong): leastDivisorisLeast
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] leastDivisorisLeast :: Ɐk ∷ Integer → Ɐn ∷ Integer → Ɐd ∷ Integer → Bool
leastDivisorIsLeast :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "d" Integer -> SBool))
leastDivisorIsLeast :: TP
  (Proof
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "d" Integer -> SBool))
leastDivisorIsLeast =
  String
-> (Forall "k" Integer
    -> Forall "n" Integer -> Forall "d" Integer -> SBool)
-> (MeasureArgs
      (Forall "k" Integer
       -> Forall "n" Integer -> Forall "d" Integer -> SBool)
      Integer,
    [ProofObj])
-> (Proof
      (Forall "k" Integer
       -> Forall "n" Integer -> Forall "d" Integer -> SBool)
    -> StepArgs
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "d" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "d" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "k" Integer
    -> Forall "n" Integer -> Forall "d" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "k" Integer
    -> Forall "n" Integer -> Forall "d" Integer -> SBool)
-> (MeasureArgs
      (Forall "k" Integer
       -> Forall "n" Integer -> Forall "d" Integer -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "k" Integer
       -> Forall "n" Integer -> Forall "d" Integer -> SBool)
    -> StepArgs
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "d" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "d" Integer -> SBool))
sInduct String
"leastDivisorisLeast"
          (\(Forall SInteger
k) (Forall SInteger
n) (Forall SInteger
d) -> SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
n SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d)
          (\SInteger
k SInteger
n SInteger
_d -> SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
k, []) ((Proof
    (Forall "k" Integer
     -> Forall "n" Integer -> Forall "d" Integer -> SBool)
  -> StepArgs
       (Forall "k" Integer
        -> Forall "n" Integer -> Forall "d" Integer -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "d" Integer -> SBool)))
-> (Proof
      (Forall "k" Integer
       -> Forall "n" Integer -> Forall "d" Integer -> SBool)
    -> StepArgs
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "d" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "d" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "d" Integer -> SBool)
ih SInteger
k SInteger
n SInteger
d -> [SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
k, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n, SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
n, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d]
                    [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
k 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 -> SInteger -> SInteger
ld SInteger
k SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d
                                                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d
                                                  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
                             , SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
k 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 -> SInteger -> SInteger
ld SInteger
k SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
d
                                                  SBool
-> Proof
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "d" Integer -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "d" 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
                             ]

-- | \(n \geq k \geq 2 \implies \mathit{ld}\,k\,(\mathit{ld}\,k\,n) = \mathit{ld}\,k\,n\)
--
-- === __Proof__
-- >>> runTP leastDivisorTwice
-- Lemma: dividesTransitive                Q.E.D.
-- Lemma: leastDivisorDivides              Q.E.D.
-- Lemma: leastDivisorIsLeast              Q.E.D.
-- Lemma: helper1                          Q.E.D.
-- Lemma: helper2                          Q.E.D.
-- Lemma: helper3                          Q.E.D.
-- Lemma: helper4                          Q.E.D.
-- Lemma: helper5
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: leastDivisorTwice                Q.E.D.
-- [Proven] leastDivisorTwice :: Ɐk ∷ Integer → Ɐn ∷ Integer → Bool
leastDivisorTwice :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorTwice :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorTwice = do
  Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dt  <- String
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dividesTransitive"   TP
  (Proof
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesTransitive
  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd <- String
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorDivides" TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorDivides
  Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "d" Integer -> SBool)
ldl <- String
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "d" Integer -> SBool))
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "d" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorIsLeast" TP
  (Proof
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "d" Integer -> SBool))
leastDivisorIsLeast

  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h1 <- String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"helper1"
              (\(Forall @"k" SInteger
k) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n) SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n)
              [Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd]

  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h2 <- String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"helper2"
              (\(Forall @"k" SInteger
k) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n SInteger -> SInteger -> SBool
`dvd` SInteger
n)
              [Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd]

  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h3 <- String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"helper3"
              (\(Forall @"k" SInteger
k) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n) SInteger -> SInteger -> SBool
`dvd` SInteger
n)
              [Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h1, Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h2, Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dt]

  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h4 <- String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"helper4"
              (\(Forall @"k" SInteger
k) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n))
              [Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd]

  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h5 <- String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> StepArgs
     (Forall "k" Integer -> Forall "n" Integer -> SBool) Bool
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "k" Integer -> Forall "n" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> StepArgs (Forall "k" Integer -> Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "k" Integer -> 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
"helper5"
              (\(Forall @"k" SInteger
k) (Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n)) (StepArgs (Forall "k" Integer -> Forall "n" Integer -> SBool) Bool
 -> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)))
-> StepArgs
     (Forall "k" Integer -> Forall "n" Integer -> SBool) Bool
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
              \SInteger
k SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2]
                   [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n)
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h3  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "k" 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 @"k" SInteger
k, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n)
                   TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h4  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "k" 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 @"k" SInteger
k, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n)
                   Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "d" Integer -> SBool)
ldl Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "d" Integer -> SBool)
-> IArgs
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "d" 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 @"k" SInteger
k, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"d" (SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n)))
                   Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (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 "k" Integer -> Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"leastDivisorTwice"
        (\(Forall SInteger
k) (Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
ld SInteger
k (SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
ld SInteger
k SInteger
n)
        [Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h1, Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
h5]

-- * Primality

-- | A number is prime if its least divisor greater than or equal to @2@ is itself.
isPrime :: SInteger -> SBool
isPrime :: SInteger -> SBool
isPrime SInteger
n = SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
ld SInteger
2 SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
n

-- | \(\mathit{isPrime}\,p \implies p \geq 2\)
--
-- === __Proof__
-- >>> runTP primeAtLeast2
-- Lemma: primeAtLeast2                    Q.E.D.
-- [Proven] primeAtLeast2 :: Ɐp ∷ Integer → Bool
primeAtLeast2 :: TP (Proof (Forall "p" Integer -> SBool))
primeAtLeast2 :: TP (Proof (Forall "p" Integer -> SBool))
primeAtLeast2 = String
-> (Forall "p" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "p" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"primeAtLeast2" (\(Forall SInteger
p) -> SInteger -> SBool
isPrime SInteger
p SBool -> SBool -> SBool
.=> SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2) []

-- | \(n \geq 2 \implies \mathit{isPrime}\,(\mathit{ld}\,2\,n)\)
--
-- === __Proof__
-- >>> runTP leastDivisorIsPrime
-- Lemma: leastDivisorTwice                Q.E.D.
-- Lemma: leastDivisorDivides              Q.E.D.
-- Lemma: leastDivisorIsPrime
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] leastDivisorIsPrime :: Ɐn ∷ Integer → Bool
leastDivisorIsPrime :: TP (Proof (Forall "n" Integer -> SBool))
leastDivisorIsPrime :: TP (Proof (Forall "n" Integer -> SBool))
leastDivisorIsPrime = do
   Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldt <- String
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorTwice" TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorTwice
   Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd <- String
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorDivides" TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorDivides

   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (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)
-> 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
"leastDivisorIsPrime"
        (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> SBool -> SBool
.=> SInteger -> SBool
isPrime (SInteger -> SInteger -> SInteger
ld SInteger
2 SInteger
n)) (StepArgs (Forall "n" Integer -> SBool) Bool
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Bool
-> 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
2] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SBool
isPrime (SInteger -> SInteger -> SInteger
ld SInteger
2 SInteger
n)
                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldt Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "k" 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 @"k" SInteger
2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n)
                        TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "k" 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 @"k" SInteger
2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n)
                        Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (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

-- | The least prime divisor is the least divisor of it starting from @2@. By 'leastDivisorIsPrime', this number
-- is guaranteed to be prime.
leastPrimeDivisor :: SInteger -> SInteger
leastPrimeDivisor :: SInteger -> SInteger
leastPrimeDivisor SInteger
n = SInteger -> SInteger -> SInteger
ld SInteger
2 SInteger
n

-- * Formalizing factorial

-- | The factorial function.
fact :: SInteger -> SInteger
fact :: SInteger -> SInteger
fact = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"fact" ((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
1 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

-- | \(n! \geq 1\)
--
-- === __Proof__
-- >>> runTP factAtLeast1
-- Inductive lemma: factAtLeast1
--   Step: Base                            Q.E.D.
--   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.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] factAtLeast1 :: Ɐn ∷ Integer → Bool
factAtLeast1 :: TP (Proof (Forall "n" Integer -> SBool))
factAtLeast1 :: TP (Proof (Forall "n" Integer -> SBool))
factAtLeast1 = 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
"factAtLeast1"
                      (\(Forall SInteger
n) -> SInteger -> SInteger
fact SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 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 -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
1
                                  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
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 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
IHArg (Forall "n" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 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
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)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 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
                                           ]

-- | \(1 \leq k \land k \leq n \implies k \mid n!\)
--
-- === __Proof__
-- >>> runTP dividesFact
-- Lemma: dividesProduct                   Q.E.D.
-- Inductive lemma: dividesFact
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2 (2 way case split)
--     Step: 2.1.1                         Q.E.D.
--     Step: 2.1.2                         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] dividesFact :: Ɐn ∷ Integer → Ɐk ∷ Integer → Bool
dividesFact :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
dividesFact :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
dividesFact = do
   Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dvp <- String
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dividesProduct" TP
  (Proof
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool))
dividesProduct

   String
-> (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> (Proof
      (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer -> Forall "k" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> Forall "k" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> (Proof
      (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> Forall "k" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> Forall "k" 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
"dividesFact"
          (\(Forall SInteger
n) (Forall SInteger
k) -> SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.=> SInteger
k SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger
fact SInteger
n) ((Proof
    (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
  -> IStepArgs
       (Forall "n" Integer -> Forall "k" Integer -> SBool) Bool)
 -> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)))
-> (Proof
      (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer -> Forall "k" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
ih IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger
k -> [SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1]
                  [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
k SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger
fact (SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger -> 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
=: SInteger
k SInteger -> SInteger -> SBool
`dvd` ((SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n 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 -> Forall "k" Integer -> SBool)
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 [ SInteger
k SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
k SInteger -> SInteger -> SBool
`dvd` ((SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n 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 -> Forall "k" Integer -> SBool)
n)
                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dvp Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> IArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" 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
k, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" (SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"z" (SInteger -> SInteger
fact SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n))
                                          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
                           , SInteger
k SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
k SInteger -> SInteger -> SBool
`dvd` ((SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n 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 -> Forall "k" Integer -> SBool)
n)
                                          SBool -> Proof (Forall "k" Integer -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
Proof (Forall "k" Integer -> SBool)
ih
                                          TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
dvp Proof
  (Forall "x" Integer
   -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> IArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" 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
k, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" (SInteger -> SInteger
fact SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"z" (SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                                          Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (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
                           ]

-- | \(1 \leq k \land k \leq n \implies \neg (k \mid n! + 1)\)
--
-- === __Proof__
-- >>> runTP notDividesFactP1
-- Lemma: dividesFact                      Q.E.D.
-- Lemma: notDividesFactP1
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] notDividesFactP1 :: Ɐn ∷ Integer → Ɐk ∷ Integer → Bool
notDividesFactP1 :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
notDividesFactP1 :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
notDividesFactP1 = do
   Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
df    <- String
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dividesFact"  TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
dividesFact

   String
-> (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> StepArgs
     (Forall "n" Integer -> Forall "k" Integer -> SBool) Bool
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> Forall "k" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> Forall "k" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"notDividesFactP1"
         (\(Forall SInteger
n) (Forall SInteger
k) -> SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
k SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SInteger
k SInteger -> SInteger -> SBool
`dvd` (SInteger -> SInteger
fact SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1))) (StepArgs (Forall "n" Integer -> Forall "k" Integer -> SBool) Bool
 -> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)))
-> StepArgs
     (Forall "n" Integer -> Forall "k" Integer -> SBool) Bool
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SInteger
n SInteger
k -> [SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
k, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n]
              [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
k SInteger -> SInteger -> SBool
`dvd` (SInteger -> SInteger
fact SInteger
n SInteger -> 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 "n" Integer -> Forall "k" Integer -> SBool)
df Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> IArgs (Forall "n" Integer -> Forall "k" 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, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" SInteger
k)
              TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
k SInteger -> SInteger -> SBool
`dvd` (SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
fact SInteger
n SInteger -> SInteger -> SInteger
`sEDiv` SInteger
k SInteger -> 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
=: SInteger
k SInteger -> SInteger -> SBool
`dvd` SInteger
1
              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

-- * Finding a greater prime

-- | Given a number, return another number which is both prime and is larger than the input. Note that
-- we don't claim to return the closest prime to the input. Just some prime that is larger, as we shall prove.
greaterPrime :: SInteger -> SInteger
greaterPrime :: SInteger -> SInteger
greaterPrime SInteger
n = SInteger -> SInteger
leastPrimeDivisor (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)

-- | \(\mathit{greaterPrime}\, n \mid n! + 1\)
--
-- === __Proof__
-- >>> runTP greaterPrimeDivides
-- Lemma: leastDivisorDivides              Q.E.D.
-- Lemma: factAtLeast1                     Q.E.D.
-- Lemma: greaterPrimeDivides
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] greaterPrimeDivides :: Ɐn ∷ Integer → Bool
greaterPrimeDivides :: TP (Proof (Forall "n" Integer -> SBool))
greaterPrimeDivides :: TP (Proof (Forall "n" Integer -> SBool))
greaterPrimeDivides = do
   Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd  <- String
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
-> TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorDivides" TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))
leastDivisorDivides
   Proof (Forall "n" Integer -> SBool)
fal1 <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"factAtLeast1"        TP (Proof (Forall "n" Integer -> SBool))
factAtLeast1

   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (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)
-> 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
"greaterPrimeDivides"
        (\(Forall SInteger
n) -> SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
`dvd` (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)) (StepArgs (Forall "n" Integer -> SBool) Bool
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Bool
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
n -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
`dvd` (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)
                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
leastPrimeDivisor (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n) SInteger -> SInteger -> SBool
`dvd` (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)
                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
ld SInteger
2 (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n) SInteger -> SInteger -> SBool
`dvd` (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)
                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
ldd  Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "k" 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 @"k" SInteger
2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n))
                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
fal1 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
                 Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (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

-- | \(\mathit{greaterPrime}\, n > n\)
--
-- === __Proof__
-- >>> runTP greaterPrimeGreater
-- Lemma: notDividesFactP1                 Q.E.D.
-- Lemma: greaterPrimeDivides              Q.E.D.
-- Lemma: leastDivisorIsPrime              Q.E.D.
-- Lemma: factAtLeast1                     Q.E.D.
-- Lemma: primeAtLeast2                    Q.E.D.
-- Lemma: greaterPrimeGreater
--   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] greaterPrimeGreater :: Ɐn ∷ Integer → Bool
greaterPrimeGreater :: TP (Proof (Forall "n" Integer -> SBool))
greaterPrimeGreater :: TP (Proof (Forall "n" Integer -> SBool))
greaterPrimeGreater = do
   Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
ndfp1 <- String
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"notDividesFactP1"    TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
notDividesFactP1
   Proof (Forall "n" Integer -> SBool)
gpd   <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"greaterPrimeDivides" TP (Proof (Forall "n" Integer -> SBool))
greaterPrimeDivides
   Proof (Forall "n" Integer -> SBool)
ldp   <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorIsPrime" TP (Proof (Forall "n" Integer -> SBool))
leastDivisorIsPrime
   Proof (Forall "n" Integer -> SBool)
fal1  <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"factAtLeast1"        TP (Proof (Forall "n" Integer -> SBool))
factAtLeast1
   Proof (Forall "p" Integer -> SBool)
pal2  <- String
-> TP (Proof (Forall "p" Integer -> SBool))
-> TP (Proof (Forall "p" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"primeAtLeast2"       TP (Proof (Forall "p" Integer -> SBool))
primeAtLeast2

   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (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)
-> 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
"greaterPrimeGreater"
         (\(Forall SInteger
n) -> SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n) (StepArgs (Forall "n" Integer -> SBool) Bool
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Bool
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SInteger
n -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> SBool
sTrue
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
ndfp1 Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> IArgs (Forall "n" Integer -> Forall "k" 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, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" (SInteger -> SInteger
greaterPrime SInteger
n))
                   TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
gpd   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
                   Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool
sNot (SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger -> SInteger
greaterPrime SInteger
n SBool -> SBool -> SBool
.&& SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n)
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger -> SInteger
greaterPrime SInteger
n SBool -> SBool -> SBool
.|| SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n)
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger -> SInteger
leastPrimeDivisor (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n) SBool -> SBool -> SBool
.|| SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n)
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger -> SInteger
leastPrimeDivisor (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n) SBool -> SBool -> SBool
.|| SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n)
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger -> SInteger -> SInteger
ld SInteger
2 (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n) SBool -> SBool -> SBool
.|| SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n)
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ldp  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
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)
                   TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "p" Integer -> SBool)
pal2 Proof (Forall "p" Integer -> SBool)
-> IArgs (Forall "p" 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 @"p" (SInteger -> SInteger -> SInteger
ld SInteger
2 (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n))
                   Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
fal1 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
                   Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
greaterPrime SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
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

-- * Infinitude of primes

-- | \(\mathit{isPrime}\,(\mathit{greaterPrime}\,n) \land \mathit{greaterPrime}\,n > n\)
--
-- We can finally prove our goal: For each given number, there is a larger number that is prime. This
-- establishes that we have an infinite number of primes.
--
-- === __Proof__
-- >>> runTP infinitudeOfPrimes
-- Lemma: leastDivisorIsPrime              Q.E.D.
-- Lemma: factAtLeast1                     Q.E.D.
-- Lemma: greaterPrimeGreater              Q.E.D.
-- Lemma: infinitudeOfPrimes
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] infinitudeOfPrimes :: Ɐn ∷ Integer → Bool
infinitudeOfPrimes :: TP (Proof (Forall "n" Integer -> SBool))
infinitudeOfPrimes :: TP (Proof (Forall "n" Integer -> SBool))
infinitudeOfPrimes = do
   Proof (Forall "n" Integer -> SBool)
ldp <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"leastDivisorIsPrime" TP (Proof (Forall "n" Integer -> SBool))
leastDivisorIsPrime
   Proof (Forall "n" Integer -> SBool)
fa1 <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"factAtLeast1"        TP (Proof (Forall "n" Integer -> SBool))
factAtLeast1
   Proof (Forall "n" Integer -> SBool)
gpg <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"greaterPrimeGreater" TP (Proof (Forall "n" Integer -> SBool))
greaterPrimeGreater

   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (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)
-> 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
"infinitudeOfPrimes"
         (\(Forall SInteger
n) -> let p :: SInteger
p = SInteger -> SInteger
greaterPrime SInteger
n in SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n SBool -> SBool -> SBool
.&& SInteger -> SBool
isPrime SInteger
p) (StepArgs (Forall "n" Integer -> SBool) Bool
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Bool
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SInteger
n -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- let p :: SInteger
p = SInteger -> SInteger
greaterPrime SInteger
n
                  in SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n SBool -> SBool -> SBool
.&& SInteger -> SBool
isPrime (SInteger -> SInteger
greaterPrime SInteger
n)
                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n SBool -> SBool -> SBool
.&& SInteger -> SBool
isPrime (SInteger -> SInteger
leastPrimeDivisor (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n))
                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n SBool -> SBool -> SBool
.&& SInteger -> SBool
isPrime (SInteger -> SInteger -> SInteger
ld SInteger
2 (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n))
                  SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ldp 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
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fact SInteger
n)
                  TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
fa1 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
                  Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
gpg 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
                  Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (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

-- | \(\forall n. \exists p. \mathit{isPrime}\,p \land p > n\)
--
-- Another expression of the fact that there are infinitely many primes. One might prefer this
-- version as it only refers to the 'isPrime' predicate only.
--
-- === __Proof__
-- >>> runTP noLargestPrime
-- Lemma: infinitudeOfPrimes               Q.E.D.
-- Lemma: noLargestPrime
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] noLargestPrime :: Ɐn ∷ Integer → Bool
noLargestPrime :: TP (Proof (Forall "n" Integer -> SBool))
noLargestPrime :: TP (Proof (Forall "n" Integer -> SBool))
noLargestPrime = do
   Proof (Forall "n" Integer -> SBool)
iop <- String
-> TP (Proof (Forall "n" Integer -> SBool))
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"infinitudeOfPrimes" TP (Proof (Forall "n" Integer -> SBool))
infinitudeOfPrimes

   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (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)
-> 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
"noLargestPrime"
        (\(Forall SInteger
n) -> (Exists Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Exists SInteger
p) -> SInteger -> SBool
isPrime SInteger
p SBool -> SBool -> SBool
.&& SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n)) (StepArgs (Forall "n" Integer -> SBool) Bool
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Bool
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
n -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (Exists Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Exists SInteger
p) -> SInteger -> SBool
isPrime SInteger
p SBool -> SBool -> SBool
.&& SInteger
p SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
n)
                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
iop 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 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

{- HLint ignore module "Avoid lambda" -}
{- HLint ignore module "Eta reduce"   -}