-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.GCD
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- We define three different versions of the GCD algorithm: (1) Regular
-- version using the modulus operator, (2) the more basic version using
-- subtraction, and (3) the so called binary GCD. We prove that the modulus
-- based algorithm correct, i.e., that it calculates the greatest-common-divisor
-- of its arguments. We then prove that the other two variants are equivalent
-- to this version, thus establishing their correctness as well.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.GCD where

import Prelude hiding (gcd)

import Data.SBV
import Data.SBV.TP
import Data.SBV.Tuple

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

-- * Calculating GCD

-- | @nGCD@ is the version of GCD that works on non-negative integers.
--
-- Ideally, we should make this function local to @gcd@, but then we can't refer to it explicitly in our proofs.
--
-- Note on maximality: Note that, by definition @gcd 0 0 = 0@. Since any number divides @0@,
-- there is no greatest common divisor for the pair @(0, 0)@. So, maximality here is meant
-- to be in terms of divisibility. That is, any divisor of @a@ and @b@ will also divide their @gcd@.
nGCD :: SInteger -> SInteger -> SInteger
nGCD :: SInteger -> SInteger -> SInteger
nGCD = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"nGCD" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
a SInteger
b -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
a (SInteger -> SInteger -> SInteger
nGCD SInteger
b (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b))

-- | Generalized GCD, working for all integers. We simply call @nGCD@ with the absolute value of the arguments.
gcd :: SInteger -> SInteger -> SInteger
gcd :: SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b = SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)

-- * Basic properties

-- | \(\gcd\, a\ b \geq 0\)
--
-- ==== __Proof__
-- >>> runTP gcdNonNegative
-- Inductive lemma (strong): nonNegativeNGCD
--   Step: Measure is non-negative         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.
-- Lemma: nonNegative                      Q.E.D.
-- [Proven] nonNegative :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdNonNegative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdNonNegative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdNonNegative = do
     -- We first prove over nGCD, using strong induction with the measure @a+b@.
     Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nn <- String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" Integer -> Forall "b" 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 "a" Integer -> Forall "b" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
sInduct String
"nonNegativeNGCD"
                   (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)
                   (\SInteger
_a SInteger
b -> SInteger
b, []) ((Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
b 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
b 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
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
b (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b))
                                               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 "a" Integer -> Forall "b" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"nonNegative"
           (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)
           [Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nn]

-- | \(\gcd\, a\ b=0\implies a=0\land b=0\)
--
-- ==== __Proof__
-- >>> runTP gcdZero
-- Inductive lemma (strong): nGCDZero
--   Step: Measure is non-negative         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.
-- Lemma: gcdZero                          Q.E.D.
-- [Proven] gcdZero :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdZero :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdZero :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdZero = do

  -- First prove over nGCD:
  Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nGCDZero <-
    String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" Integer -> Forall "b" 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 "a" Integer -> Forall "b" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
sInduct String
"nGCDZero"
            (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.=> SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)
            (\SInteger
_a SInteger
b -> SInteger
b, []) ((Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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 -> SInteger -> SInteger
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.=> SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)
                    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
b 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
b 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 -> SInteger -> SInteger
nGCD SInteger
b (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.=> SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)
                                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b))
                                        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 "a" Integer -> Forall "b" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"gcdZero"
        (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.=> SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) 
        [Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nGCDZero]

