-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.PowerMod
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proofs about power and modulus. Adapted from an example by amigalemming,
-- see <http://github.com/LeventErkok/sbv/issues/744>.
--
-- We also demonstrate the proof-caching features of TP.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.PowerMod where

import Data.SBV
import Data.SBV.TP

-- | The proofs in this module are structured so they are presented at the top-level and reused.
-- This results in re-running the proofs over and over, as each proof has to run all its dependents.
-- To avoid re-running proofs, we tell TP to use a proof-cache. Note that use of a proof-cache comes
-- with the user obligation that all proofs used are uniquely named. Otherwise the results can be
-- unsound, and SBV will indicate this possibility in its output.
runCached :: TP a -> IO a
runCached :: forall a. TP a -> IO a
runCached = SMTConfig -> TP a -> IO a
forall a. SMTConfig -> TP a -> IO a
runTPWith (SMTConfig -> SMTConfig
tpCache SMTConfig
z3)

-- | Power function over integers.
power :: SInteger -> SInteger -> SInteger
power :: SBV Integer -> SBV Integer -> SBV Integer
power = String
-> (SBV Integer -> SBV Integer -> SBV Integer)
-> SBV Integer
-> SBV Integer
-> SBV Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"power" ((SBV Integer -> SBV Integer -> SBV Integer)
 -> SBV Integer -> SBV Integer -> SBV Integer)
-> (SBV Integer -> SBV Integer -> SBV Integer)
-> SBV Integer
-> SBV Integer
-> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SBV Integer
b SBV Integer
n -> SBool -> SBV Integer -> SBV Integer -> SBV Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
0) SBV Integer
1 (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b (SBV Integer
nSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
-SBV Integer
1))

