Library aritmo
Require Import Znumtheory.
Require Import ZArith.
Require Import Setoid.
Require Import Ring.
Require Import Omega.
Local Open Scope Z_scope.
Definition Z_zerop (z:Z) : { z = 0 } + { z ≠ 0 }.
Defined.
Lemma div_0_is_0 : ∀ {a}, (0|a) → a = 0.
Lemma plus_div_2 : ∀ z, ( z + z ) / 2 = z.
Section Congruence.
Definition congrS n x y := { q : Z | y = x + q × n }.
Definition congr n x y : Prop :=
∃ q, y = x + q × n.
Lemma congr_refl : ∀ n x, congr n x x.
Lemma congr_sym : ∀ n x y, congr n x y → congr n y x.
Lemma congr_trans n : transitive _ (congr n).
Lemma congr_0_eq : ∀ x y, congr 0 x y → x = y.
Lemma congr_1 : ∀ x y, congr 1 x y.
Lemma congr_divide : ∀ n m x y,
congr n x y → (m | n) →
congr m x y.
Lemma congr_plus_compat_l : ∀ n x y m,
congr n x y →
congr n (x + m) (y + m).
Lemma congr_minus_compat_l : ∀ n x y m,
congr n x y →
congr n (x - m) (y - m).
Lemma congr_minus_compat n x y z t :
congr n x y →
congr n z t →
congr n (x - z) (y - t).
Lemma congr_neg_compat n x y :
congr n x y →
congr n (-x) (-y).
Lemma congr_plus_compat : ∀ n x y z t,
congr n x y → congr n z t →
congr n (x + z) (y + t).
Lemma congr_diff : ∀ a b,
congr (a - b) a b.
Lemma congr_mod_compat : ∀ n x, n > 0 →
congr n x (x mod n).
Lemma congr_eqm : ∀ n x y, n > 0 →
congr n x y → eqm n x y.
Lemma eqm_congr : ∀ n x y, n > 0 →
eqm n x y → congr n x y.
Lemma congr_mult_l_compat :
∀ n p x y,
congr n x y →
congr (p × n) (p × x) (p × y).
Lemma congr_opp n x y :
congr n x y →
congr n (-x) (-y).
Definition congr_dec n x y :
{congr n x y} + {¬congr n x y}.
Definition congrS_dec {n} {x} {y} (H :congr n x y) : congrS n x y.
End Congruence.
Hint Resolve congr_refl congr_trans congr_sym congr_0_eq congr_1 : congr.
Notation "x ≡ y [ n ]" := (congr n x y) (at level 80).
Section ggT.
Variables a b : Z.
Hypothesis a_pos : 0 ≤ a.
Hypothesis b_pos : 0 ≤ b.
Inductive Eucl : Set :=
| Eucl_intro : ∀ (u v d:Z) (Hbez:u × a + v × b = d)
(Hpos: 0 ≤ d)
(Hgcd: Zis_gcd a b d), Eucl.
Require Import ZArith.
Require Import Setoid.
Require Import Ring.
Require Import Omega.
Local Open Scope Z_scope.
Definition Z_zerop (z:Z) : { z = 0 } + { z ≠ 0 }.
Defined.
Lemma div_0_is_0 : ∀ {a}, (0|a) → a = 0.
Lemma plus_div_2 : ∀ z, ( z + z ) / 2 = z.
Section Congruence.
Definition congrS n x y := { q : Z | y = x + q × n }.
Definition congr n x y : Prop :=
∃ q, y = x + q × n.
Lemma congr_refl : ∀ n x, congr n x x.
Lemma congr_sym : ∀ n x y, congr n x y → congr n y x.
Lemma congr_trans n : transitive _ (congr n).
Lemma congr_0_eq : ∀ x y, congr 0 x y → x = y.
Lemma congr_1 : ∀ x y, congr 1 x y.
Lemma congr_divide : ∀ n m x y,
congr n x y → (m | n) →
congr m x y.
Lemma congr_plus_compat_l : ∀ n x y m,
congr n x y →
congr n (x + m) (y + m).
Lemma congr_minus_compat_l : ∀ n x y m,
congr n x y →
congr n (x - m) (y - m).
Lemma congr_minus_compat n x y z t :
congr n x y →
congr n z t →
congr n (x - z) (y - t).
Lemma congr_neg_compat n x y :
congr n x y →
congr n (-x) (-y).
Lemma congr_plus_compat : ∀ n x y z t,
congr n x y → congr n z t →
congr n (x + z) (y + t).
Lemma congr_diff : ∀ a b,
congr (a - b) a b.
Lemma congr_mod_compat : ∀ n x, n > 0 →
congr n x (x mod n).
Lemma congr_eqm : ∀ n x y, n > 0 →
congr n x y → eqm n x y.
Lemma eqm_congr : ∀ n x y, n > 0 →
eqm n x y → congr n x y.
Lemma congr_mult_l_compat :
∀ n p x y,
congr n x y →
congr (p × n) (p × x) (p × y).
Lemma congr_opp n x y :
congr n x y →
congr n (-x) (-y).
Definition congr_dec n x y :
{congr n x y} + {¬congr n x y}.
Definition congrS_dec {n} {x} {y} (H :congr n x y) : congrS n x y.
End Congruence.
Hint Resolve congr_refl congr_trans congr_sym congr_0_eq congr_1 : congr.
Notation "x ≡ y [ n ]" := (congr n x y) (at level 80).
Section ggT.
Variables a b : Z.
Hypothesis a_pos : 0 ≤ a.
Hypothesis b_pos : 0 ≤ b.
Inductive Eucl : Set :=
| Eucl_intro : ∀ (u v d:Z) (Hbez:u × a + v × b = d)
(Hpos: 0 ≤ d)
(Hgcd: Zis_gcd a b d), Eucl.
The recursive part of Euclid's algorithm uses well-founded
recursion of non-negative integers. It maintains 6 integers
u1,u2,u3,v1,v2,v3 such that the following invariant holds:
u1×a+u2×b=u3 and v1×a+v2×b=v3 and gcd(u2,v3)=gcd(a,b).
Lemma eucl_rec :
∀ (v3:Z) (Hv3: 0 ≤ v3)
(u3 : Z),
0 ≤ u3 →
∀ u1 u2 v1 v2:Z,
u1 × a + u2 × b = u3 →
v1 × a + v2 × b = v3 →
(∀ d:Z, Zis_gcd u3 v3 d → Zis_gcd a b d) → Eucl.
We get Euclid's algorithm by applying euclid_rec on
1,0,a,0,1,b when b>=0 and 1,0,a,0,-1,-b when b<0.
Lemma eucl : Eucl.
Definition ggT := match eucl with
Eucl_intro _ _ g _ _ _ ⇒ g
end.
Lemma ggT_pos : 0 ≤ ggT.
Lemma ggT_is_Zgcd : ggT = Zgcd a b.
End ggT.
Section on_gcd.
Variables a b : Z.
Lemma Zgcd_divides_l : (Zgcd a b | a).
Lemma Zgcd_divides_r : (Zgcd a b | b).
Lemma Zis_gcd_0_inv_l : Zis_gcd a b 0 → a = 0.
Lemma Zis_gcd_0_inv_r : Zis_gcd a b 0 → b = 0.
End on_gcd.
Section RemEqn.
Variables a b ma mb : Z.
Hypothesis Hma : 0 ≤ ma.
Hypothesis Hmb : 0 ≤ mb.
Definition rem_eqn_spec n := congr ma a n ∧ congr mb b n.
Lemma rem_eqn_nes n : rem_eqn_spec n →
congr (Zgcd ma mb) a b.
Definition rem_eqn_particular : congr (Zgcd ma mb) a b →
{ n : Z | rem_eqn_spec n}.
Lemma rem_eqn_other_solution' :
∀ (H : congr (Zgcd ma mb) a b),
let (n, _) := rem_eqn_particular H in
∀ k, rem_eqn_spec (n + k × Z.lcm ma mb).
Lemma rem_eqn_other_solution :
∀ {n} k, rem_eqn_spec (n + k × Z.lcm ma mb) →
rem_eqn_spec n.
Lemma rem_eqn_other_solution_congr :
∀ {n m}, n ≡ m [Z.lcm ma mb] →
rem_eqn_spec m →
rem_eqn_spec n.
Lemma rem_eqn_all_solutions' :
∀ N (Hsol: rem_eqn_spec N),
let H := rem_eqn_nes N Hsol in
let (n, _) := rem_eqn_particular H in
N ≡ n [Z.lcm ma mb].
Lemma rem_eqn_all_solutions :
∀ N n, rem_eqn_spec N → rem_eqn_spec n →
N ≡ n [Z.lcm ma mb].
Lemma rem_eqn_0_l : ∀ {n},
ma = 0 → rem_eqn_spec n → n = a.
Definition smallest_larger_than (m: Z) (P : Z → Prop) (n: Z) : Prop :=
P n ∧ m ≤ n ∧ ∀ q, P q → m ≤ q → n ≤ q.
Lemma smallest_larger_than_unique m P n n' :
smallest_larger_than m P n →
smallest_larger_than m P n' →
n = n'.
Definition largest_smaller_than (m: Z) (P : Z → Prop) (n: Z) : Prop :=
P n ∧ n ≤ m ∧ ∀ q, P q → q ≤ m → q ≤ n.
Lemma largest_smaller_than_unique m P n n' :
largest_smaller_than m P n →
largest_smaller_than m P n' →
n = n'.
Lemma smallest_solution_larger_than' A :
Z.lcm ma mb > 0 →
∀ q n,
rem_eqn_spec q →
rem_eqn_spec (A + (n - A) mod Z.lcm ma mb) →
A ≤ q →
A + (n - A) mod Z.lcm ma mb ≤ q.
Lemma smallest_solution_larger_than H A :
Z.lcm ma mb > 0 →
smallest_larger_than A rem_eqn_spec (A + (proj1_sig (rem_eqn_particular H) - A) mod Z.lcm ma mb).
Lemma largest_solution_smaller_than H B :
Z.lcm ma mb > 0 →
largest_smaller_than B rem_eqn_spec (B - (B - proj1_sig (rem_eqn_particular H)) mod Z.lcm ma mb).
End RemEqn.
Require Import Utf8.
Require Psatz.
Lemma le_congr i j s :
i < j →
i ≡ j [Zpos s] →
i ≤ j - Zpos s.
Definition Nabs_diff (x y: Z) := N_of_Z (Zmax (x - y) (y - x)).
Lemma Nabs_diff_case x y :
x ≤ y ∧ Nabs_diff x y = N_of_Z (y - x) ∨
y ≤ x ∧ Nabs_diff x y = N_of_Z (x - y).
Definition Zdivides_dec (a b: Z) : { (a | b) } + { ¬ (a | b) }.
Local Coercion Z_of_N : N >-> Z.
Definition Ndivides_dec (a b: N) : { (a | b) } + { ¬ (a | b) }.
Remark Ngcd_is_Zgcd (x y: N) : (N.gcd x y:Z) = Zgcd x y.
Remark Nlcm_is_Zlcm (x y: N) : (N.lcm x y:Z) = Z.lcm x y.
Lemma N_of_pos (x: Z) : 0 ≤ x → (N_of_Z x : Z) = x.