-- | \(\gcd\, a\ b=\gcd\, b\ a\)
--
-- ==== __Proof__
-- >>> runTP commutative
-- Lemma: nGCDCommutative
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: commutative
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] commutative :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
commutative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
commutative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
commutative = do
    -- First prove over nGCD. Simple enough proof, but quantifiers and recursive functions
    -- cause z3 to diverge. So, we have to explicitly write it out.
    Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nGCDComm <-
        String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"nGCDCommutative"
             (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
nGCD SInteger
b SInteger
a) (StepArgs
   (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
             \SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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 -> SInteger
nGCD SInteger
a SInteger
b
                  SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
b SInteger
a
                  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

    -- It's unfortunate we have to spell this out explicitly, a simple lemma call
    -- that uses the above proof doesn't converge.
    String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"commutative"
          (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
b SInteger
a) (StepArgs
   (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \SInteger
a SInteger
b -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
                     SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                     SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nGCDComm Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b))
                     TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
gcd SInteger
b SInteger
a
                     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

-- | \(\gcd\,(-a)\,b = \gcd\,a\,b = \gcd\,a\,(-b)\)
--
-- ==== __Proof__
-- >>> runTP negGCD
-- Lemma: negGCD                           Q.E.D.
-- [Proven] negGCD :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
negGCD :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
negGCD :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
negGCD = String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"negGCD" (\(Forall SInteger
a) (Forall SInteger
b) -> let g :: SInteger
g = SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b in SInteger -> SInteger -> SInteger
gcd (-SInteger
a) SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
g SBool -> SBool -> SBool
.&& SInteger
g SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
a (-SInteger
b)) []

-- | \( \gcd\,a\,0 = \gcd\,0\,a = |a| \land \gcd\,0\,0 = 0\)
--
-- ==== __Proof__
-- >>> runTP zeroGCD
-- Lemma: negGCD                           Q.E.D.
-- [Proven] negGCD :: Ɐa ∷ Integer → Bool
zeroGCD :: TP (Proof (Forall "a" Integer -> SBool))
zeroGCD :: TP (Proof (Forall "a" Integer -> SBool))
zeroGCD = String
-> (Forall "a" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"negGCD" (\(Forall SInteger
a) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
0 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
0 SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
gcd SInteger
0 SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
gcd SInteger
0 SInteger
0 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) []

-- * Even and odd

-- | Is the given integer even?
isEven :: SInteger -> SBool
isEven :: SInteger -> SBool
isEven = (Integer
2 Integer -> SInteger -> SBool
`sDivides`)

-- | Is the given integer odd?
isOdd :: SInteger -> SBool
isOdd :: SInteger -> SBool
isOdd  = SBool -> SBool
sNot (SBool -> SBool) -> (SInteger -> SBool) -> SInteger -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger -> SBool
isEven

-- * Divisibility

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

-- | \(a \mid |b| \iff a \mid b\)
--
-- A number divides another exactly when it also divides its absolute value. While this property
-- seems obvious, I was unable to get z3 to prove it. Even CVC5 needs a bit of help to guide it through
-- the case split on @b@.
--
-- ==== __Proof__
-- >>> runTP dvdAbs
-- Lemma: dvdAbs_l2r
--   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.
-- Lemma: dvdAbs_r2l
--   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.
-- Lemma: dvdAbs                           Q.E.D.
-- [Proven] dvdAbs :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
dvdAbs :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdAbs :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdAbs = do
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
l2r <- SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcWith SMTConfig
cvc5 String
"dvdAbs_l2r"
                   (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b SBool -> SBool -> SBool
.=> SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger
b) (StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b]
                        [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
b 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)
==> 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
b 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)
==> SBool
sTrue SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                 ]

   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
r2l <- SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcWith SMTConfig
cvc5 String
"dvdAbs_r2l"
                   (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b) (StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger
b]
                        [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
b 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)
==> 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
b 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)
==> 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 "a" Integer -> Forall "b" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"dvdAbs"
         (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
a SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
         [Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
l2r, Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
r2l]

-- | \(d \mid a \implies d \mid ka\)
--
-- ==== __Proof__
-- >>> runTP dvdMul
-- Lemma: dvdMul
--   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] dvdMul :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐk ∷ Integer → Bool
dvdMul :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "k" Integer -> SBool))
dvdMul :: TP
  (Proof
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "k" Integer -> SBool))
dvdMul = String
-> (Forall "d" Integer
    -> Forall "a" Integer -> Forall "k" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "k" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "k" Integer -> SBool))
forall t.
(Proposition
   (Forall "d" Integer
    -> Forall "a" Integer -> Forall "k" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "d" Integer
    -> Forall "a" Integer -> Forall "k" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "k" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" 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
"dvdMul"
              (\(Forall SInteger
d) (Forall SInteger
a) (Forall SInteger
k) -> SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.=> SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a)) (StepArgs
   (Forall "d" Integer
    -> Forall "a" Integer -> Forall "k" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "d" Integer
          -> Forall "a" Integer -> Forall "k" Integer -> SBool)))
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "k" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "k" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
              \SInteger
d SInteger
a SInteger
k -> [SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a]
                     [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
d 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
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a)
                                         SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
