Skip to content

Commit 2d34652

Browse files
pi8027pi8027
committed
Minor cleanup
1 parent 3396bdc commit 2d34652

File tree

3 files changed

+76
-83
lines changed

3 files changed

+76
-83
lines changed

‎theories/ssrZ.v‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ Fact leZ_add m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m + n). Proof. lia. Qed.
8787
Fact leZ_mul m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m * n). Proof. lia. Qed.
8888
Fact leZ_anti m : Z.leb 0 m -> Z.leb m 0 -> m = Z0. Proof. lia. Qed.
8989

90-
Lemma subZ_ge0 m n : Z.leb 0 (n - m)%R = Z.leb m n.
90+
Fact subZ_ge0 m n : Z.leb 0 (n - m)%R = Z.leb m n.
9191
Proof. by rewrite /GRing.add /GRing.opp /=; lia. Qed.
9292

9393
Fact leZ_total m n : Z.leb m n || Z.leb n m. Proof. lia. Qed.
@@ -111,30 +111,30 @@ Canonical Z_numDomainType := NumDomainType Z Mixin.
111111
Canonical Z_normedZmodType := NormedZmodType Z Z Mixin.
112112
Canonical Z_realDomainType := [realDomainType of Z].
113113

114-
Lemma Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
114+
Fact Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
115115
Proof.
116116
have Hnat (m : nat) : Z.of_nat m = (m%:R)%R.
117117
by elim: m => // m; rewrite Nat2Z.inj_succ -Z.add_1_l mulrS => ->.
118118
case: n => n; rewrite /intmul /=; first exact: Hnat.
119119
by congr Z.opp; rewrite Nat2Z.inj_add /= mulrSr Hnat.
120120
Qed.
121121

122-
Lemma Z_of_int_is_additive : additive Z_of_int.
122+
Fact Z_of_int_is_additive : additive Z_of_int.
123123
Proof. by move=> m n; rewrite !Z_of_intE raddfB. Qed.
124124

125125
Canonical Z_of_int_additive := Additive Z_of_int_is_additive.
126126

127-
Lemma int_of_Z_is_additive : additive int_of_Z.
127+
Fact int_of_Z_is_additive : additive int_of_Z.
128128
Proof. exact: can2_additive Z_of_intK int_of_ZK. Qed.
129129

130130
Canonical int_of_Z_additive := Additive int_of_Z_is_additive.
131131

132-
Lemma Z_of_int_is_multiplicative : multiplicative Z_of_int.
132+
Fact Z_of_int_is_multiplicative : multiplicative Z_of_int.
133133
Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed.
134134

135135
Canonical Z_of_int_rmorphism := AddRMorphism Z_of_int_is_multiplicative.
136136

137-
Lemma int_of_Z_is_multiplicative : multiplicative int_of_Z.
137+
Fact int_of_Z_is_multiplicative : multiplicative int_of_Z.
138138
Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed.
139139

140140
Canonical int_of_Z_rmorphism := AddRMorphism int_of_Z_is_multiplicative.

‎theories/zify_algebra.v‎

Lines changed: 36 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -22,27 +22,24 @@ Import Order.Theory GRing.Theory Num.Theory SsreflectZifyInstances.
2222
(******************************************************************************)
2323

2424
Instance Inj_int_Z : InjTyp int Z :=
25-
{ inj := Z_of_int; pred := fun => True; cstr := fun => I }.
25+
{ inj := Z_of_int; pred _ := True; cstr _ := I }.
2626
Add Zify InjTyp Inj_int_Z.
2727

28-
Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj := fun => erefl }.
28+
Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj _ := erefl }.
2929
Add Zify UnOp Op_Z_of_int.
3030

3131
Instance Op_int_of_Z : UnOp int_of_Z := { TUOp := id; TUOpInj := int_of_ZK }.
3232
Add Zify UnOp Op_int_of_Z.
3333

34-
Instance Op_Posz : UnOp Posz := { TUOp := id; TUOpInj := fun => erefl }.
34+
Instance Op_Posz : UnOp Posz := { TUOp := id; TUOpInj _ := erefl }.
3535
Add Zify UnOp Op_Posz.
3636

3737
Instance Op_Negz : UnOp Negz :=
38-
{ TUOp := fun x => (- (x + 1))%Z; TUOpInj := ltac:(simpl; lia) }.
38+
{ TUOp x := (- (x + 1))%Z; TUOpInj := ltac:(simpl; lia) }.
3939
Add Zify UnOp Op_Negz.
4040

41-
Lemma Op_int_eq_subproof n m : n = m <-> Z_of_int n = Z_of_int m.
42-
Proof. split=> [->|] //; case: n m => ? [] ? ?; f_equal; lia. Qed.
43-
4441
Instance Op_int_eq : BinRel (@eq int) :=
45-
{ TR := @eq Z; TRInj := Op_int_eq_subproof }.
42+
{ TR := @eq Z; TRInj := ltac:(by split=> [->|/(can_inj Z_of_intK)]) }.
4643
Add Zify BinRel Op_int_eq.
4744

4845
Instance Op_int_eq_op : BinOp (@eq_op int_eqType : int -> int -> bool) :=
@@ -76,27 +73,26 @@ Instance Op_int_mulr : BinOp *%R := Op_mulz.
7673
Add Zify BinOp Op_int_mulr.
7774

7875
Instance Op_int_natmul : BinOp (@GRing.natmul _ : int -> nat -> int) :=
79-
{ TBOp := Z.mul;
80-
TBOpInj := ltac:(move=> ? ?; rewrite /= pmulrn mulrzz; lia) }.
76+
{ TBOp := Z.mul; TBOpInj _ _ := ltac:(rewrite /= pmulrn mulrzz; lia) }.
8177
Add Zify BinOp Op_int_natmul.
8278

8379
Instance Op_int_intmul : BinOp ( *~%R%R : int -> int -> int) :=
84-
{ TBOp := Z.mul; TBOpInj := ltac:(move=> ? ?; rewrite /= mulrzz; lia) }.
80+
{ TBOp := Z.mul; TBOpInj _ _ := ltac:(rewrite /= mulrzz; lia) }.
8581
Add Zify BinOp Op_int_intmul.
8682

8783
Instance Op_int_scale : BinOp (@GRing.scale _ [lmodType int of int^o]) :=
8884
Op_mulz.
8985
Add Zify BinOp Op_int_scale.
9086

91-
Lemma Op_int_exp_subproof n m : Z_of_int (n ^+ m) = (Z_of_int n ^ Z.of_nat m)%Z.
87+
Fact Op_int_exp_subproof n m : Z_of_int (n ^+ m) = (Z_of_int n ^ Z.of_nat m)%Z.
9288
Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed.
9389

9490
Instance Op_int_exp : BinOp (@GRing.exp _ : int -> nat -> int) :=
9591
{ TBOp := Z.pow; TBOpInj := Op_int_exp_subproof }.
9692
Add Zify BinOp Op_int_exp.
9793

9894
Instance Op_invz : UnOp intUnitRing.invz :=
99-
{ TUOp := id; TUOpInj := fun => erefl }.
95+
{ TUOp := id; TUOpInj _ := erefl }.
10096
Add Zify UnOp Op_invz.
10197

10298
Instance Op_int_inv : UnOp GRing.inv := Op_invz.
@@ -152,30 +148,30 @@ Instance Op_int_gt' : BinOp (<^d%O : rel int^d) := Op_int_gt.
152148
Add Zify BinOp Op_int_gt'.
153149

154150
Instance Op_int_min : BinOp (Order.min : int -> int -> int) :=
155-
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
151+
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
156152
Add Zify BinOp Op_int_min.
157153

158154
Instance Op_int_min' : BinOp ((Order.max : int^d -> _) : int -> int -> int) :=
159-
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
155+
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
160156
Add Zify BinOp Op_int_min'.
161157

162158
Instance Op_int_max : BinOp (Order.max : int -> int -> int) :=
163-
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
159+
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
164160
Add Zify BinOp Op_int_max.
165161

166162
Instance Op_int_max' : BinOp ((Order.min : int^d -> _) : int -> int -> int) :=
167-
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
163+
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
168164
Add Zify BinOp Op_int_max'.
169165

170166
Instance Op_int_meet : BinOp (Order.meet : int -> int -> int) :=
171-
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
167+
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
172168
Add Zify BinOp Op_int_meet.
173169

174170
Instance Op_int_meet' : BinOp (Order.join : int^d -> _) := Op_int_min.
175171
Add Zify BinOp Op_int_meet'.
176172

177173
Instance Op_int_join : BinOp (Order.join : int -> int -> int) :=
178-
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
174+
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
179175
Add Zify BinOp Op_int_join.
180176

181177
Instance Op_int_join' : BinOp (Order.meet : int^d -> _) := Op_int_max.
@@ -192,21 +188,21 @@ Instance Op_Z_0 : CstOp (0%R : Z) := { TCst := 0%Z; TCstInj := erefl }.
192188
Add Zify CstOp Op_Z_0.
193189

194190
Instance Op_Z_add : BinOp (+%R : Z -> Z -> Z) :=
195-
{ TBOp := Z.add; TBOpInj := fun _ _ => erefl }.
191+
{ TBOp := Z.add; TBOpInj _ _ := erefl }.
196192
Add Zify BinOp Op_Z_add.
197193

198194
Instance Op_Z_opp : UnOp (@GRing.opp _ : Z -> Z) :=
199-
{ TUOp := Z.opp; TUOpInj := fun => erefl }.
195+
{ TUOp := Z.opp; TUOpInj _ := erefl }.
200196
Add Zify UnOp Op_Z_opp.
201197

202198
Instance Op_Z_1 : CstOp (1%R : Z) := { TCst := 1%Z; TCstInj := erefl }.
203199
Add Zify CstOp Op_Z_1.
204200

205201
Instance Op_Z_mulr : BinOp ( *%R : Z -> Z -> Z) :=
206-
{ TBOp := Z.mul; TBOpInj := fun _ _ => erefl }.
202+
{ TBOp := Z.mul; TBOpInj _ _ := erefl }.
207203
Add Zify BinOp Op_Z_mulr.
208204

209-
Lemma Op_Z_natmul_subproof (n : Z) (m : nat) : (n *+ m)%R = (n * Z.of_nat m)%Z.
205+
Fact Op_Z_natmul_subproof (n : Z) (m : nat) : (n *+ m)%R = (n * Z.of_nat m)%Z.
210206
Proof. elim: m => [|m]; rewrite (mulr0n, mulrS); lia. Qed.
211207

212208
Instance Op_Z_natmul : BinOp (@GRing.natmul _ : Z -> nat -> Z) :=
@@ -220,31 +216,30 @@ Add Zify BinOp Op_Z_intmul.
220216
Instance Op_Z_scale : BinOp (@GRing.scale _ [lmodType Z of Z^o]) := Op_Z_mulr.
221217
Add Zify BinOp Op_Z_scale.
222218

223-
Lemma Op_Z_exp_subproof n m : (n ^+ m)%R = (n ^ Z.of_nat m)%Z.
219+
Fact Op_Z_exp_subproof n m : (n ^+ m)%R = (n ^ Z.of_nat m)%Z.
224220
Proof. by rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS. Qed.
225221

226222
Instance Op_Z_exp : BinOp (@GRing.exp _ : Z -> nat -> Z) :=
227223
{ TBOp := Z.pow; TBOpInj := Op_Z_exp_subproof }.
228224
Add Zify BinOp Op_Z_exp.
229225

230-
Instance Op_invZ : UnOp ZInstances.invZ :=
231-
{ TUOp := id; TUOpInj := fun => erefl }.
226+
Instance Op_invZ : UnOp ZInstances.invZ := { TUOp := id; TUOpInj _ := erefl }.
232227
Add Zify UnOp Op_invZ.
233228

234229
Instance Op_Z_inv : UnOp (GRing.inv : Z -> Z) :=
235-
{ TUOp := id; TUOpInj := fun => erefl }.
230+
{ TUOp := id; TUOpInj _ := erefl }.
236231
Add Zify UnOp Op_Z_inv.
237232

238233
Instance Op_Z_normr : UnOp (Num.norm : Z -> Z) :=
239-
{ TUOp := Z.abs; TUOpInj := fun => erefl }.
234+
{ TUOp := Z.abs; TUOpInj _ := erefl }.
240235
Add Zify UnOp Op_Z_normr.
241236

