| Modular arithmetic |
Require Import Arith ZArith Euclid.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Tactics.
Set Implicit Arguments.
Basic definitions |
| Equality of naturals modulo a natural |
Definition eqMod m n1 n2 :=
exists k,
(Z_of_nat n1 = Z_of_nat n2 + k * Z_of_nat m)%Z.
Lemma two_gt_0 : 2 > 0.
Definition div2 n :=
let (q, r, pfGt, pfEq) := eucl_dev 2 two_gt_0 n in
q.
Definition mod2 n :=
let (q, r, pfGt, pfEq) := eucl_dev 2 two_gt_0 n in
r.
Definition mod2_bool n :=
if eq_nat_dec (mod2 n) 0 then
false
else
true.
|
Theorem eqMod_refl : forall m n,
eqMod m n n.
Theorem eqMod_sym : forall m n1 n2,
eqMod m n1 n2
-> eqMod m n2 n1.
Theorem eqMod_trans : forall m n1 n2 n3,
eqMod m n1 n2
-> eqMod m n2 n3
-> eqMod m n1 n3.
|
Theorem eqMod_plus : forall m n1 n2 k1 k2,
eqMod m n1 n2
-> eqMod m k1 k2
-> eqMod m (n1 + k1) (n2 + k2).
Theorem eqMod_minus : forall m n1 n2 k1 k2,
eqMod m n1 n2
-> eqMod m k1 k2
-> k1 <= n1
-> k2 <= n2
-> eqMod m (n1 - k1) (n2 - k2).
Theorem eqMod_S : forall m n1 n2,
eqMod m n1 n2
-> eqMod m (S n1) (S n2).
Theorem eqMod_mult : forall m n1 n2 k1 k2,
eqMod m n1 n2
-> eqMod m k1 k2
-> eqMod m (n1 * k1) (n2 * k2).
Specific properties of modular equality |
Theorem eqMod_mult_mod : forall m n1 n2 k,
eqMod m n1 n2
-> eqMod (k * m) (k * n1) (k * n2).
Theorem eqMod_one : forall n1 n2,
eqMod 1 n1 n2.
Theorem eqMod_mod : forall m n1 n2,
eqMod m n1 n2
-> eqMod m n1 (m + n2).
Theorem eqMod_plus_minus_mod : forall m n1 n21 n22,
n22 <= n21
-> eqMod m n1 (n21 - n22)
-> eqMod m n1 (n21 + m - n22).
Theorem eqMod_mod' : forall m n1 n2,
eqMod m n1 (m + n2)
-> eqMod m n1 n2.
Theorem eqMod_plus_minus_mod' : forall m n1 n21 n22,
n22 <= n21
-> n22 <= m
-> eqMod m n1 (n21 + (m - n22))
-> eqMod m n1 (n21 - n22).
Theorem eqMod_mod_times : forall m n,
eqMod m m (n * m).
Theorem eqMod_add_mod : forall m n,
eqMod m n (n + m).
Lemma eqMod_mod_plus : forall m n1 n2 k,
eqMod m n1 n2
-> eqMod m (k * m + n1) n2.
Alternative
|
Lemma eqMod_nat : forall m n1 n2,
eqMod m n1 n2
-> exists k, (n1 = n2 + k * m \/ n2 = n1 + k * m).
Lemma eqMod_inj : forall m n1 n2,
eqMod m n1 n2
-> n1 < n2 + m
-> n2 < n1 + m
-> n1 = n2.
Lemma eqMod_nat' : forall m n1 n2 k,
(n1 = n2 + k * m \/ n2 = n1 + k * m)
-> eqMod m n1 n2.
Lemma eqMod_mod2_bool : forall m n1 n2,
eqMod (2 * m) n1 n2
-> mod2_bool n1 = mod2_bool n2.
Lemma eqMod_div2 : forall m n1 n2,
eqMod (2 * m) n1 n2
-> eqMod m (div2 n1) (div2 n2).
Theorem eqMod_contra : forall m n k,
0 < k < m
-> eqMod m n (n + k)
-> False.
Theorem eqMod_S_contra : forall m n,
m >= 2
-> eqMod m n (S n)
-> False.
Theorem eqMod_S_contra_pow2 : forall m n,
eqMod (pow2 (S m)) n (S n)
-> False.
Properties of
|
Lemma mod2_S2 : forall n,
mod2 (S (2 * n)) = 1.
Lemma mod2_bool_S2 : forall n,
mod2_bool (S (2 * n)) = true.
Lemma div2_S2 : forall n,
div2 (S (2 * n)) = n.
Lemma mod2_2 : forall n,
mod2 (2 * n) = 0.
Lemma mod2_bool_2 : forall n,
mod2_bool (2 * n) = false.
Lemma div2_2 : forall n,
div2 (2 * n) = n.
Hint Rewrite mod2_S2 mod2_bool_S2 div2_S2 : asm.
Hint Rewrite mod2_2 mod2_bool_2 div2_2 : asm.
Hints |
Hint Resolve eqMod_refl eqMod_sym eqMod_trans eqMod_one
eqMod_plus eqMod_S eqMod_mult eqMod_mult_mod
eqMod_mod eqMod_plus_minus_mod eqMod_mod_times : asm.