a 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
d 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
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a)
                                         SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                         TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` 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
                              ]

-- | \(d \mid (2a + 1) \implies \mathrm{isOdd}(d)\)
--
-- ==== __Proof__
-- >>> runTP dvdOddThenOdd
-- Lemma: dvdOddThenOdd
--   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] dvdOddThenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool
dvdOddThenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdOddThenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdOddThenOdd = String
-> (Forall "d" Integer -> Forall "a" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer -> Forall "a" Integer -> SBool) Bool
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall t.
(Proposition (Forall "d" Integer -> Forall "a" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "d" Integer -> Forall "a" Integer -> SBool)
-> StepArgs (Forall "d" Integer -> Forall "a" Integer -> SBool) t
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"dvdOddThenOdd"
                     (\(Forall SInteger
d) (Forall SInteger
a) -> SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SBool -> SBool -> SBool
.=> SInteger -> SBool
isOdd SInteger
d) (StepArgs (Forall "d" Integer -> Forall "a" Integer -> SBool) Bool
 -> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)))
-> StepArgs
     (Forall "d" Integer -> Forall "a" Integer -> SBool) Bool
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                     \SInteger
d SInteger
a -> [SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> 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)
|- [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger -> SBool
isOdd  SInteger
d SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                                   , SInteger -> SBool
isEven SInteger
d SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
d SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2)) SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> 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
2 SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> 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
=: ChainsTo SBool
TPProofRaw SBool
forall a. Contradiction a => a
contradiction
                                   ]

-- | \(\mathrm{isOdd}(d) \land d \mid 2a \implies d \mid a\)
--
-- ==== __Proof__
-- >>> runTP dvdEvenWhenOdd
-- Lemma: dvdEvenWhenOdd
--   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] dvdEvenWhenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool
dvdEvenWhenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdEvenWhenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdEvenWhenOdd = String
-> (Forall "d" Integer -> Forall "a" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer -> Forall "a" Integer -> SBool) Bool
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall t.
(Proposition (Forall "d" Integer -> Forall "a" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "d" Integer -> Forall "a" Integer -> SBool)
-> StepArgs (Forall "d" Integer -> Forall "a" Integer -> SBool) t
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"dvdEvenWhenOdd"
                      (\(Forall SInteger
d) (Forall SInteger
a) -> SInteger -> SBool
isOdd SInteger
d SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a) SBool -> SBool -> SBool
.=> SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a) (StepArgs (Forall "d" Integer -> Forall "a" Integer -> SBool) Bool
 -> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)))
-> StepArgs
     (Forall "d" Integer -> Forall "a" Integer -> SBool) Bool
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                      \SInteger
d SInteger
a ->  [SInteger -> SBool
isOdd SInteger
d, SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a)]
                           [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|-  let t :: SInteger
t = (SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                                   m :: SInteger
m = (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a)   SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                            in SBool
sTrue

                            -- Observe that d = 2t+1 and 2a = dm
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
t SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1 SBool -> SBool -> SBool
.&& SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
dSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
m

                            -- So, 2a == (2t+1)m holds
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
tSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
m

                            -- Arithmetic gives us
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
tSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
m SBool -> SBool -> SBool
.&& SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
tSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
m) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
m

                            -- So, we now now m is even
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger
m

                            -- Give that divisor a name:
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let n :: SInteger
n = SInteger
m SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2

                            -- It follows that 2a = d(2n) = 2(dn)
                            in SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n) SBool -> SBool -> SBool
.&& SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n)

                            -- From which we can conclude a = dn
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n

                            -- Thus we can deduce d must divide a
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a

                            -- Done!
                            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

-- | \(d \mid a \land d \mid b \implies d \mid (a + b)\)
--
-- ==== __Proof__
-- >>> runTP dvdSum1
-- Lemma: dvdSum1
--   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] dvdSum1 :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
dvdSum1 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum1 :: TP
  (Proof
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum1 =
  String
-> (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition
   (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"dvdSum1"
       (\(Forall SInteger
d) (Forall SInteger
a) (Forall SInteger
b) -> SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b)) (StepArgs
   (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "d" Integer
          -> Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SInteger
d SInteger
a SInteger
b -> [SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
b]
              [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
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.|| SInteger
b 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
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b 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
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b)
                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d)
                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d))
                                              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
                       ]

-- | \(d \mid (a + b) \land d \mid b \implies d \mid a \)
--
-- ==== __Proof__
-- >>> runTP dvdSum2
-- Lemma: dvdSum2
--   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] dvdSum2 :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
dvdSum2 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum2 :: TP
  (Proof
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum2 =
  String
-> (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition
   (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"dvdSum2"
       (\(Forall SInteger
d) (Forall SInteger
a) (Forall SInteger
b) -> SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b) SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
a) (StepArgs
   (Forall "d" Integer
    -> Forall "a" Integer -> Forall "b" Integer -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "d" Integer
          -> Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SInteger
d SInteger
a SInteger
b -> [SInteger
d SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b) SBool -> SBool -> SBool
.&& SInteger
d SInteger -> SInteger -> SBool
`dvd` SInteger
b]
              [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                       , SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let k1 :: SInteger
k1 = (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                         k2 :: SInteger
k2 =      SInteger
b  SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                     in SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                     SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                     SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
k1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
k2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                     SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
k1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
k2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d SInteger -> SInteger -> SInteger
`sEDiv` SInteger
d
                                     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
                       ]

-- * Correctness of GCD

-- | \(\gcd\,a\,b \mid a \land \gcd\,a\,b \mid b\)
--
-- GCD of two numbers divide these numbers. This is part one of the proof, where we are
-- not concerned with maximality. Our goal is to show that the calculated gcd divides both inputs.
--
-- ==== __Proof__
-- >>> runTP gcdDivides
-- Lemma: dvdAbs                           Q.E.D.
-- Lemma: helper
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma (strong): dvdNGCD
--   Step: Measure is non-negative         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.
-- Lemma: gcdDivides                       Q.E.D.
-- [Proven] gcdDivides :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdDivides :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdDivides :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdDivides = do

   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdAbs" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdAbs

   -- Helper about divisibility. If x|b and x| a%b, then x|a.
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
helper <- String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"helper"
                  (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) (Forall @"x" SInteger
x) ->
                           SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b)
                       SBool -> SBool -> SBool
.=> -----------------------------------------------
                                       SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a
                  ) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \SInteger
a SInteger
b SInteger
x -> [SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0, SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b, SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b)]
                         [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a
                         SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
b) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
x) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b) 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

   -- Use strong induction to prove divisibility over non-negative numbers.
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dNGCD <- String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" Integer -> Forall "b" 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 "a" Integer -> Forall "b" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
sInduct String
"dvdNGCD"
                     (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b SInteger -> SInteger -> SBool
`dvd` SInteger
b)
                     (\SInteger
_a SInteger
b -> SInteger
b, []) ((Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                     \Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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)
|- let g :: SInteger
g = SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                             in SInteger
g SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
g SInteger -> SInteger -> SBool
`dvd` SInteger
b
                             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
b 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
b 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)
==> let g' :: SInteger
g' = SInteger -> SInteger -> SInteger
nGCD SInteger
b (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b)
                                                 in SInteger
g' SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
g' SInteger -> SInteger -> SBool
`dvd` SInteger
b
                                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b))
                                                 TPProofRaw SBool
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
helper
                                                 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
                                      ]

   -- Now generalize to arbitrary integers.
   String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemmaString
"gcdDivides"
        (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
`dvd` SInteger
b)
        [Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs, Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dNGCD]

-- | \(x \mid a \land x \mid b \implies x \mid \gcd\,a\,b\)
--
-- Maximality. Any divisor of the inputs divides the GCD.
--
-- ==== __Proof__
-- >>> runTP gcdMaximal
-- Lemma: dvdAbs                           Q.E.D.
-- Lemma: gcdComm                          Q.E.D.
-- Lemma: eDiv                             Q.E.D.
-- Lemma: helper
--   Step: 1 (x `dvd` a && x `dvd` b)      Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma (strong): mNGCD
--   Step: Measure is non-negative         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.
-- Lemma: gcdMaximal
--   Step: 1 (2 way case split)
--     Step: 1.1.1                         Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.2.4                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] gcdMaximal :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐx ∷ Integer → Bool
gcdMaximal :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdMaximal :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdMaximal = do

   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdAbs" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdAbs
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdComm" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
commutative

   Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
eDiv <- String
-> (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"eDiv"
                 (\(Forall @"x" SInteger
x) (Forall @"y" SInteger
y) -> SInteger
y 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
x SInteger -> SInteger -> SInteger
`sEDiv` SInteger
y) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
x SInteger -> SInteger -> SInteger
`sEMod` SInteger
y)
                 []

   -- Helper: If x|a, x|b then x|a%b.
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
helper <- String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"helper"
                  (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) (Forall @"x" SInteger
x) ->
                           SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b
                       SBool -> SBool -> SBool
.=> -----------------------------------------------
                                     SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b)
                  ) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \SInteger
a SInteger
b SInteger
x -> [SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0, SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0, SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a, SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b]
                         [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
`dvd` (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b)
                         SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"x `dvd` a && x `dvd` b"
                         TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let k1 :: SInteger
k1 = SInteger
a SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
x
                                k2 :: SInteger
k2 = SInteger
b SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
x
                         in SInteger
x SInteger -> SInteger -> SBool
`dvd` ((SInteger
k1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x) SInteger -> SInteger -> SInteger
`sEMod` (SInteger
k2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x))
                         SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
eDiv Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> IArgs (Forall "x" Integer -> Forall "y" 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
k1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" (SInteger
k2SInteger -> 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
k1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- ((SInteger
k1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x) SInteger -> SInteger -> SInteger
`sEDiv` (SInteger
k2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x)) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
k2SInteger -> 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

   -- Now prove maximality for non-negative integers:
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
mNGCD <- String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer
       -> Forall "b" Integer -> Forall "x" Integer -> SBool)
      Integer,
    [ProofObj])
-> (Proof
      (Forall "a" Integer
       -> Forall "b" Integer -> Forall "x" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" 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 "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer
       -> Forall "b" Integer -> Forall "x" Integer -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "a" Integer
       -> Forall "b" Integer -> Forall "x" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
sInduct String
"mNGCD"
                    (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) (Forall @"x" SInteger
x) ->
                          SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b)
                    (\SInteger
_a SInteger
b SInteger
_x -> SInteger
b, []) ((Proof
    (Forall "a" Integer
     -> Forall "b" Integer -> Forall "x" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "x" Integer -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)))
-> (Proof
      (Forall "a" Integer
       -> Forall "b" Integer -> Forall "x" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
ih SInteger
a SInteger
b SInteger
x -> let g :: SInteger
g = SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                              in [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b]
                              [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
g
                              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
b 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
b 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
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
nGCD SInteger
b (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b)
                                                  SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
ih Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                                  TPProofRaw SBool
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
helper
                                                  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
                                                  ]

   -- Generalize to arbitrary integers:
   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"gcdMaximal"
        (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) (Forall @"x" SInteger
x) -> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
a SInteger
b SInteger
x -> [SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a, SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b]
               [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
               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 -> SInteger
forall a. Num a => a -> a
abs SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                                           SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
mNGCD    Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                           TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs     Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
a)
                                           Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs     Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                                           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
                        , SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
                                           SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                                           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 -> SInteger -> SInteger
gcd SInteger
b SInteger
a
                                           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a)
                                           SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
mNGCD    Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                           TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs     Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
a)
                                           Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
dAbs     Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                                           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
                        ]

-- | \(\gcd\,a\,b \mid a \land \gcd\,a\,b \mid b \land (x \mid a \land x \mid b \implies x \mid \gcd\,a\,b)\)
--
-- Putting it all together: GCD divides both arguments, and its maximal.
--
-- ==== __Proof__
-- >>> runTP gcdCorrect
-- Lemma: gcdDivides                       Q.E.D.
-- Lemma: gcdMaximal                       Q.E.D.
-- Lemma: gcdCorrect
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] gcdCorrect :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdCorrect :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdCorrect :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdCorrect = do
  Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdDivides" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdDivides
  Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
maximal <- String
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdMaximal" TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdMaximal

  String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"gcdCorrect"
       (\(Forall SInteger
a) (Forall SInteger
b) ->
             let g :: SInteger
g = SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
          in  SInteger
g SInteger -> SInteger -> SBool
`dvd` SInteger
a
          SBool -> SBool -> SBool
.&& SInteger
g SInteger -> SInteger -> SBool
`dvd` SInteger
b
          SBool -> SBool -> SBool
.&& (Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SInteger
x) -> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
g)
       ) (StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SInteger
a SInteger
b -> []
            [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- let g :: SInteger
g = SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
                   m :: SBool
m = (Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SInteger
x) -> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
g)
            in SInteger
g SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
g SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.&& SBool
m
            SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
            TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
m
            SBool
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
maximal
            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

-- | \(\bigl((a \neq 0 \lor b \neq 0) \land x \mid a \land x \mid b \bigr) \implies x \leq \gcd\,a\,b\)
--
-- Additionally prove that GCD is really maximum, i.e., it is the largest in the regular sense. Note
-- that we have to make an exception for @gcd 0 0@ since by definition the GCD is @0@, which is clearly
-- not the largest divisor of @0@ and @0@. (Since any number is a GCD for the pair @(0, 0)@, there is
-- no maximum.)
--
-- ==== __Proof__
-- >>> runTP gcdLargest
-- Lemma: gcdMaximal                       Q.E.D.
-- Lemma: gcdZero                          Q.E.D.
-- Lemma: gcdNonNegative                   Q.E.D.
-- Lemma: gcdLargest
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] gcdLargest :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐx ∷ Integer → Bool
gcdLargest :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdLargest :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdLargest = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
maximal <- String
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdMaximal"     TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdMaximal
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
zero    <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdZero"        TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdZero
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nn      <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdNonNegative" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdNonNegative

   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"gcdLargest"
        (\(Forall SInteger
a) (Forall SInteger
b) (Forall SInteger
x) -> (SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.|| SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0) SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "x" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "x" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
a SInteger
b SInteger
x -> [(SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.|| SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0) SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
a, SInteger
x SInteger -> SInteger -> SBool
`dvd` SInteger
b]
               [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
maximal Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" 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 -> SInteger -> SInteger
gcd SInteger
a SInteger
b SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b)
               SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
zero  Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
               TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nn    Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
               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

-- * Other GCD Facts

-- | \(\gcd\, a\, b = \gcd\, (a + b)\, b\)
--
-- ==== __Proof__
-- >>> runTP gcdAdd
-- Lemma: dvdSum1                          Q.E.D.
-- Lemma: dvdSum2                          Q.E.D.
-- Lemma: gcdDivides                       Q.E.D.
-- Lemma: gcdLargest                       Q.E.D.
-- Lemma: gcdAdd
--   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] gcdAdd :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdAdd :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdAdd :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdAdd = do

   Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "b" Integer -> SBool)
dSum1   <- String
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdSum1"    TP
  (Proof
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum1
   Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "b" Integer -> SBool)
dSum2   <- String
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdSum2"    TP
  (Proof
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum2
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdDivides" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdDivides
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
largest <- String
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdLargest" TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdLargest

   String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"gcdAdd"
        (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b) SInteger
b) (StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
a SInteger
b -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let g1 :: SInteger
g1 = SInteger -> SInteger -> SInteger
gcd SInteger
a       SInteger
b
                           g2 :: SInteger
g2 = SInteger -> SInteger -> SInteger
gcd (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b) SInteger
b
                    in SBool
sTrue

                    -- First use the divides property to conclude that g1 divides a and b
                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                    TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
`dvd` SInteger
a SBool -> SBool -> SBool
.&& SInteger
g1 SInteger -> SInteger -> SBool
`dvd` SInteger
b

                    -- Same for g2 for a+b and b
                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                    TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g2 SInteger -> SInteger -> SBool
`dvd` (SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
b) SBool -> SBool -> SBool
.&& SInteger
g2 SInteger -> SInteger -> SBool
`dvd` SInteger
b

                    -- Use dSum1 to show g1 divides a+b
                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "b" Integer -> SBool)
dSum1 Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" 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 @"d" SInteger
g1, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                    TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
`dvd` (SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
b)

                    -- Similarly, use dSum2 to show g2 divides a
                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "b" Integer -> SBool)
dSum2 Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "b" 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 @"d" SInteger
g2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                    TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=:  SInteger
g2 SInteger -> SInteger -> SBool
`dvd` SInteger
a

                    -- Now use largest to show g1 >= g2
                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
largest Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" SInteger
a,     forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
g2)
                    TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
g2

                    -- But again via largest, we can show g2 >= g1
                    SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
largest Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" (SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
g1)
                    TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
g1

                    -- Finally conclude g1 = g2, since both are greater-than-equal to each other:
                    SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
g2
                    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

-- | \(\gcd\, (2a)\, (2b) = 2 (\gcd\,a\, b)\)
--
-- ==== __Proof__
-- >>> runTP gcdEvenEven
-- Lemma: modEE                            Q.E.D.
-- Inductive lemma (strong): nGCDEvenEven
--   Step: Measure is non-negative         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.2.3                         Q.E.D.
--     Step: 1.2.4                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: gcdEvenEven
--   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] gcdEvenEven :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdEvenEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdEvenEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdEvenEven = do

   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
modEE <- String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"modEE"
                  (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.=> (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a) SInteger -> SInteger -> SInteger
`sEMod` (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b))
                  []

   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nGCDEvenEven <- String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
-> TP (Proof (Forall "a" Integer -> Forall "b" 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 "a" Integer -> Forall "b" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
sInduct String
"nGCDEvenEven"
                           (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
nGCD (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a) (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b)
                           (\SInteger
_a SInteger
b -> SInteger
b, []) ((Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                           \Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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 -> SInteger
nGCD (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a) (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b)
                                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                            , SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCD (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a) (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b)
                                                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b) ((SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a) SInteger -> SInteger -> SInteger
`sEMod` (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b))
                                                       SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
modEE Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                                                       TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b) (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
a SInteger -> SInteger -> SInteger
`sEMod` SInteger
b))
                                                       SInteger
-> Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih
                                                       TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                       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 "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"gcdEvenEven"
        (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a) (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b) (StepArgs
   (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
a SInteger
b -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
gcd (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a) (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b)
                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
a)) (SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b))
                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                   SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nGCDEvenEven Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b))
                   TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
                   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

-- | \(\gcd\, (2a+1)\, (2b) = \gcd\,(2a+1)\, b\)
--
-- ==== __Proof__
-- >>> runTP gcdOddEven
-- Lemma: gcdDivides                       Q.E.D.
-- Lemma: gcdLargest                       Q.E.D.
-- Lemma: dvdMul                           Q.E.D.
-- Lemma: dvdOddThenOdd                    Q.E.D.
-- Lemma: dvdEvenWhenOdd                   Q.E.D.
-- Lemma: gcdOddEven
--   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] gcdOddEven :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdOddEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdOddEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdOddEven = do

   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides      <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdDivides"     TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdDivides
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
largest      <- String
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "x" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdLargest"     TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdLargest
   Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "k" Integer -> SBool)
dMul         <- String
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "k" Integer -> SBool))
-> TP
     (Proof
        (Forall "d" Integer
         -> Forall "a" Integer -> Forall "k" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdMul"         TP
  (Proof
     (Forall "d" Integer
      -> Forall "a" Integer -> Forall "k" Integer -> SBool))
dvdMul
   Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)
dOddThenOdd  <- String
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdOddThenOdd"  TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdOddThenOdd
   Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)
dEvenWhenOdd <- String
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
-> TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"dvdEvenWhenOdd" TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdEvenWhenOdd

   String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"gcdOddEven"
        (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
b) (StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Bool
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SInteger
a SInteger
b -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
|-> let g1 :: SInteger
g1 = SInteger -> SInteger -> SInteger
gcd (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b)
                           g2 :: SInteger
g2 = SInteger -> SInteger -> SInteger
gcd (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
b
                   in SBool
sTrue

                   -- First use the divides property to conclude that g1 divides both 2*a+1 and 2*b
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b))
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SBool -> SBool -> SBool
.&& SInteger
g1 SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b)

                   -- Same for g2, for 2*a+1 and b
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
divides Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g2 SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SBool -> SBool -> SBool
.&& SInteger
g2 SInteger -> SInteger -> SBool
`dvd` SInteger
b

                   -- By arithmetic, g2 divides 2*b
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "k" Integer -> SBool)
dMul Proof
  (Forall "d" Integer
   -> Forall "a" Integer -> Forall "k" Integer -> SBool)
-> IArgs
     (Forall "d" Integer
      -> Forall "a" 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 @"d" SInteger
g2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" SInteger
2)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g2 SInteger -> SInteger -> SBool
`dvd` (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b)

                   -- Observe that g1 must be odd
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)
dOddThenOdd Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)
-> IArgs (Forall "d" Integer -> Forall "a" 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 @"d" SInteger
g1, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
a)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SBool
isOdd SInteger
g1

                   -- Conclude that g1 must divide b
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)
dEvenWhenOdd Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)
-> IArgs (Forall "d" Integer -> Forall "a" 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 @"d" SInteger
g1, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
b)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
`dvd` SInteger
b

                   -- Now use largest to show g1 >= g2
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
largest Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1),  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
g2)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
g2

                   -- But again via largest, we can show g2 >= g1
                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
largest Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "x" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "x" 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 @"a" (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
g1)
                   TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
g1

                   -- Finally conclude g1 = g2 since both are greater-than-equal to each other:
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
g1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
g2
                   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

-- * GCD via subtraction

-- | @nGCDSub@ is the original verision of Euclid, which uses subtraction instead of modulus. This is the version that
-- works on non-negative numbers. It has the precondition that @a >= b >= 0@, and maintains this invariant in each
-- recursive call.
nGCDSub :: SInteger -> SInteger -> SInteger
nGCDSub :: SInteger -> SInteger -> SInteger
nGCDSub = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"nGCDSub" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
a SInteger
b -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
b) SInteger
a
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
b
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
a
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
b)  (SInteger -> SInteger -> SInteger
nGCDSub (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b) SInteger
b)
                                                        (SInteger -> SInteger -> SInteger
nGCDSub SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a))

-- | Generalized version of subtraction based GCD, working over all integers.
gcdSub :: SInteger -> SInteger -> SInteger
gcdSub :: SInteger -> SInteger -> SInteger
gcdSub SInteger
a SInteger
b = SInteger -> SInteger -> SInteger
nGCDSub (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)

-- | \(\mathrm{gcdSub}\, a\, b = \gcd\, a\, b\)
--
-- Instead of proving @gcdSub@ correct, we'll simply show that it is equivalent to @gcd@, hence it has
-- all the properties we already established.
--
-- ==== __Proof__
-- >>> runTP gcdSubEquiv
-- Lemma: commutative                      Q.E.D.
-- Lemma: gcdAdd                           Q.E.D.
-- Inductive lemma (strong): nGCDSubEquiv
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (5 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.3                           Q.E.D.
--     Step: 1.4.1                         Q.E.D.
--     Step: 1.4.2                         Q.E.D.
--     Step: 1.4.3                         Q.E.D.
--     Step: 1.5.1                         Q.E.D.
--     Step: 1.5.2                         Q.E.D.
--     Step: 1.5.3                         Q.E.D.
--     Step: 1.5.4                         Q.E.D.
--     Step: 1.5.5                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: gcdSubEquiv
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] gcdSubEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdSubEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdSubEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdSubEquiv = do

   -- We'll be using the commutativity of GCD and the gcdAdd property
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"commutative" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
commutative
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
addG <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdAdd"      TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdAdd

   -- First prove over the non-negative numbers:
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nEq <- String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
-> TP (Proof (Forall "a" Integer -> Forall "b" 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 "a" Integer -> Forall "b" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
sInduct String
"nGCDSubEquiv"
                  (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
nGCDSub SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b)
                  (\SInteger
a SInteger
b -> SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
b, []) ((Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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 -> SInteger
nGCDSub SInteger
a SInteger
b
                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
b             SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b 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
                                   , SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0             SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b 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
                                   , SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0             SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b 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
                                   , SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
b  SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCDSub (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b) SInteger
b
                                                          SInteger
-> Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih
                                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b) SInteger
b
                                                          SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
addG Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                          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
                                   , SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
b  SBool -> SBool -> SBool
.&& SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCDSub SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a)
                                                          SInteger
-> Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih
                                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a)
                                                          SInteger
-> Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm
                                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a) SInteger
a
                                                          SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
addG Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
a)
                                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
b SInteger
a
                                                          SInteger
-> Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm
                                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                          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
                                   ]

   -- Now prove over all integers
   SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcWith SMTConfig
cvc5 String
"gcdSubEquiv"
         (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcdSub SInteger
a SInteger
b) (StepArgs
   (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SInteger
a SInteger
b -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
                    SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                    SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nEq Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b))
                    TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCDSub (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                    SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
gcdSub SInteger
a SInteger
b
                    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

-- * Binary GCD

-- | @nGCDBin@ is the binary GCD algorithm that works on non-negative numbers.
nGCDBin :: SInteger -> SInteger -> SInteger
nGCDBin :: SInteger -> SInteger -> SInteger
nGCDBin = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"nGCDBin" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
a SInteger
b -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)               SInteger
b
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)               SInteger
a
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger -> SBool
isEven SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SBool
isEven SInteger
b) (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
nGCDBin (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2))
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger -> SBool
isOdd  SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SBool
isEven SInteger
b) (    SInteger -> SInteger -> SInteger
nGCDBin SInteger
a             (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2))
                                        (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
b)               (    SInteger -> SInteger -> SInteger
nGCDBin SInteger
a             (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a))
                                                                      (    SInteger -> SInteger -> SInteger
nGCDBin (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b)       SInteger
b)
-- | Generalized version that works on arbitrary integers.
gcdBin :: SInteger -> SInteger -> SInteger
gcdBin :: SInteger -> SInteger -> SInteger
gcdBin SInteger
a SInteger
b = SInteger -> SInteger -> SInteger
nGCDBin (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)

-- | \(\mathrm{gcdBin}\, a\, b = \gcd\, a\, b\)
--
-- Instead of proving @gcdBin@ correct, we'll simply show that it is equivalent to @gcd@, hence it has
-- all the properties we already established.
--
-- ==== __Proof__
-- >>> runTP gcdBinEquiv
-- Lemma: gcdEvenEven                      Q.E.D.
-- Lemma: gcdOddEven                       Q.E.D.
-- Lemma: gcdAdd                           Q.E.D.
-- Lemma: commutative                      Q.E.D.
-- Inductive lemma (strong): nGCDBinEquiv
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (5 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.3.1                         Q.E.D.
--     Step: 1.3.2                         Q.E.D.
--     Step: 1.3.3                         Q.E.D.
--     Step: 1.4.1                         Q.E.D.
--     Step: 1.4.2                         Q.E.D.
--     Step: 1.4.3                         Q.E.D.
--     Step: 1.5 (3 way case split)
--       Step: 1.5.1                       Q.E.D.
--       Step: 1.5.2.1                     Q.E.D.
--       Step: 1.5.2.2                     Q.E.D.
--       Step: 1.5.2.3                     Q.E.D.
--       Step: 1.5.2.4                     Q.E.D.
--       Step: 1.5.2.5                     Q.E.D.
--       Step: 1.5.2.6                     Q.E.D.
--       Step: 1.5.3.1                     Q.E.D.
--       Step: 1.5.3.2                     Q.E.D.
--       Step: 1.5.3.3                     Q.E.D.
--       Step: 1.5.3.4                     Q.E.D.
--       Step: 1.5.Completeness            Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: gcdBinEquiv
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] gcdBinEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool
gcdBinEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdBinEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdBinEquiv = do
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gEvenEven <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdEvenEven" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdEvenEven
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gOddEven  <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdOddEven"  TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdOddEven
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gAdd      <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"gcdAdd"      TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdAdd
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm      <- String
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a. String -> TP (Proof a) -> TP (Proof a)
recall String
"commutative" TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
commutative

   -- First prove over the non-negative numbers:
   Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nEq <- String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool)
      (Integer, Integer),
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
-> TP (Proof (Forall "a" Integer -> Forall "b" 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 "a" Integer -> Forall "b" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> (MeasureArgs
      (Forall "a" Integer -> Forall "b" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
sInduct String
"nGCDBinEquiv"
                  (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
b SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
nGCDBin SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b)
                  (\SInteger
a SInteger
b -> (SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
a, SInteger
b), []) ((Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
  -> StepArgs
       (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
    -> StepArgs
         (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer)
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih SInteger
a SInteger
b -> [SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
b 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 -> SInteger
nGCDBin SInteger
a SInteger
b
                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0               SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                   , SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0               SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                   , SInteger -> SBool
isEven SInteger
a SBool -> SBool -> SBool
.&& SInteger -> SBool
isEven SInteger
b SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
nGCDBin (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2)
                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2))
                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
nGCD (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2)
                                                            SInteger -> SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                                                            TPProofRaw SInteger -> SBool -> Hinted (TPProofRaw SInteger)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                                                            Hinted (TPProofRaw SInteger)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SInteger))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gEvenEven Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
a SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2))
                                                            Hinted (Hinted (TPProofRaw SInteger))
-> ChainsTo (Hinted (Hinted (TPProofRaw SInteger)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SInteger)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                            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
                                   , SInteger -> SBool
isOdd SInteger
a  SBool -> SBool -> SBool
.&& SInteger -> SBool
isEven SInteger
b SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCDBin SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2)
                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2))
                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2)
                                                            SInteger -> SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* ((SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                                                            TPProofRaw SInteger -> SBool -> Hinted (TPProofRaw SInteger)
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                                                            Hinted (TPProofRaw SInteger)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SInteger))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gOddEven Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" ((SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
b SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2))
                                                            Hinted (Hinted (TPProofRaw SInteger))
-> ChainsTo (Hinted (Hinted (TPProofRaw SInteger)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SInteger)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                            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
                                   , SInteger -> SBool
isOdd SInteger
b               SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0             SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                                                     , SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
b SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCDBin SInteger
a SInteger
b
                                                                                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCDBin SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a)
                                                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a))
                                                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a)
                                                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a))
                                                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a) SInteger
a
                                                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gAdd Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
a)
                                                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
b SInteger
a
                                                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
comm Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
a)
                                                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                                                            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
                                                                     , SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
b             SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
nGCDBin SInteger
a SInteger
b
                                                                                            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCDBin (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b) SInteger
b
                                                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SInteger
b)
                                                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b) SInteger
b
                                                                                            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
gAdd Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (-SInteger
b))
                                                                                            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD SInteger
a SInteger
b
                                                                                            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
                                                                     ]
                                   ]

   -- Now prove over all integers
   SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> Forall "b" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcWith SMTConfig
cvc5 String
"gcdBinEquiv"
         (\(Forall SInteger
a) (Forall SInteger
b) -> SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcdBin SInteger
a SInteger
b) (StepArgs
   (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
 -> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer -> Forall "b" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SInteger
a SInteger
b -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
gcd SInteger
a SInteger
b
                    SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCD (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                    SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
nEq Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "a" Integer -> Forall "b" 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 @"a" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b))
                    TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
nGCDBin (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
a) (SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
b)
                    SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
gcdBin SInteger
a SInteger
b
                    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

{- HLint ignore gcdSubEquiv "Avoid lambda" -}
{- HLint ignore gcdBinEquiv "Use curry"    -}