-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.CaseSplit
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Use KnuckleDragger to prove @2n^2 + n + 1@ is never divisible by @3@.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.CaseSplit where

import Prelude hiding (sum, length)

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

-- | Prove that @2n^2 + n + 1@ is not divisible by @3@.
--
-- We have:
--
-- >>> notDiv3
-- Lemma: case_n_mod_3_eq_0
--   Asms  : 1                             Q.E.D.
--   Step  : 1                             Q.E.D.
--   Step  : 2                             Q.E.D.
--   Step  : 3                             Q.E.D.
--   Step  : 4                             Q.E.D.
--   Step  : 5                             Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: case_n_mod_3_eq_1
--   Asms  : 1                             Q.E.D.
--   Step  : 1                             Q.E.D.
--   Step  : 2                             Q.E.D.
--   Step  : 3                             Q.E.D.
--   Step  : 4                             Q.E.D.
--   Step  : 5                             Q.E.D.
--   Step  : 6                             Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: case_n_mod_3_eq_2
--   Asms  : 1                             Q.E.D.
--   Step  : 1                             Q.E.D.
--   Step  : 2                             Q.E.D.
--   Step  : 3                             Q.E.D.
--   Step  : 4                             Q.E.D.
--   Step  : 5                             Q.E.D.
--   Step  : 6                             Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: notDiv3
--   Step 1: Case split 3 ways:
--     Case [1 of 3]: n_mod_3[1]           Q.E.D.
--     Case [2 of 3]: n_mod_3[2]           Q.E.D.
--     Case [3 of 3]: n_mod_3[3]           Q.E.D.
--     Completeness:                       Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] notDiv3
notDiv3 :: IO Proof
notDiv3 :: IO Proof
notDiv3 = 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 s :: a -> a
s a
n = a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
n a -> a -> a
forall a. Num a => a -> a -> a
* a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
       p :: SInteger -> SBool
p SInteger
n = SInteger -> SInteger
forall {a}. Num a => a -> a
s SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
0

   -- Do the proof in 3 phases; one each for the possible value of n `mod` 3 being 0, 1, and 2
   -- Note that we use the euclidian definition of division/modulus.

   let case0 :: SInteger -> SBool
case0 SInteger
n = SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
       case1 :: SInteger -> SBool
case1 SInteger
n = SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1
       case2 :: SInteger -> SBool
case2 SInteger
n = SInteger
n SInteger -> SInteger -> SInteger
`sEMod` SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2

   -- Case 0: n = 0 (mod 3)
   c0 <- String
-> (Forall "n" Integer -> SBool)
-> (SInteger -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
String -> a -> steps -> KD Proof
calc String
"case_n_mod_3_eq_0"
              (\(Forall @"n" SInteger
n) -> SInteger -> SBool
case0 SInteger
n SBool -> SBool -> SBool
.=> SInteger -> SBool
p SInteger
n) ((SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof)
-> (SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
              \SInteger
n -> [SInteger -> SBool
case0 SInteger
n] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
forall {a}. Num a => a -> a
s SInteger
n                                       SInteger -> SBool -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger -> SBool
case0 SInteger
n
                              ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let w :: SInteger
w = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"witness" ((SInteger -> SBool) -> SInteger)
-> (SInteger -> SBool) -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
k -> SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
k  -- Grab the witness for the case
                              in SInteger -> SInteger
forall {a}. Num a => a -> a
s (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w)
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. Num a => a -> a
s (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w)
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
18SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
6SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
w) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

   -- Case 1: n = 1 (mod 3)
   c1 <- calc "case_n_mod_3_eq_1"
              (\(Forall @"n" SInteger
n) -> SInteger -> SBool
case1 SInteger
n SBool -> SBool -> SBool
.=> SInteger -> SBool
p SInteger
n) $
              \SInteger
n -> [SInteger -> SBool
case1 SInteger
n] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
forall {a}. Num a => a -> a
s SInteger
n                                         SInteger -> SBool -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger -> SBool
case1 SInteger
n
                              ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let w :: SInteger
w = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"witness" ((SInteger -> SBool) -> SInteger)
-> (SInteger -> SBool) -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
k -> SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1  -- Grab the witness for n being 1 modulo 3
                              in SInteger -> SInteger
forall {a}. Num a => a -> a
s (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> 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
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
9SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
18SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
12SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
18SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
15SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
6SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
5SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

   -- Case 2: n = 2 (mod 3)
   c2 <- calc "case_n_mod_3_eq_2"
              (\(Forall @"n" SInteger
n) -> SInteger -> SBool
case2 SInteger
n SBool -> SBool -> SBool
.=> SInteger -> SBool
p SInteger
n) $
              \SInteger
n -> [SInteger -> SBool
case2 SInteger
n] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
forall {a}. Num a => a -> a
s SInteger
n                                        SInteger -> SBool -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? SInteger -> SBool
case2 SInteger
n
                              ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let w :: SInteger
w = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"witness" ((SInteger -> SBool) -> SInteger)
-> (SInteger -> SBool) -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
k -> SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2 -- Grab the witness for n being 2 modulo 3
                              in SInteger -> SInteger
forall {a}. Num a => a -> a
s (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2)
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2)SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
9SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
6SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
6SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
18SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
24SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
8 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
18SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
27SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
11
                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
6SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
wSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
9SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
w SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2
                              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

   calc "notDiv3"
        (\(Forall @"n" SInteger
n) -> SInteger -> SBool
p SInteger
n) $
        \SInteger
n -> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SBool
p SInteger
n
                 SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ String -> [SBool] -> Helper
cases String
"n_mod_3" [SInteger -> SBool
case0 SInteger
n, SInteger -> SBool
case1 SInteger
n, SInteger -> SBool
case2 SInteger
n]
                   , Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
c0 Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n
                   , Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
c1 Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n
                   , Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
c2 Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` 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
=: 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