-- | \(m > 1 \Rightarrow n + mk \equiv n \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modAddMultiple
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] modAddMultiple :: Ɐk ∷ Integer → Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
modAddMultiple :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool))
modAddMultiple :: TP
  (Proof
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
modAddMultiple = do
   SMTConfig
-> String
-> (Forall "k" Integer
    -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "k" Integer
    -> Forall "n" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "k" Integer
    -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith (SMTConfig -> SMTConfig
tpCache SMTConfig
cvc5) String
"modAddMultiple"
      (\(Forall SBV Integer
k) (Forall SBV Integer
n) (Forall SBV Integer
m) -> SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
1 SBool -> SBool -> SBool
.=> (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
mSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
k) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) ((Proof
    (IHType
       (Forall "k" Integer
        -> Forall "n" Integer -> Forall "m" Integer -> SBool))
  -> IHArg
       (Forall "k" Integer
        -> Forall "n" Integer -> Forall "m" Integer -> SBool)
  -> IStepArgs
       (Forall "k" Integer
        -> Forall "n" Integer -> Forall "m" Integer -> SBool)
       Integer)
 -> TP
      (Proof
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)))
-> (Proof
      (IHType
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "k" Integer
          -> Forall "n" Integer -> Forall "m" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "k" Integer
         -> Forall "n" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \Proof
  (IHType
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
ih IHArg
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
k SBV Integer
n SBV Integer
m -> [SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
1] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
mSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*(SBV Integer
IHArg
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
kSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                              SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
mSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
IHArg
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
k SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                              SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
mSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
IHArg
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
k) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                              SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)
ih Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)
-> IArgs (Forall "n" Integer -> Forall "m" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                              TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                              SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(m > 0 \Rightarrow a + b \equiv a + (b \bmod m) \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modAddRight
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] modAddRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modAddRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddRight :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddRight = do
   Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
mAddMul <- TP
  (Proof
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
modAddMultiple
   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"modAddRight"
      (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0  SBool -> SBool -> SBool
.=>  (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \SBV Integer
a SBV Integer
b SBV Integer
m -> [SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
mAddMul Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
m), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                         TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(m > 0 \Rightarrow a + b \equiv (a \bmod m) + b \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modAddLeft
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] modAddLeft :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modAddLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddLeft :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddLeft = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddR <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddRight
   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"modAddLeft"
      (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=>  (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \SBV Integer
a SBV Integer
b SBV Integer
m -> [SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
bSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
a) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddR
                         TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(m > 0 \Rightarrow a - b \equiv a - (b \bmod m) \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modSubRight
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] modSubRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modSubRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modSubRight :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modSubRight = do
   Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
mAddMul <- TP
  (Proof
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
modAddMultiple
   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"modSubRight"
      (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=>  (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
-SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \SBV Integer
a SBV Integer
b SBV Integer
m -> [SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
-SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
m)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
mSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*(- (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
m))) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
mAddMul Proof
  (Forall "k" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "k" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" (- (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
m)), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                         TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                         SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(a \geq 0 \land m > 0 \Rightarrow ab \equiv a \cdot (b \bmod m) \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modMulRightNonneg
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Inductive lemma: modMulRightNonneg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven. Cached: modAddRight] modMulRightNonneg :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modMulRightNonneg :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRightNonneg :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRightNonneg = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddL <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddLeft
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddR <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddRight

   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"modMulRightNonneg"
      (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.&& SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=> (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) ((Proof
    (IHType
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  -> IHArg
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "m" Integer -> SBool)
  -> IStepArgs
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "m" Integer -> SBool)
       Integer)
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> (Proof
      (IHType
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \Proof
  (IHType
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
ih IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer
b SBV Integer
m -> [SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0, SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- ((SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1)SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
bSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddR Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddL Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
Proof (Forall "b" Integer -> Forall "m" Integer -> SBool)
ih Proof (Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs (Forall "b" Integer -> Forall "m" 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 @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddL
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(a \geq 0 \land m > 0 \Rightarrow -ab \equiv -\left(a \cdot (b \bmod m)\right) \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modMulRightNeg
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modMulRightNeg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven. Cached: modAddMultiple] modMulRightNeg :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modMulRightNeg :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRightNeg :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRightNeg = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddL <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modAddLeft
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mSubR <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modSubRight

   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"modMulRightNeg"
      (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.&& SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=> (-(SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (-(SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) ((Proof
    (IHType
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  -> IHArg
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "m" Integer -> SBool)
  -> IStepArgs
       (Forall "a" Integer
        -> Forall "b" Integer -> Forall "m" Integer -> SBool)
       Integer)
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> (Proof
      (IHType
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool))
    -> IHArg
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
    -> IStepArgs
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \Proof
  (IHType
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
ih IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer
b SBV Integer
m -> [SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0, SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (-((SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1)SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
-SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mSubR Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddL Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" (- (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m)), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
Proof (Forall "b" Integer -> Forall "m" Integer -> SBool)
ih Proof (Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs (Forall "b" Integer -> Forall "m" 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 @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ((-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mAddL
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (-(SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (-((SBV Integer
IHArg
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(m > 0 \Rightarrow ab \equiv a \cdot (b \bmod m) \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modMulRight
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Inductive lemma: modMulRightNonneg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modMulRightNeg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modMulRight
--   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. Cached: modAddLeft, modAddMultiple, modAddRight] modMulRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modMulRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRight :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRight = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulNonneg <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRightNonneg
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulNeg    <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRightNeg

   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"modMulRight"
        (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=> (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV Integer
a SBV Integer
b SBV Integer
m -> [SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw (SBV Integer))] -> TPProofRaw (SBV Integer)
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                               SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulNonneg Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" SBV Integer
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                               TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed
                                    , SBV Integer
a SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  SBV Integer
0 SBool
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (-((-SBV Integer
a)SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                               SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulNeg Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (-SBV Integer
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                               TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (-((-SBV Integer
a) SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m)) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed
                                    ]

-- | \(m > 0 \Rightarrow ab \equiv (a \bmod m) \cdot b \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached modMulLeft
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Inductive lemma: modMulRightNonneg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modMulRightNeg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modMulRight
--   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.
-- Lemma: modMulLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight] modMulLeft :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
modMulLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulLeft :: TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulLeft = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulR <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRight

   String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"modMulLeft"
        (\(Forall SBV Integer
a) (Forall SBV Integer
b) (Forall SBV Integer
m) -> SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=> (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (StepArgs
   (Forall "a" Integer
    -> Forall "b" Integer -> Forall "m" Integer -> SBool)
   Integer
 -> TP
      (Proof
         (Forall "a" Integer
          -> Forall "b" Integer -> Forall "m" Integer -> SBool)))
-> StepArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
     Integer
-> TP
     (Proof
        (Forall "a" Integer
         -> Forall "b" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV Integer
a SBV Integer
b SBV Integer
m -> [SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SBV Integer
aSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                           SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
bSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
*SBV Integer
a) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                           SBV Integer
-> Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulR
                           TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                           SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
a SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                           SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(n \geq 0 \land m > 0 \Rightarrow b^n \equiv (b \bmod m)^n \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached powerMod
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Inductive lemma: modMulRightNonneg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modMulRightNeg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modMulRight
--   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.
-- Lemma: modMulLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modMulRightNonneg               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modSubRight                     Q.E.D.
-- Cached: modMulRightNeg                  Q.E.D.
-- Cached: modMulRight                     Q.E.D.
-- Inductive lemma: powerModInduct
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: powerMod                         Q.E.D.
-- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerMod :: Ɐb ∷ Integer → Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
powerMod :: TP (Proof (Forall "b" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool))
powerMod :: TP
  (Proof
     (Forall "b" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
powerMod = do
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulL <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulLeft
   Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulR <- TP
  (Proof
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" Integer -> SBool))
modMulRight

   -- We want to write the b parameter first, but need to induct on n. So, this helper rearranges the parameters only.
   Proof
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
pMod <- String
-> (Forall "n" Integer
    -> Forall "m" Integer -> Forall "b" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool))
    -> IHArg
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "m" Integer -> Forall "b" Integer -> SBool))
forall t.
(Proposition
   (Forall "n" Integer
    -> Forall "m" Integer -> Forall "b" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer
    -> Forall "m" Integer -> Forall "b" Integer -> SBool)
-> (Proof
      (IHType
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool))
    -> IHArg
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "m" Integer -> Forall "b" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"powerModInduct"
      (\(Forall @"n" SBV Integer
n) (Forall @"m" SBV Integer
m) (Forall @"b" SBV Integer
b) -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.&& SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) ((Proof
    (IHType
       (Forall "n" Integer
        -> Forall "m" Integer -> Forall "b" Integer -> SBool))
  -> IHArg
       (Forall "n" Integer
        -> Forall "m" Integer -> Forall "b" Integer -> SBool)
  -> IStepArgs
       (Forall "n" Integer
        -> Forall "m" Integer -> Forall "b" Integer -> SBool)
       Integer)
 -> TP
      (Proof
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)))
-> (Proof
      (IHType
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool))
    -> IHArg
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer
          -> Forall "m" Integer -> Forall "b" Integer -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "n" Integer
         -> Forall "m" Integer -> Forall "b" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
      \Proof
  (IHType
     (Forall "n" Integer
      -> Forall "m" Integer -> Forall "b" Integer -> SBool))
ih IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer
m SBV Integer
b -> [SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0, SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b (SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
nSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulL Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "n" Integer
      -> Forall "m" Integer -> Forall "b" Integer -> SBool))
Proof (Forall "m" Integer -> Forall "b" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "b" Integer -> SBool)
-> IArgs (Forall "m" 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 @"m" SBV Integer
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulL Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
mMulR Proof
  (Forall "a" Integer
   -> Forall "b" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "a" Integer
      -> Forall "b" Integer -> Forall "m" 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" (SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b" SBV Integer
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
m)
                                     TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (SBV Integer
IHArg
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
nSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                     SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

   -- Same as above, just a more natural selection of variable order.
   String
-> (Forall "b" Integer
    -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "b" Integer
         -> Forall "n" Integer -> Forall "m" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"powerMod"
         (\(Forall SBV Integer
b) (Forall SBV Integer
n) (Forall SBV Integer
m) -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.&& SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
b SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
b SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m)
         [Proof
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "n" Integer
   -> Forall "m" Integer -> Forall "b" Integer -> SBool)
pMod]

-- | \(n \geq 0 \Rightarrow 1^n = 1\)
--
-- ==== __Proof__
-- >>> runCached onePower
-- Inductive lemma: onePower
--   Step: Base                            Q.E.D.
--   Step: 1 (unfold power)                Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] onePower :: Ɐn ∷ Integer → Bool
onePower :: TP (Proof (Forall "n" Integer -> SBool))
onePower :: TP (Proof (Forall "n" Integer -> SBool))
onePower = String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"onePower"
                  (\(Forall SBV Integer
n) -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
1 SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
1) ((Proof (IHType (Forall "n" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> SBool)
  -> IStepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (IHType (Forall "n" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof (IHType (Forall "n" Integer -> SBool))
ih IHArg (Forall "n" Integer -> SBool)
n -> [] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
1 (SBV Integer
IHArg (Forall "n" Integer -> SBool)
nSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+SBV Integer
1)
                               SBV Integer -> String -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold power"
                               TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer
1 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
1 SBV Integer
IHArg (Forall "n" Integer -> SBool)
n
                               SBV Integer -> Proof SBool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "n" Integer -> SBool))
ih
                               TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
1 :: SInteger)
                               SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(n \geq 0 \Rightarrow (27^n \bmod 13) = 1\)
--
-- ==== __Proof__
-- >>> runCached powerOf27
-- Inductive lemma: onePower
--   Step: Base                            Q.E.D.
--   Step: 1 (unfold power)                Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Inductive lemma: modMulRightNonneg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modMulRightNeg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modMulRight
--   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.
-- Lemma: modMulLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modMulRightNonneg               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modSubRight                     Q.E.D.
-- Cached: modMulRightNeg                  Q.E.D.
-- Cached: modMulRight                     Q.E.D.
-- Inductive lemma: powerModInduct
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: powerMod                         Q.E.D.
-- Lemma: powerOf27
--   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. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerOf27 :: Ɐn ∷ Integer → Bool
powerOf27 :: TP (Proof (Forall "n" Integer -> SBool))
powerOf27 :: TP (Proof (Forall "n" Integer -> SBool))
powerOf27 = do
   Proof (Forall "n" Integer -> SBool)
pOne <- TP (Proof (Forall "n" Integer -> SBool))
onePower
   Proof
  (Forall "b" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
pMod <- TP
  (Proof
     (Forall "b" Integer
      -> Forall "n" Integer -> Forall "m" Integer -> SBool))
powerMod
   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"powerOf27" (\(Forall SBV Integer
n) -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
27 SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
1) (StepArgs (Forall "n" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \SBV Integer
n -> [SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0]
                       [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
27 SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13
                       SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "b" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
pMod Proof
  (Forall "b" Integer
   -> Forall "n" Integer -> Forall "m" Integer -> SBool)
-> IArgs
     (Forall "b" Integer
      -> Forall "n" Integer -> Forall "m" 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 @"b" SBV Integer
27, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SBV Integer
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV Integer
13)
                       TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer -> SBV Integer -> SBV Integer
power (SBV Integer
27 SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13) SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13
                       SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
1 SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13
                       SBV Integer
-> Proof (Forall "n" Integer -> SBool) -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
pOne
                       TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer
1 SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13
                       SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
1 :: SInteger)
                       SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed

-- | \(n \geq 0 \wedge m > 0 \implies (27^{\frac{n}{3}} \bmod 13) \cdot 3^{n \bmod 3} \equiv 3^{n \bmod 3} \pmod{m}\)
--
-- ==== __Proof__
-- >>> runCached powerOfThreeMod13VarDivisor
-- Inductive lemma: onePower
--   Step: Base                            Q.E.D.
--   Step: 1 (unfold power)                Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modAddMultiple
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modAddLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Inductive lemma: modMulRightNonneg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Lemma: modSubRight
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: modMulRightNeg
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: modMulRight
--   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.
-- Lemma: modMulLeft
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modMulRightNonneg               Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modAddRight                     Q.E.D.
-- Cached: modAddLeft                      Q.E.D.
-- Cached: modAddMultiple                  Q.E.D.
-- Cached: modSubRight                     Q.E.D.
-- Cached: modMulRightNeg                  Q.E.D.
-- Cached: modMulRight                     Q.E.D.
-- Inductive lemma: powerModInduct
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: powerMod                         Q.E.D.
-- Lemma: powerOf27
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: powerOfThreeMod13VarDivisor
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerOfThreeMod13VarDivisor :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
powerOfThreeMod13VarDivisor :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
powerOfThreeMod13VarDivisor :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
powerOfThreeMod13VarDivisor = do
   Proof (Forall "n" Integer -> SBool)
p27 <- TP (Proof (Forall "n" Integer -> SBool))
powerOf27
   String
-> (Forall "n" Integer -> Forall "m" Integer -> SBool)
-> StepArgs
     (Forall "n" Integer -> Forall "m" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> Forall "m" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> Forall "m" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> Forall "m" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"powerOfThreeMod13VarDivisor"
        (\(Forall SBV Integer
n) (Forall SBV Integer
m) ->
            SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.&& SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0 SBool -> SBool -> SBool
.=>     SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
27 (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
3) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
3 (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
                                   SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer -> SBV Integer -> SBV Integer
power  SBV Integer
3 (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m) (StepArgs
   (Forall "n" Integer -> Forall "m" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)))
-> StepArgs
     (Forall "n" Integer -> Forall "m" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV Integer
n SBV Integer
m -> [SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0, SBV Integer
m SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
0]
             [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
27 (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEDiv` SBV Integer
3) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
13 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
3 (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
             SBV Integer -> Proof Bool -> Hinted (SBV Integer)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
p27 Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SBV Integer -> SBV Integer -> SBV Integer
sEDiv SBV Integer
n SBV Integer
3)
             TPProofRaw (SBV Integer)
-> ChainsTo (TPProofRaw (SBV Integer))
-> ChainsTo (TPProofRaw (SBV Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Integer -> SBV Integer -> SBV Integer
power SBV Integer
3 (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3) SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
m
             SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed