Library ZArith_ext
Require Import Ndec ZArith Znumtheory.
Require Import Arith_ext.
Require Import Bool_ext.
Require Import ssreflect eqtype ssrbool.
Export ZArith.
Export Znumtheory.
Local Close Scope Z_scope.
Local Close Scope positive_scope.
Lemma positiveP : Equality.axiom Ndec.Peqb.
Canonical Structure positive_eqMixin := EqMixin positiveP.
Canonical Structure positive_eqType := Eval hnf in EqType _ positive_eqMixin.
Require Import Arith_ext.
Require Import Bool_ext.
Require Import ssreflect eqtype ssrbool.
Export ZArith.
Export Znumtheory.
Local Close Scope Z_scope.
Local Close Scope positive_scope.
Lemma positiveP : Equality.axiom Ndec.Peqb.
Canonical Structure positive_eqMixin := EqMixin positiveP.
Canonical Structure positive_eqType := Eval hnf in EqType _ positive_eqMixin.
Lemmas on Zeq_bool
Lemma Zeq_bool_refl : forall x, Zeq_bool x x = true.
Lemma Zeq_bool_neq' : forall x y, x <> y -> Zeq_bool x y = false.
Lemma Zeq_bool_classic : forall x y, Zeq_bool x y = true \/ Zeq_bool x y = false.
Lemma Zeq_bool_sym : forall x y, Zeq_bool x y = Zeq_bool y x.
Lemma Zeq_boolP : Equality.axiom Zeq_bool.
Canonical Structure Z_eqMixin := EqMixin Zeq_boolP.
Canonical Structure Z_eqType := Eval hnf in EqType _ Z_eqMixin.
Lemmas on Z
Local Open Scope Z_scope.
Lemma Zlt_pos_0 : forall p, 0 < Zpos p.
Lemma Zopp_eq_mult_neg_1_L : forall n : Z, -1 * n = - n.
Lemma Zplus_Zopp : forall a b, a + - b = a - b.
Lemma Znot_lt_le: forall n m : Z, ~ m < n -> n <= m.
Lemma Zle_minus_1 : forall a b, a < b -> a <= b - 1.
Lemma Zminus_le_decr : forall a b, 0 <= b -> a - b <= a.
Lemma neg_Zlt : forall n, 0 < n -> - n < 0.
Lemma Zminus_lt_compat_r : forall n m p : Z, n < m -> n - p < m - p.
Lemma Zmult_sign : forall a b, 0 <= a -> b <= 0 -> a * b <= 0.
Lemma Zle_scale : forall a b, 0 <= a -> 0 < b -> a <= a * b.
Lemma Zle_scale_neg : forall a b, a <=0 -> 0 < b -> a * b <= a.
Lemma Zle_plus_trans : forall a b c,
0 <= b ->
a <= c ->
a <= b + c.
Lemma Zle_plus_trans_L : forall a b c,
b <= 0 ->
a <= c ->
a + b <= c.
Lemma Z_opposite_sign : forall a b, a < 0 -> 0 <= b -> a <> b.
Lemma Zminus_le_compat : forall a b c, a <= c -> a - b <= c - b.
Lemma Zmult_lt_compat3 : forall a b c, 0 <= a -> 0 < b -> 0 <= c -> a * b < c -> a < c.
Lemma Zmult_lt_reg_l : forall n m p : Z, 0 < p -> p * n < p * m -> n < m.
Lemma Zlt_compat : forall a b c d, b < c -> a = b -> c = d -> a < d.
Lemma Zle_neq_lt : forall n m, n <= m -> n <> m -> n < m.
Lemma neg_Zle: forall n : Z, 0 <= n -> - n <= 0.
Lemma Zlt_neg_pos : forall p q, Zneg p < Zpos q.
Lemma Zlt_opp : forall a b, - b < - a -> a < b.
Lemmas on Z_of_nat
Lemma Z_of_nat_Zpos_P_of_succ_nat : forall n, Z_of_nat (n + 1) = Zpos (P_of_succ_nat n).
Lemma Z_of_nat_inj : forall x y, Z_of_nat x = Z_of_nat y -> x = y.
Lemma Z_of_nat_inj_neq : forall x y, Z_of_nat x <> Z_of_nat y -> x <> y.
Lemma Z_S : forall n, Z_of_nat (S n) = Z_of_nat n + 1.
Lemma Z_of_nat_le_inj: forall x y, Z_of_nat x <= Z_of_nat y -> (x <= y)%nat.
Lemma Z_of_nat_lt_inj: forall x y, Z_of_nat x < Z_of_nat y -> (x < y)%nat.
Lemma Z_of_nat_ge_inj: forall x y, Z_of_nat x >= Z_of_nat y -> (x >= y)%nat.
Lemma Z_of_nat_gt_inj: forall x y, Z_of_nat x > Z_of_nat y -> (x > y)%nat.
Lemma Z_of_nat_0 : forall a, Z_of_nat a = 0 -> a = O.
Lemma Z_of_nat_lt0 : forall a, (0 < a)%nat -> 0 < Z_of_nat a.
Lemma Zmult_neg' : forall a b, a < 0 -> (0 < b)%nat -> a * Z_of_nat b < 0.
Lemma Zmult_neg : forall a b, a < 0 -> 0 < b -> a * b < 0.
Lemma Zle_plus_0_inv : forall (a b : Z), a + b <= 0 -> 0 <= a -> b <= 0.
Lemma Zle_0_mult_inv : forall (a b : Z), 0 <= a * b -> (0 <= a /\ 0 <= b) \/ (a <= 0 /\ b <= 0).
Lemma Zle_mult_0_inv : forall (a b : Z), a * b <= 0 -> 0 < a -> b <= 0.
Lemma Zlt_mult_0_inv : forall (a b : Z), a * b < 0 -> (a < 0 /\ 0 < b) \/ (0 < a /\ b < 0).
Lemmas on Zabs/Zabs_nat
Lemma Zabs_pos : forall z, 0 <= Zabs z.
Lemma Zsgn_Zabs_1 : forall z, z <> 0 -> Zsgn (Zabs z) = 1.
Lemma Zabs_nat_Z_of_nat : forall n, Zabs_nat (Z_of_nat n) = n.
Lemma Zabs_nat_0 : forall a, Zabs_nat a = O -> a = 0.
Lemma Zabs_nat_eq : forall a b, a = b -> Zabs_nat a = Zabs_nat b.
Lemma Zabs_nat_mult : forall a b, Zabs_nat (a * b) = (Zabs_nat a * Zabs_nat b)%nat.
Lemma Zabs_nat_plus_pos : forall a b, 0 <= a -> 0 <= b ->
Zabs_nat (a + b) = (Zabs_nat a + Zabs_nat b)%nat.
Lemma Zabs_nat_Zneg_inj : forall a b, a < 0 -> b < 0 -> Zabs_nat a = Zabs_nat b -> a = b.
Lemma Zabs_nat_Zpos_inj : forall a b, 0 < a -> 0 < b -> Zabs_nat a = Zabs_nat b -> a = b.
Lemma Zabs_nat_Zpos_Z0_inj : forall a b, 0 <= a -> 0 <= b -> Zabs_nat a = Zabs_nat b -> a = b.
Lemma Zabs_nat_Zopp : forall z, Zabs_nat (- z) = Zabs_nat z.
Lemma Z_of_nat_Zabs_nat : forall z, 0 <= z -> Z_of_nat (Zabs_nat z) = z.
Lemma S_Zabs_nat : forall n, 0 <= n -> S (Zabs_nat n) = Zabs_nat (n + 1).
Lemma O_lt_Zabs_nat : forall z, 0 < z -> (O < Zabs_nat z)%nat.
Lemma Zabs_nat_Zsgn : forall z, z <> 0 -> Zabs_nat (Zsgn z) = 1%nat.
Lemma Zabs_mod : forall z b, 0 < b -> z mod b = 0 -> Zabs z mod b = 0.
Lemma Zabs_lt : forall b z, - b < z < b -> Zabs z < b.
Lemma Zlt_abs : forall b z, Zabs z < b -> - b < z < b.
Lemma Zodd_abs : forall z, Zodd z -> Zodd (Zabs z).
Lemma Zlt_0_Zdiv : forall a b, 0 < b -> b <= a -> 0 < a / b.
Lemma Z_div_neg: forall a b : Z, b > 0 -> a <= 0 -> a / b <= 0.
Lemma Zdiv_le_pos : forall z b, 0 <= z -> 0 < b -> z / b <= z.
Lemma Zdiv_le_neg : forall z b, z <= 0 -> 0 < b -> z <= z / b.
Lemma poly_eq0_inv : forall a b k, 0 <= k -> -k < b < k ->
a * k + b = 0 -> a = 0 /\ b = 0.
Lemma poly_eq_inv : forall a b a' b' k,
0 <= a /\ 0 <= b < k /\ 0 <= a' /\ 0 <= b' < k ->
a * k + b = a' * k + b' -> a = a' /\ b = b'.
Lemma poly_Zlt1_inv : forall b a k,
0 <= b -> 0 <= a -> 0 <= k ->
a * k + b < k -> a = 0.
Lemma poly_Zlt1_inv_new : forall b a k : Z, 0 <= b -> 0 <= a -> 0 <= k -> Zabs (a * k + b) < k -> a = 0.
Lemma poly_Zlt : forall a a' b b' k,
0 <= a -> 0 <= a' -> 0 <= b -> 0 <= b' -> 0 <= k ->
a < k ->
a >= a' ->
b < b' ->
a + k * b < a' + k * b'.
Zlt_bool
Lemma Zlt_bool_true : forall a b, a < b -> Zlt_bool a b = true.
Lemma Zlt_bool_true' : forall m n, Zlt_bool m n -> m < n.
Lemma Zlt_bool_false : forall a b, b >= a -> Zlt_bool b a = false.
Lemma Zlt_bool_trans : forall a b c, Zlt_bool a b -> Zlt_bool b c -> Zlt_bool a c.
Lemma Zlt_boolP : forall m n, reflect (m < n) (Zlt_bool m n).
Implicit Arguments Zlt_boolP [m n].
Zle_bool
Lemma Zle_bool_true' : forall m n, Zle_bool m n -> m <= n.
Lemma Zle_bool_true : forall a b, (a <= b) -> Zle_bool a b = true.
Lemma Zle_boolP : forall m n, reflect (m <= n) (Zle_bool m n).
Implicit Arguments Zle_boolP [m n].
Lemma Zle_bool_Zlt_bool : forall a b, Zle_bool a b = ~~ Zlt_bool b a.
Zge_bool
Lemma Zge_bool_true' : forall a b, a >= b -> Zge_bool a b = true.
Lemma Zge_bool_true : forall a b, Zge_bool a b = true -> a >= b.
Lemma Zge_bool_false : forall a b, Zge_bool a b = false -> a < b.
Lemma Zge_boolP : forall m n, reflect (m >= n) (Zge_bool m n).
Implicit Arguments Zge_boolP [m n].
Zgt_bool
Lemma Zgt_bool_true' : forall a b, a > b -> Zgt_bool a b = true.
Lemma Zgt_bool_true : forall a b, Zgt_bool a b = true -> a > b.
Lemma Zgt_bool_false: forall a b, Zgt_bool a b = false -> a <= b.
Lemma Zgt_boolP : forall m n, reflect (m > n) (Zgt_bool m n).
Implicit Arguments Zgt_boolP [m n].
Lemma Zge_bool_Zgt_bool : forall a b, Zge_bool a b = ~~ Zgt_bool b a.
Lemma Zsgn_involutive : forall z, Zsgn (Zsgn z) = Zsgn z.
Lemma Zsgn_0_le_inv : forall z, 0 <= Zsgn z -> Zsgn z = 0 \/ Zsgn z = 1.
Lemma Zabs_Zsgn_1 : forall z, z <> 0 -> Zabs (Zsgn z) = 1.
Definition bZsgn z := if Zeq_bool z 0 then 1%Z else (-1)%Z.
Lemma Zmod_le : forall a b, 0 <= b -> 0 <= a mod b.
Zpower
this function is extensionally the same as Coq.ZArith.Zpower.Zpower_nat but it is defined in a more direct way,
there is already a function Zpower in Coq.ZArith.Zpow_def but with a different type (the exponent can be negative)
Fixpoint Zpower (b : Z) (e : nat) { struct e } : Z :=
match e with
| O => 1
| S e' => b * Zpower b e'
end.
Notation "b ^^ e" := (Zpower b e) (at level 30, right associativity) : zarith_ext_scope.
Local Open Scope zarith_ext_scope.
Lemma Zpower_S : forall k n, k ^^ (S n) = k * k ^^ n.
Lemma Zpower_b_is_exp : forall b n m, b ^^ (n + m) = b ^^ n * b ^^ m.
Lemma Zpower_is_exp : forall n m, 2 ^^ (n + m) = 2 ^^ n * 2 ^^ m.
Lemma Zpower_0 : forall n, 0 < 2 ^^ n.
Lemma Zpower_0' : forall n, 0 <= 2 ^^ n.
Lemma Zpower_1 : forall n, 1 <= 2 ^^ n.
Lemma Zpower_2_le : forall n m, (n <= m)%nat -> 2 ^^ n <= 2 ^^ m.
Lemma Zpower_2_lt : forall n m, (n < m)%nat -> 2 ^^ n < 2 ^^ m.
Lemma Zpower_plus : forall n, 2 ^^ n + 2 ^^ n = 2 ^^ (S n).
Lemma Zpower_b_square : forall z, z * z = z ^^ 2.
Lemma Zpower_b_mult : forall n z, z ^^ n * z ^^ n = z ^^ (2 * n).
Lemma Zpower_unit : forall n, 1 ^^ n = 1.
Lemma Zpower_exp : forall m n z, (z ^^ n) ^^ m = z ^^ (n * m).
Lemma Zpower_exp_mod : forall m n z modu,
(z ^^ n mod modu) ^^ m mod modu = z ^^ (n * m) mod modu.
Lemma power_Zpower : forall b n, Z_of_nat (power b n) = Z_of_nat b ^^ n.
Lemma power_Zpower2 : forall n, Zabs_nat (2 ^^ n - 1) = (power 2 n - 1)%nat.
Lemma Zpower_2_inv : forall n m, 2 ^^ (S n) < 2 ^^ (S m) -> (n < m)%nat.
Lemma Zpower_mod : forall b (n : nat), O <> n -> Zpower b n mod b = 0.
Lemma Zpower_div : forall b n, 0 < b -> O <> n -> Zpower b n / b = Zpower b (n - 1).
Lemma Zpower_nat_Zpower : forall n, Zpower_nat 2 n = Zpower 2 n.
Lemma Zmod_2_Zeven : forall z, z mod 2 = 0 -> Zeven z.
Lemma not_Zmod_2_Zodd : forall z, z mod 2 <> 0 -> Zodd z.
Lemma Zeven_2 : forall m, Zeven (2 * m).
Lemma Zodd_1 : forall m, Zodd (2 * m + 1).
Lemma Zodd_opp : forall z, Zodd z -> Zodd (- z).
Lemma Zeven_opp : forall z, Zeven z -> Zeven (- z).
Lemma Zeven_opp_inv : forall z, Zeven (- z) -> Zeven (z).
Lemma Zodd_Zdivide_2 : forall m, Zodd m -> ~ (2 | m ).
Lemma Zeven_Zeven_bool : forall a, Zeven a -> Zeven_bool a.
Lemma Zeven_bool_Zeven : forall a, Zeven_bool a -> Zeven a.
Lemma Zodd_Zeven_bool_false : forall a, Zodd a -> Zeven_bool a = false.
Definition Zodd_bool z :=
match Zeven_bool z with
| true => false
| _ => true
end.
Lemma Zodd_mult_inv : forall a b, Zodd (a * b) -> Zodd a /\ Zodd b.
Lemma Zeven_Zmod_2 : forall z, Zeven z -> z mod 2 = 0.
Lemma Zodd_Zmod_2 : forall z, Zodd z -> z mod 2 = 1.
Lemma Zeven_plus_inv : forall a b, Zeven (a + b) ->
(Zeven a /\ Zeven b) \/ (Zodd a /\ Zodd b).
Lemma Zmult_2_Zeven : forall a b, a = 2 * b -> Zeven a.
Lemma Zeven_mult_inv : forall a b, Zeven (a * b) -> Zeven a \/ Zeven b.
Lemma Zodd_Zodd_bool : forall z, Zodd z <-> Zodd_bool z.
Lemma Zodd_plus_inv : forall a b, Zodd (a + b) -> (Zodd a /\ Zeven b) \/ (Zeven a /\ Zodd b).
Lemma Zodd_bool_Zplus : forall a b, Zeven_bool b -> Zodd_bool (a + b) = Zodd_bool a.
Lemma Zeven_power : forall m, Zeven (2 ^^ (S m)).
Lemma Zeven_power' : forall m, (0 < m)%nat -> Zeven (2 ^^ m).
Lemma Zodd_bool_Zplus_Zpower : forall n (z : Z) b k, (0 < n)%nat -> (0 < k)%nat ->
Zodd_bool (z + (2 ^^ (k * n)) * b) = Zodd_bool z.
Lemma Zpower_Zdivide : forall n d1 d2, d1 >= 0 -> 2 ^^ n = d1 * d2 ->
exists p, exists q, d1 = 2 ^^ p /\ d2 = 2 ^^ q.
Lemma Zis_gcd_eq : forall n m, 0 <= n -> Zis_gcd n n m -> n = m \/ n = - m.
Lemma Zis_gcd_Zpower_odd : forall n m, Zodd m -> Zis_gcd (2 ^^ n) m 1.
Lemma Zis_gcd_even : forall a b g, Zeven a -> Zeven b ->
Zis_gcd a b (2 * g) -> Zis_gcd (a / 2) (b / 2) g.
Lemma Zis_gcd_even_odd_new : forall a b g,
Zis_gcd a (2 * b + 1) g -> Zis_gcd (2 * a) (2 * b + 1) g.
Lemma Zgcd_0_R : forall a, 0 <= a -> Zgcd a 0 = a.
Lemma Zgcd_same : forall a, 0 <= a -> Zgcd a a = a.
Lemma Zgcd_sym : forall a b, Zgcd a b = Zgcd b a.
Lemma Zgcd_opp : forall a b, Zgcd a (-b) = Zgcd a b.
Lemma Zgcd_even : forall a b, Zeven a -> Zeven b -> Zgcd a b = 2 * Zgcd (a / 2) (b / 2).
Lemma Zgcd_mult : forall a b k, 0 <= k -> Zgcd (k * a) (k * b) = k * Zgcd a b.
Lemma Zgcd_even_odd : forall a b, Zeven a -> Zodd b -> Zgcd a b = Zgcd (a / 2) b.
Lemma Zgcd_Zpower_odd : forall k a b, Zodd b -> Zgcd (a * 2 ^^ k) b = Zgcd a b.
Lemma Zgcd_for_euclid : forall a b q, Zgcd (a + q * b) b = Zgcd a b.
Lemma Zgcd_minus : forall a b, Zgcd a b = Zgcd (a - b) b.
match e with
| O => 1
| S e' => b * Zpower b e'
end.
Notation "b ^^ e" := (Zpower b e) (at level 30, right associativity) : zarith_ext_scope.
Local Open Scope zarith_ext_scope.
Lemma Zpower_S : forall k n, k ^^ (S n) = k * k ^^ n.
Lemma Zpower_b_is_exp : forall b n m, b ^^ (n + m) = b ^^ n * b ^^ m.
Lemma Zpower_is_exp : forall n m, 2 ^^ (n + m) = 2 ^^ n * 2 ^^ m.
Lemma Zpower_0 : forall n, 0 < 2 ^^ n.
Lemma Zpower_0' : forall n, 0 <= 2 ^^ n.
Lemma Zpower_1 : forall n, 1 <= 2 ^^ n.
Lemma Zpower_2_le : forall n m, (n <= m)%nat -> 2 ^^ n <= 2 ^^ m.
Lemma Zpower_2_lt : forall n m, (n < m)%nat -> 2 ^^ n < 2 ^^ m.
Lemma Zpower_plus : forall n, 2 ^^ n + 2 ^^ n = 2 ^^ (S n).
Lemma Zpower_b_square : forall z, z * z = z ^^ 2.
Lemma Zpower_b_mult : forall n z, z ^^ n * z ^^ n = z ^^ (2 * n).
Lemma Zpower_unit : forall n, 1 ^^ n = 1.
Lemma Zpower_exp : forall m n z, (z ^^ n) ^^ m = z ^^ (n * m).
Lemma Zpower_exp_mod : forall m n z modu,
(z ^^ n mod modu) ^^ m mod modu = z ^^ (n * m) mod modu.
Lemma power_Zpower : forall b n, Z_of_nat (power b n) = Z_of_nat b ^^ n.
Lemma power_Zpower2 : forall n, Zabs_nat (2 ^^ n - 1) = (power 2 n - 1)%nat.
Lemma Zpower_2_inv : forall n m, 2 ^^ (S n) < 2 ^^ (S m) -> (n < m)%nat.
Lemma Zpower_mod : forall b (n : nat), O <> n -> Zpower b n mod b = 0.
Lemma Zpower_div : forall b n, 0 < b -> O <> n -> Zpower b n / b = Zpower b (n - 1).
Lemma Zpower_nat_Zpower : forall n, Zpower_nat 2 n = Zpower 2 n.
Lemma Zmod_2_Zeven : forall z, z mod 2 = 0 -> Zeven z.
Lemma not_Zmod_2_Zodd : forall z, z mod 2 <> 0 -> Zodd z.
Lemma Zeven_2 : forall m, Zeven (2 * m).
Lemma Zodd_1 : forall m, Zodd (2 * m + 1).
Lemma Zodd_opp : forall z, Zodd z -> Zodd (- z).
Lemma Zeven_opp : forall z, Zeven z -> Zeven (- z).
Lemma Zeven_opp_inv : forall z, Zeven (- z) -> Zeven (z).
Lemma Zodd_Zdivide_2 : forall m, Zodd m -> ~ (2 | m ).
Lemma Zeven_Zeven_bool : forall a, Zeven a -> Zeven_bool a.
Lemma Zeven_bool_Zeven : forall a, Zeven_bool a -> Zeven a.
Lemma Zodd_Zeven_bool_false : forall a, Zodd a -> Zeven_bool a = false.
Definition Zodd_bool z :=
match Zeven_bool z with
| true => false
| _ => true
end.
Lemma Zodd_mult_inv : forall a b, Zodd (a * b) -> Zodd a /\ Zodd b.
Lemma Zeven_Zmod_2 : forall z, Zeven z -> z mod 2 = 0.
Lemma Zodd_Zmod_2 : forall z, Zodd z -> z mod 2 = 1.
Lemma Zeven_plus_inv : forall a b, Zeven (a + b) ->
(Zeven a /\ Zeven b) \/ (Zodd a /\ Zodd b).
Lemma Zmult_2_Zeven : forall a b, a = 2 * b -> Zeven a.
Lemma Zeven_mult_inv : forall a b, Zeven (a * b) -> Zeven a \/ Zeven b.
Lemma Zodd_Zodd_bool : forall z, Zodd z <-> Zodd_bool z.
Lemma Zodd_plus_inv : forall a b, Zodd (a + b) -> (Zodd a /\ Zeven b) \/ (Zeven a /\ Zodd b).
Lemma Zodd_bool_Zplus : forall a b, Zeven_bool b -> Zodd_bool (a + b) = Zodd_bool a.
Lemma Zeven_power : forall m, Zeven (2 ^^ (S m)).
Lemma Zeven_power' : forall m, (0 < m)%nat -> Zeven (2 ^^ m).
Lemma Zodd_bool_Zplus_Zpower : forall n (z : Z) b k, (0 < n)%nat -> (0 < k)%nat ->
Zodd_bool (z + (2 ^^ (k * n)) * b) = Zodd_bool z.
Lemma Zpower_Zdivide : forall n d1 d2, d1 >= 0 -> 2 ^^ n = d1 * d2 ->
exists p, exists q, d1 = 2 ^^ p /\ d2 = 2 ^^ q.
Lemma Zis_gcd_eq : forall n m, 0 <= n -> Zis_gcd n n m -> n = m \/ n = - m.
Lemma Zis_gcd_Zpower_odd : forall n m, Zodd m -> Zis_gcd (2 ^^ n) m 1.
Lemma Zis_gcd_even : forall a b g, Zeven a -> Zeven b ->
Zis_gcd a b (2 * g) -> Zis_gcd (a / 2) (b / 2) g.
Lemma Zis_gcd_even_odd_new : forall a b g,
Zis_gcd a (2 * b + 1) g -> Zis_gcd (2 * a) (2 * b + 1) g.
Lemma Zgcd_0_R : forall a, 0 <= a -> Zgcd a 0 = a.
Lemma Zgcd_same : forall a, 0 <= a -> Zgcd a a = a.
Lemma Zgcd_sym : forall a b, Zgcd a b = Zgcd b a.
Lemma Zgcd_opp : forall a b, Zgcd a (-b) = Zgcd a b.
Lemma Zgcd_even : forall a b, Zeven a -> Zeven b -> Zgcd a b = 2 * Zgcd (a / 2) (b / 2).
Lemma Zgcd_mult : forall a b k, 0 <= k -> Zgcd (k * a) (k * b) = k * Zgcd a b.
Lemma Zgcd_even_odd : forall a b, Zeven a -> Zodd b -> Zgcd a b = Zgcd (a / 2) b.
Lemma Zgcd_Zpower_odd : forall k a b, Zodd b -> Zgcd (a * 2 ^^ k) b = Zgcd a b.
Lemma Zgcd_for_euclid : forall a b q, Zgcd (a + q * b) b = Zgcd a b.
Lemma Zgcd_minus : forall a b, Zgcd a b = Zgcd (a - b) b.
Zbeta
Definition Zbeta e := Zpower 2 (e * 32).
Lemma Zbeta_power : forall e, Zbeta e = Zpower 2 (e * 32).
Lemma Zbeta1_Zpower2 : Zbeta 1 = 2 ^^ 32.
Lemma Zpower_64_Zbeta : 2 ^^ 64 = Zbeta 2.
Lemma Zbeta_is_exp : forall n m, Zbeta (n + m) = Zbeta n * Zbeta m.
Lemma Zbeta_S : forall n, Zbeta (S n) = Zbeta 1 * Zbeta n.
Lemma Zbeta_0 : forall l, 0 < Zbeta l.
Lemma Zbeta_0' : forall n, 0 <= Zbeta n.
Lemma Zbeta_1 : forall l, 1 <= Zbeta l.
Lemma Zbeta_lt : forall m n, (m < n)%nat -> Zbeta m < Zbeta n.
Lemma Zbeta_le : forall m n, (m <= n)%nat -> Zbeta m <= Zbeta n.
Lemma Zpower_shift_2 : forall n, 4 * n < Zbeta 1 -> n < 2 ^^ 30.
Lemma Zbeta1_1 : forall a, ~ a * Zbeta 1 = 1.
Lemma inv_mod_beta0 : forall m, 1 * m + 0 * Zbeta 1 = m.
Lemma inv_mod_beta1 : forall m, 0 * m + 1 * Zbeta 1 = Zbeta 1.
Lemma inv_mod_beta2 : forall m d, Zis_gcd m (Zbeta 1) d -> Zis_gcd m (Zbeta 1) d.
Definition inv_mod_beta m :=
match euclid_rec m (Zbeta 1) (Zbeta 1) (Zbeta_0' 1) 1 0 m 0 1 (inv_mod_beta0 m) (inv_mod_beta1 m) (inv_mod_beta2 m) with
Euclid_intro u _ d _ _ =>
if Zle_bool d 0 then u mod (Zbeta 1) else
if Zeq_bool u 0 then 0 else
- (u mod (Zbeta 1)) + Zbeta 1
end.
Equality modulo
Definition eqmod (a b m : Z) := exists k : Z, a = b + k * m.
Notation "a =m b {{ m }}" := (eqmod a b m) (at level 80) : eqmod_scope.
Local Open Scope eqmod_scope.
Lemma eqmod_Zmod : forall a b m, 0 < m -> (a =m b {{ m }} <-> a mod m = b mod m).
Lemma eqmod_Zmod2 : forall a b m, 0 <= m -> (a =m b {{ m }} -> a mod m = b mod m).
Lemma eqmod_refl : forall a m, a =m a {{ m }}.
Lemma eqmod_sym : forall a b m, a =m b {{ m }} -> b =m a {{ m }}.
Lemma eqmod_trans : forall a b c m, a =m b {{ m }} -> b =m c {{ m }} -> a =m c {{ m }}.
Lemma eqmod_compat_plus_R : forall a b c m, a =m c {{ m }} -> a + b =m c + b {{ m }}.
Lemma eqmod_div : forall k m a b, a =m b {{ k * m }} -> a =m b {{ m }}.
Lemma eqmod_reg_mult : forall a b d m, a =m b {{ m }} -> a * d =m b * d {{ m }}.
Lemma eqmod_reg_mult_l : forall a b d m, a =m b {{ m }} -> d * a =m d * b {{ m }}.
Lemma eqmod_rewrite : forall m a a' b c,
a =m a' {{ m }} -> a * b =m c {{ m }} -> a' * b =m c {{ m }}.
Lemma eqmod_reg_mult' : forall a b d m, Zis_gcd m d 1 ->
a * d =m b * d {{ m }} -> a =m b {{ m }}.
Lemma eqmod_reg_mult_beta_odd : forall a b k m, Zodd m ->
Zbeta k * a =m Zbeta k * b {{ m }} -> a =m b {{ m }}.
Lemma eqmod_minmod : forall m a b k, a =m b {{ m }} -> a - k * m =m b {{ m }}.
Lemma eqmod_mod : forall m a b, 0 < m -> a =m b {{ m }} -> a =m b mod m {{ m }}.
Lemma eqmod_inv : forall a a' m, 0 <= a < m -> 0 <= a' < m -> a =m a' {{ m }} -> a = a'.
Local Close Scope eqmod_scope.
Local Close Scope zarith_ext_scope.
Definition Zisum z := if z is Zpos p then Z_of_nat (isum (nat_of_P p)) else 0.
Lemma Zisum_prop' : forall a, 0 <= a -> Zisum (a + 1) = Zisum a + (a + 1).
factorial in Z
Definition Zfact (z : Z) : Z :=
match z with
| Zpos p => Z_of_nat (fact (nat_of_P p))
| _ => 1
end.
Lemma Zfact_neg : forall z, z < 0 -> Zfact z = 1.
Lemma Zfact_zero : Zfact 0 = 1.
Lemma fact_lemma : forall n, (0 < n)%nat -> (fact n = n * fact (n - 1))%nat.
Lemma Zfact_pos : forall z, z > 0 -> Zfact z = z * Zfact (z - 1).
Local Open Scope zarith_ext_scope.
Require Import List.
Fixpoint bbs_fun_rec (n : nat) (seed m : Z) {struct n} : list bool :=
match n with
| O => nil
| S n => (Zodd_bool seed) :: (bbs_fun_rec n (seed ^^ 2 mod m) m)
end.
Definition bbs_fun (len:nat)(seed m:Z) : list bool :=
bbs_fun_rec len ((seed * seed) mod m) m.
Lemma bbs_fun_rec_app0 : forall n seed modu,
bbs_fun_rec (S n) (seed mod modu) modu =
bbs_fun_rec n (seed mod modu) modu ++
bbs_fun_rec 1 ((seed mod modu)^^(power 2 n) mod modu) modu.
Lemma bbs_fun_rec_app0' : forall n seed modu,
bbs_fun_rec (S n) (seed mod modu) modu =
bbs_fun_rec 1 (seed mod modu) modu ++
bbs_fun_rec n ((seed mod modu)^^2 mod modu) modu.
Lemma bbs_fun_rec_app1 : forall n k seed modu,
bbs_fun_rec (n + k) (seed mod modu) modu =
bbs_fun_rec n (seed mod modu) modu ++
bbs_fun_rec k ((seed mod modu)^^(power 2 n) mod modu) modu.
Lemma bbs_fun_rec_app : forall k n seed modu,
bbs_fun_rec (k * S n) (seed mod modu) modu =
bbs_fun_rec (k * n) (seed mod modu) modu ++
bbs_fun_rec k ((seed mod modu)^^(power 2 (k * n)) mod modu) modu.