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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.Numeric where

import Prelude hiding (sum, length)

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

-- | Prove that sum of constants @c@ from @0@ to @n@ is @n*c@.
--
-- We have:
--
-- >>> sumConstProof
-- Inductive lemma: sumConst_correct
--   Base: sumConst_correct.Base           Q.E.D.
--   Asms: 1                               Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: sumConst_correct.Step           Q.E.D.
-- [Proven] sumConst_correct
sumConstProof :: IO Proof
sumConstProof :: IO Proof
sumConstProof = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let c :: SInteger
       c :: SInteger
c = String -> SInteger
forall a. SMTDefinable a => String -> a
uninterpret String
"c"

       sum :: SInteger -> SInteger
       sum :: SInteger -> SInteger
sum = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"sum" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
0 (SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sum (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

       spec :: SInteger -> SInteger
       spec :: SInteger -> SInteger
spec SInteger
n = SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n

   String
-> (Forall "n" Integer -> SBool)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"sumConst_correct"
          (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger
sum SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec SInteger
n) ((Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
sum (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)  SInteger -> SBool -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sum SInteger
n  SInteger -> [Helper] -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [Proof -> Helper
hprf Proof
ih, SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
spec SInteger
n
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
c SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
cSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
n
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
cSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
spec (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

-- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.
--
-- >>> sumProof
-- Inductive lemma: sum_correct
--   Base: sum_correct.Base                Q.E.D.
--   Asms: 1                               Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: sum_correct.Step                Q.E.D.
-- [Proven] sum_correct
sumProof :: IO Proof
sumProof :: IO Proof
sumProof = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let sum :: SInteger -> SInteger
       sum :: SInteger -> SInteger
sum = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"sum" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
0 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sum (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

       spec :: SInteger -> SInteger
       spec :: SInteger -> SInteger
spec SInteger
n = (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
2

       p :: SInteger -> SBool
       p :: SInteger -> SBool
p SInteger
n = SInteger -> SInteger
sum SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec SInteger
n

   String
-> (Forall "n" Integer -> SBool)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"sum_correct"
          (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SBool
p SInteger
n) ((Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
sum (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)    SInteger -> SBool -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sum SInteger
n  SInteger -> [Helper] -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [Proof -> Helper
hprf Proof
ih, SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
spec SInteger
n
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
spec (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

-- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.
--
-- >>> sumSquareProof
-- Inductive lemma: sumSquare_correct
--   Base: sumSquare_correct.Base          Q.E.D.
--   Asms: 1                               Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: sumSquare_correct.Step          Q.E.D.
-- [Proven] sumSquare_correct
sumSquareProof :: IO Proof
sumSquareProof :: IO Proof
sumSquareProof = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let sumSquare :: SInteger -> SInteger
       sumSquare :: SInteger -> SInteger
sumSquare = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"sumSquare" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
0 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sumSquare (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

       spec :: SInteger -> SInteger
       spec :: SInteger -> SInteger
spec SInteger
n = (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
6

       p :: SInteger -> SBool
       p :: SInteger -> SBool
p SInteger
n = SInteger -> SInteger
sumSquare SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec SInteger
n

   String
-> (Forall "n" Integer -> SBool)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"sumSquare_correct"
          (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SBool
p SInteger
n) ((Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
sumSquare (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)           SInteger -> SBool -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
sumSquare SInteger
n SInteger -> [Helper] -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [Proof -> Helper
hprf Proof
ih, SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
spec SInteger
n
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
spec (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

-- | Prove that @11^n - 4^n@ is always divisible by 7.
--
-- NB. As of Feb 2025, z3 struggles with the inductive step in this proof, but cvc5 performs just fine.
--
-- We have:
--
-- >>> elevenMinusFour
-- Lemma: powN                             Q.E.D.
-- Inductive lemma: elevenMinusFour
--   Base: elevenMinusFour.Base            Q.E.D.
--   Step: 1                               Q.E.D.
--   Asms: 2                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Asms: 3                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Asms: 6                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Step: 7                               Q.E.D.
--   Step: 8                               Q.E.D.
--   Step: elevenMinusFour.Step            Q.E.D.
-- [Proven] elevenMinusFour
elevenMinusFour :: IO Proof
elevenMinusFour :: IO Proof
elevenMinusFour = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
   let pow :: SInteger -> SInteger -> SInteger
       pow :: SInteger -> SInteger -> SInteger
pow = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"pow" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
x SInteger
y -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SInteger
1 (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger -> SInteger
pow SInteger
x (SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

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

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

   inductWith cvc5 "elevenMinusFour"
          (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SBool
emf SInteger
n) $
          \Proof
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SBool
emf (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
`pow` (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0), Proof -> Helper
hprf (Proof
powN Proof -> (Inst "x" Integer, Inst "n" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" (SInteger
11 :: SInteger), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n))]
                ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0), Proof -> Helper
hprf (Proof
powN Proof -> (Inst "x" Integer, Inst "n" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" ( SInteger
4 :: SInteger), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n))]
                ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
11 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
n)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
n)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
n))
                SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0), Proof -> Helper
hprf Proof
ih]
                ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let x :: SInteger
x = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"x" (\SInteger
v -> SInteger
7SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 SInteger -> SInteger -> SInteger
`pow` SInteger
n)   -- Apply the IH and grab the witness for it
                in Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x)
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
7 Integer -> SInteger -> SBool
`sDivides` (SInteger
7 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
11 SInteger -> SInteger -> SInteger
`pow` SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x))
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed