1+ /-
2+ Copyright (c) 2018 Chris Hughes. All rights reserved.
3+ Released under Apache 2.0 license as described in the file LICENSE.
4+ Author: Chris Hughes
5+ -/
6+ import data.int.modeq data.fintype data.nat.prime data.nat.gcd data.pnat
7+
8+ open nat nat.modeq int
9+
10+ def zmod (n : ℕ+) := fin n
11+
12+ namespace zmod
13+
14+ instance (n : ℕ+) : has_neg (zmod n) :=
15+ ⟨λ a, ⟨nat_mod (-(a.1 : ℤ)) n,
16+ have h : (n : ℤ) ≠ 0 := int.coe_nat_ne_zero_iff_pos.2 n.pos,
17+ have h₁ : ((n : ℕ) : ℤ) = abs n := (abs_of_nonneg (int.coe_nat_nonneg n)).symm,
18+ by rw [← int.coe_nat_lt, nat_mod, to_nat_of_nonneg (int.mod_nonneg _ h), h₁];
19+ exact int.mod_lt _ h⟩⟩
20+
21+ instance (n : ℕ+) : add_comm_semigroup (zmod n) :=
22+ { add_assoc := λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
23+ (show ((a + b) % n + c) ≡ (a + (b + c) % n) [MOD n],
24+ from calc ((a + b) % n + c) ≡ a + b + c [MOD n] : modeq_add (nat.mod_mod _ _) rfl
25+ ... ≡ a + (b + c) [MOD n] : by rw add_assoc
26+ ... ≡ (a + (b + c) % n) [MOD n] : modeq_add rfl (nat.mod_mod _ _).symm),
27+ add_comm := λ ⟨a, _⟩ ⟨b, _⟩, fin.eq_of_veq (show (a + b) % n = (b + a) % n, by rw add_comm),
28+ ..fin.has_add }
29+
30+ instance (n : ℕ+) : comm_semigroup (zmod n) :=
31+ { mul_assoc := λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
32+ (calc ((a * b) % n * c) ≡ a * b * c [MOD n] : modeq_mul (nat.mod_mod _ _) rfl
33+ ... ≡ a * (b * c) [MOD n] : by rw mul_assoc
34+ ... ≡ a * (b * c % n) [MOD n] : modeq_mul rfl (nat.mod_mod _ _).symm),
35+ mul_comm := λ ⟨a, _⟩ ⟨b, _⟩, fin.eq_of_veq (show (a * b) % n = (b * a) % n, by rw mul_comm),
36+ ..fin.has_mul }
37+
38+ instance (n : ℕ+) : has_one (zmod n) := ⟨⟨(1 % n), nat.mod_lt _ n.pos⟩⟩
39+
40+ instance (n : ℕ+) : has_zero (zmod n) := ⟨⟨0 , n.pos⟩⟩
41+
42+ instance zmod_one.subsingleton : subsingleton (zmod 1 ) :=
43+ ⟨λ a b, fin.eq_of_veq (by rw [eq_zero_of_le_zero (le_of_lt_succ a.2 ),
44+ eq_zero_of_le_zero (le_of_lt_succ b.2 )])⟩
45+
46+ lemma add_val {n : ℕ+} : ∀ a b : zmod n, (a + b).val = (a.val + b.val) % n
47+ | ⟨_, _⟩ ⟨_, _⟩ := rfl
48+
49+ lemma mul_val {n : ℕ+} : ∀ a b : zmod n, (a * b).val = (a.val * b.val) % n
50+ | ⟨_, _⟩ ⟨_, _⟩ := rfl
51+
52+ lemma one_val {n : ℕ+} : (1 : zmod n).val = 1 % n := rfl
53+
54+ @[simp] lemma zero_val (n : ℕ+) : (0 : zmod n).val = 0 := rfl
55+
56+ private lemma one_mul_aux (n : ℕ+) (a : zmod n) : (1 : zmod n) * a = a :=
57+ begin
58+ cases n with n hn,
59+ cases n with n,
60+ { exact (lt_irrefl _ hn).elim },
61+ { cases n with n,
62+ { exact @subsingleton.elim (zmod 1 ) _ _ _ },
63+ { have h₁ : a.1 % n.succ.succ = a.1 := nat.mod_eq_of_lt a.2 ,
64+ have h₂ : 1 % n.succ.succ = 1 := nat.mod_eq_of_lt dec_trivial,
65+ refine fin.eq_of_veq _,
66+ simp [mul_val, one_val, h₁, h₂] } }
67+ end
68+
69+ private lemma left_distrib_aux (n : ℕ+) : ∀ a b c : zmod n, a * (b + c) = a * b + a * c :=
70+ λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
71+ (calc a * ((b + c) % n) ≡ a * (b + c) [MOD n] : modeq_mul rfl (nat.mod_mod _ _)
72+ ... ≡ a * b + a * c [MOD n] : by rw mul_add
73+ ... ≡ (a * b) % n + (a * c) % n [MOD n] : modeq_add (nat.mod_mod _ _).symm (nat.mod_mod _ _).symm)
74+
75+ instance (n : ℕ+) : comm_ring (zmod n) :=
76+ { zero_add := λ ⟨a, ha⟩, fin.eq_of_veq (show (0 + a) % n = a, by rw zero_add; exact nat.mod_eq_of_lt ha),
77+ add_zero := λ ⟨a, ha⟩, fin.eq_of_veq (nat.mod_eq_of_lt ha),
78+ add_left_neg :=
79+ λ ⟨a, ha⟩, fin.eq_of_veq (show (((-a : ℤ) % n).to_nat + a) % n = 0 ,
80+ from int.coe_nat_inj
81+ begin
82+ have hn : (n : ℤ) ≠ 0 := (ne_of_lt (int.coe_nat_lt.2 n.pos)).symm,
83+ rw [int.coe_nat_mod, int.coe_nat_add, to_nat_of_nonneg (int.mod_nonneg _ hn), add_comm],
84+ simp,
85+ end ),
86+ one_mul := one_mul_aux n,
87+ mul_one := λ a, by rw mul_comm; exact one_mul_aux n a,
88+ left_distrib := left_distrib_aux n,
89+ right_distrib := λ a b c, by rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]; refl,
90+ ..zmod.has_zero n,
91+ ..zmod.has_one n,
92+ ..zmod.has_neg n,
93+ ..zmod.add_comm_semigroup n,
94+ ..zmod.comm_semigroup n }
95+
96+ lemma val_cast_nat {n : ℕ+} (a : ℕ) : (a : zmod n).val = a % n :=
97+ begin
98+ induction a with a ih,
99+ { rw [nat.zero_mod]; refl },
100+ { rw [succ_eq_add_one, nat.cast_add, add_val, ih],
101+ show (a % n + ((0 + (1 % n)) % n)) % n = (a + 1 ) % n,
102+ rw [zero_add, nat.mod_mod],
103+ exact nat.modeq.modeq_add (nat.mod_mod a n) (nat.mod_mod 1 n) }
104+ end
105+
106+ lemma mk_eq_cast {n : ℕ+} {a : ℕ} (h : a < n) : (⟨a, h⟩ : zmod n) = (a : zmod n) :=
107+ fin.eq_of_veq (by rw [val_cast_nat, nat.mod_eq_of_lt h])
108+
109+
110+ @[simp] lemma cast_self_eq_zero {n : ℕ+} : ((n : ℕ) : zmod n) = 0 :=
111+ fin.eq_of_veq (show (n : zmod n).val = 0 , by simp [val_cast_nat])
112+
113+ lemma val_cast_of_lt {n : ℕ+} {a : ℕ} (h : a < n) : (a : zmod n).val = a :=
114+ by rw [val_cast_nat, nat.mod_eq_of_lt h]
115+
116+ @[simp] lemma cast_mod_nat (n : ℕ+) (a : ℕ) : ((a % n : ℕ) : zmod n) = a :=
117+ by conv {to_rhs, rw ← nat.mod_add_div a n}; simp
118+
119+ @[simp] lemma cast_val {n : ℕ+} (a : zmod n) : (a.val : zmod n) = a :=
120+ by cases a; simp [mk_eq_cast]
121+
122+ @[simp] lemma cast_mod_int (n : ℕ+) (a : ℤ) : ((a % (n : ℕ) : ℤ) : zmod n) = a :=
123+ by conv {to_rhs, rw ← int.mod_add_div a n}; simp
124+
125+ lemma val_cast_int {n : ℕ+} (a : ℤ) : (a : zmod n).val = (a % (n : ℕ)).nat_abs :=
126+ have h : nat_abs (a % (n : ℕ)) < n := int.coe_nat_lt.1 begin
127+ rw [nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))],
128+ conv {to_rhs, rw ← abs_of_nonneg (int.coe_nat_nonneg n)},
129+ exact int.mod_lt _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)
130+ end ,
131+ int.coe_nat_inj $
132+ by conv {to_lhs, rw [← cast_mod_int n a,
133+ ← nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)),
134+ int.cast_coe_nat, val_cast_of_lt h] }
135+
136+ lemma eq_iff_modeq_nat {n : ℕ+} {a b : ℕ} : (a : zmod n) = b ↔ a ≡ b [MOD n] :=
137+ ⟨λ h, by have := fin.veq_of_eq h;
138+ rwa [val_cast_nat, val_cast_nat] at this ,
139+ λ h, fin.eq_of_veq $ by rwa [val_cast_nat, val_cast_nat]⟩
140+
141+ lemma eq_iff_modeq_int {n : ℕ+} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZMOD (n : ℕ)] :=
142+ ⟨λ h, by have := fin.veq_of_eq h;
143+ rwa [val_cast_int, val_cast_int, ← int.coe_nat_eq_coe_nat_iff,
144+ nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)),
145+ nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))] at this ,
146+ λ h : a % (n : ℕ) = b % (n : ℕ),
147+ by rw [← cast_mod_int n a, ← cast_mod_int n b, h]⟩
148+
149+ instance (n : ℕ+) : fintype (zmod n) := fin.fintype _
150+
151+ lemma card_zmod (n : ℕ+) : fintype.card (zmod n) = n := fintype.card_fin n
152+
153+ end zmod
154+
155+ def zmodp (p : ℕ) (hp : prime p) : Type := zmod ⟨p, hp.pos⟩
156+
157+ namespace zmodp
158+
159+ variables {p : ℕ} (hp : prime p)
160+
161+ instance : comm_ring (zmodp p hp) := zmod.comm_ring ⟨p, hp.pos⟩
162+
163+ instance {p : ℕ} (hp : prime p) : has_inv (zmodp p hp) :=
164+ ⟨λ a, gcd_a a.1 p⟩
165+
166+ lemma add_val : ∀ a b : zmodp p hp, (a + b).val = (a.val + b.val) % p
167+ | ⟨_, _⟩ ⟨_, _⟩ := rfl
168+
169+ lemma mul_val : ∀ a b : zmodp p hp, (a * b).val = (a.val * b.val) % p
170+ | ⟨_, _⟩ ⟨_, _⟩ := rfl
171+
172+ @[simp] lemma one_val : (1 : zmodp p hp).val = 1 :=
173+ nat.mod_eq_of_lt hp.gt_one
174+
175+ @[simp] lemma zero_val : (0 : zmodp p hp).val = 0 := rfl
176+
177+ lemma val_cast_nat (a : ℕ) : (a : zmodp p hp).val = a % p :=
178+ @zmod.val_cast_nat ⟨p, hp.pos⟩ _
179+
180+ lemma mk_eq_cast {a : ℕ} (h : a < p) : (⟨a, h⟩ : zmodp p hp) = (a : zmodp p hp) :=
181+ @zmod.mk_eq_cast ⟨p, hp.pos⟩ _ _
182+
183+ @[simp] lemma cast_self_eq_zero : (p : zmodp p hp) = 0 :=
184+ fin.eq_of_veq (by simpa [val_cast_nat])
185+
186+ lemma val_cast_of_lt {a : ℕ} (h : a < p) : (a : zmodp p hp).val = a :=
187+ @zmod.val_cast_of_lt ⟨p, hp.pos⟩ _ h
188+
189+ @[simp] lemma cast_mod_nat (a : ℕ) : ((a % p : ℕ) : zmodp p hp) = a :=
190+ @zmod.cast_mod_nat ⟨p, hp.pos⟩ _
191+
192+ @[simp] lemma cast_val (a : zmodp p hp) : (a.val : zmodp p hp) = a :=
193+ @zmod.cast_val ⟨p, hp.pos⟩ _
194+
195+ @[simp] lemma cast_mod_int (a : ℤ) : ((a % p : ℤ) : zmodp p hp) = a :=
196+ @zmod.cast_mod_int ⟨p, hp.pos⟩ _
197+
198+ lemma val_cast_int (a : ℤ) : (a : zmodp p hp).val = (a % p).nat_abs :=
199+ @zmod.val_cast_int ⟨p, hp.pos⟩ _
200+
201+ lemma eq_iff_modeq_nat {a b : ℕ} : (a : zmodp p hp) = b ↔ a ≡ b [MOD p] :=
202+ @zmod.eq_iff_modeq_nat ⟨p, hp.pos⟩ _ _
203+
204+ lemma eq_iff_modeq_int {a b : ℤ} : (a : zmodp p hp) = b ↔ a ≡ b [ZMOD p] :=
205+ @zmod.eq_iff_modeq_int ⟨p, hp.pos⟩ _ _
206+
207+ lemma gcd_a_modeq (a b : ℕ) : (a : ℤ) * gcd_a a b ≡ nat.gcd a b [ZMOD b] :=
208+ by rw [← add_zero ((a : ℤ) * _), gcd_eq_gcd_ab];
209+ exact int.modeq.modeq_add rfl (int.modeq.modeq_zero_iff.2 (dvd_mul_right _ _)).symm
210+
211+ lemma mul_inv_eq_gcd (a : ℕ) : (a : zmodp p hp) * a⁻¹ = nat.gcd a p :=
212+ by rw [← int.cast_coe_nat (nat.gcd _ _), nat.gcd_comm, nat.gcd_rec, ← (eq_iff_modeq_int _).2 (gcd_a_modeq _ _)];
213+ simp [has_inv.inv, val_cast_nat]
214+
215+ private lemma mul_inv_cancel_aux : ∀ a : zmodp p hp, a ≠ 0 → a * a⁻¹ = 1 :=
216+ λ ⟨a, hap⟩ ha0, begin
217+ rw [mk_eq_cast, ne.def, ← @nat.cast_zero (zmodp p hp), eq_iff_modeq_nat, modeq_zero_iff] at ha0,
218+ have : nat.gcd p a = 1 := (prime.coprime_iff_not_dvd hp).2 ha0,
219+ rw [mk_eq_cast _ hap, mul_inv_eq_gcd, gcd_comm],
220+ simpa [gcd_comm, this ]
221+ end
222+
223+ instance : discrete_field (zmodp p hp) :=
224+ { zero_ne_one := fin.ne_of_vne $ show 0 ≠ 1 % p,
225+ by rw nat.mod_eq_of_lt hp.gt_one;
226+ exact zero_ne_one,
227+ mul_inv_cancel := mul_inv_cancel_aux hp,
228+ inv_mul_cancel := λ a, by rw mul_comm; exact mul_inv_cancel_aux hp _,
229+ has_decidable_eq := by apply_instance,
230+ inv_zero := show (gcd_a 0 p : zmodp p hp) = 0 ,
231+ by unfold gcd_a xgcd xgcd_aux; refl,
232+ ..zmodp.comm_ring hp,
233+ ..zmodp.has_inv hp }
234+
235+ end zmodp
0 commit comments