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.

power :: SInteger -> SInteger -> SInteger Source #

Power function over integers.

modAddMultiple :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool)) Source #

\(m > 1 \Rightarrow n + mk \equiv n \pmod{m}\)

Proof

Expand

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

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

Expand

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

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

Expand

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

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

Expand

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

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

Expand

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

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

Expand

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

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

Expand

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

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

Expand

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

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

Expand

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

onePower :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(n \geq 0 \Rightarrow 1^n = 1\)

Proof

Expand

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

powerOf27 :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(n \geq 0 \Rightarrow (27^n \bmod 13) = 1\)

Proof

Expand

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

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

Expand

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