| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.TP.PowerMod
Description
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.
Synopsis
- runCached :: TP a -> IO a
- power :: SInteger -> SInteger -> SInteger
- modAddMultiple :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool))
- modAddRight :: 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))
- modSubRight :: 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))
- modMulRightNeg :: 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))
- modMulLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
- powerMod :: TP (Proof (Forall "b" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool))
- onePower :: TP (Proof (Forall "n" Integer -> SBool))
- powerOf27 :: TP (Proof (Forall "n" Integer -> SBool))
- powerOfThreeMod13VarDivisor :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
Documentation
runCached :: TP a -> IO a Source #
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.
modAddMultiple :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool)) Source #
\(m > 1 \Rightarrow n + mk \equiv n \pmod{m}\)
Proof
>>>runCached modAddMultipleInductive 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
modAddRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(m > 0 \Rightarrow a + b \equiv a + (b \bmod m) \pmod{m}\)
Proof
>>>runCached modAddRightInductive 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
modAddLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(m > 0 \Rightarrow a + b \equiv (a \bmod m) + b \pmod{m}\)
Proof
>>>runCached modAddLeftInductive 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
modSubRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(m > 0 \Rightarrow a - b \equiv a - (b \bmod m) \pmod{m}\)
Proof
>>>runCached modSubRightInductive 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
modMulRightNonneg :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(a \geq 0 \land m > 0 \Rightarrow ab \equiv a \cdot (b \bmod m) \pmod{m}\)
Proof
>>>runCached modMulRightNonnegInductive 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
modMulRightNeg :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(a \geq 0 \land m > 0 \Rightarrow -ab \equiv -\left(a \cdot (b \bmod m)\right) \pmod{m}\)
Proof
>>>runCached modMulRightNegInductive 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
modMulRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(m > 0 \Rightarrow ab \equiv a \cdot (b \bmod m) \pmod{m}\)
Proof
>>>runCached modMulRightInductive 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
modMulLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool)) Source #
\(m > 0 \Rightarrow ab \equiv (a \bmod m) \cdot b \pmod{m}\)
Proof
>>>runCached modMulLeftInductive 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
powerMod :: TP (Proof (Forall "b" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool)) Source #
\(n \geq 0 \land m > 0 \Rightarrow b^n \equiv (b \bmod m)^n \pmod{m}\)
Proof
>>>runCached powerModInductive 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
onePower :: TP (Proof (Forall "n" Integer -> SBool)) Source #
\(n \geq 0 \Rightarrow 1^n = 1\)
Proof
>>>runCached onePowerInductive 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
powerOf27 :: TP (Proof (Forall "n" Integer -> SBool)) Source #
\(n \geq 0 \Rightarrow (27^n \bmod 13) = 1\)
Proof
>>>runCached powerOf27Inductive 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
powerOfThreeMod13VarDivisor :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)) Source #
\(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 powerOfThreeMod13VarDivisorInductive 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