242237
Instance Op_Z_sgr : UnOp (Num.sg : Z -> Z) :=
243238
{ TUOp := Z.sgn; TUOpInj := ltac:(case=> //=; lia) }.
244239
Add Zify UnOp Op_Z_sgr.
245240

246241
Instance Op_Z_le : BinOp (<=%O : Z -> Z -> bool) :=
247-
{ TBOp := Z.leb; TBOpInj := fun _ _ => erefl }.
242+
{ TBOp := Z.leb; TBOpInj _ _ := erefl }.
248243
Add Zify BinOp Op_Z_le.
249244

250245
Instance Op_Z_le' : BinOp (>=^d%O : rel Z^d) := Op_Z_le.
@@ -258,7 +253,7 @@ Instance Op_Z_ge' : BinOp (<=^d%O : rel Z^d) := Op_Z_ge.
258253
Add Zify BinOp Op_Z_ge'.
259254

260255
Instance Op_Z_lt : BinOp (<%O : Z -> Z -> bool) :=
261-
{ TBOp := Z.ltb; TBOpInj := fun _ _ => erefl }.
256+
{ TBOp := Z.ltb; TBOpInj _ _ := erefl }.
262257
Add Zify BinOp Op_Z_lt.
263258

264259
Instance Op_Z_lt' : BinOp (>^d%O : rel Z^d) := Op_Z_lt.
@@ -272,30 +267,30 @@ Instance Op_Z_gt' : BinOp (<^d%O : rel Z^d) := Op_Z_gt.
272267
Add Zify BinOp Op_Z_gt'.
273268

274269
Instance Op_Z_min : BinOp (Order.min : Z -> Z -> Z) :=
275-
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
270+
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
276271
Add Zify BinOp Op_Z_min.
277272

278273
Instance Op_Z_min' : BinOp ((Order.max : Z^d -> _) : Z -> Z -> Z) :=
279-
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
274+
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
280275
Add Zify BinOp Op_Z_min'.
281276

282277
Instance Op_Z_max : BinOp (Order.max : Z -> Z -> Z) :=
283-
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
278+
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
284279
Add Zify BinOp Op_Z_max.
285280

286281
Instance Op_Z_max' : BinOp ((Order.min : Z^d -> _) : Z -> Z -> Z) :=
287-
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
282+
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
288283
Add Zify BinOp Op_Z_max'.
289284

290285
Instance Op_Z_meet : BinOp (Order.meet : Z -> Z -> Z) :=
291-
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
286+
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
292287
Add Zify BinOp Op_Z_meet.
293288

294289
Instance Op_Z_meet' : BinOp (Order.join : Z^d -> _) := Op_Z_min.
295290
Add Zify BinOp Op_Z_meet'.
296291

297292
Instance Op_Z_join : BinOp (Order.join : Z -> Z -> Z) :=
298-
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
293+
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
299294
Add Zify BinOp Op_Z_join.
300295

301296
Instance Op_Z_join' : BinOp (Order.meet : Z^d -> _) := Op_Z_max.
@@ -305,7 +300,7 @@ Add Zify BinOp Op_Z_join'.
305300
(* intdiv *)
306301
(******************************************************************************)
307302

308-
Lemma Op_divz_subproof n m :
303+
Fact Op_divz_subproof n m :
309304
Z_of_int (divz n m) = divZ (Z_of_int n) (Z_of_int m).
310305
Proof. case: n => [[|n]|n]; rewrite /divz /divZ /= ?addn1 /=; nia. Qed.
311306

@@ -318,19 +313,19 @@ Instance Op_modz : BinOp modz :=
318313
Add Zify BinOp Op_modz.
319314

320315
Instance Op_dvdz : BinOp dvdz :=
321-
{ TBOp := fun n m => Z.eqb (modZ m n) 0%Z;
322-
TBOpInj := ltac:(move=> ? ? /=; apply/dvdz_mod0P/idP; lia) }.
316+
{ TBOp n m := Z.eqb (modZ m n) 0%Z;
317+
TBOpInj _ _ := ltac:(apply/dvdz_mod0P/idP; lia) }.
323318
Add Zify BinOp Op_dvdz.
324319

325-
Lemma Op_gcdz_subproof n m :
320+
Fact Op_gcdz_subproof n m :
326321
Z_of_int (gcdz n m) = Z.gcd (Z_of_int n) (Z_of_int m).
327322
Proof. rewrite /gcdz -Z.gcd_abs_l -Z.gcd_abs_r; lia. Qed.
328323

329324
Instance Op_gcdz : BinOp gcdz := { TBOp := Z.gcd; TBOpInj := Op_gcdz_subproof }.
330325
Add Zify BinOp Op_gcdz.
331326

332327
Instance Op_coprimez : BinOp coprimez :=
333-
{ TBOp := fun x y => Z.eqb (Z.gcd x y) 1%Z;
328+
{ TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
334329
TBOpInj := ltac:(rewrite /= /coprimez; lia) }.
335330
Add Zify BinOp Op_coprimez.
336331

0 commit comments

Comments
 (0)