Merge pull request #27 from math-comp/unitz

Add support for `GRing.unit`
math-comp · Sep 30, 2021 · 400edcb · 400edcb
2 parents 8887210 + 1dd2f42
commit 400edcb
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 11 deletions.
diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v
@@ -91,6 +91,13 @@ Instance Op_int_exp : BinOp (@GRing.exp _ : int -> nat -> int) :=
   { TBOp := Z.pow; TBOpInj := Op_int_exp_subproof }.
 Add Zify BinOp Op_int_exp.
 
+Instance Op_unitz : UnOp (has_quality 1 intUnitRing.unitz : int -> bool) :=
+  { TUOp x := (x =? 1)%Z || (x =? - 1)%Z; TUOpInj := ltac:(simpl; lia) }.
+Add Zify UnOp Op_unitz.
+
+Instance Op_int_unit : UnOp (has_quality 1 GRing.unit) := Op_unitz.
+Add Zify UnOp Op_int_unit.
+
 Instance Op_invz : UnOp intUnitRing.invz :=
   { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_invz.
@@ -223,6 +230,13 @@ Instance Op_Z_exp : BinOp (@GRing.exp _ : Z -> nat -> Z) :=
   { TBOp := Z.pow; TBOpInj := Op_Z_exp_subproof }.
 Add Zify BinOp Op_Z_exp.
 
+Instance Op_unitZ : UnOp (has_quality 1 ZInstances.unitZ : Z -> bool) :=
+  { TUOp x := (x =? 1)%Z || (x =? - 1)%Z; TUOpInj _ := erefl }.
+Add Zify UnOp Op_unitZ.
+
+Instance Op_Z_unit : UnOp (has_quality 1 GRing.unit : Z -> bool) := Op_unitZ.
+Add Zify UnOp Op_Z_unit.
+
 Instance Op_invZ : UnOp ZInstances.invZ := { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_invZ.
 
@@ -313,7 +327,7 @@ Instance Op_modz : BinOp modz :=
 Add Zify BinOp Op_modz.
 
 Instance Op_dvdz : BinOp dvdz :=
-  { TBOp n m := Z.eqb (modZ m n) 0%Z;
+  { TBOp n m := (modZ m n =? 0)%Z;
     TBOpInj _ _ := ltac:(apply/dvdz_mod0P/idP; lia) }.
 Add Zify BinOp Op_dvdz.
 
@@ -325,7 +339,7 @@ Instance Op_gcdz : BinOp gcdz := { TBOp := Z.gcd; TBOpInj := Op_gcdz_subproof }.
 Add Zify BinOp Op_gcdz.
 
 Instance Op_coprimez : BinOp coprimez :=
-  { TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
+  { TBOp x y := (Z.gcd x y =? 1)%Z;
     TBOpInj := ltac:(rewrite /= /coprimez; lia) }.
 Add Zify BinOp Op_coprimez.
 
@@ -348,6 +362,8 @@ Add Zify BinOp Op_int_natmul.
 Add Zify BinOp Op_int_intmul.
 Add Zify BinOp Op_int_scale.
 Add Zify BinOp Op_int_exp.
+Add Zify UnOp Op_unitz.
+Add Zify UnOp Op_int_unit.
 Add Zify UnOp Op_invz.
 Add Zify UnOp Op_int_inv.
 Add Zify UnOp Op_absz.
@@ -382,6 +398,8 @@ Add Zify BinOp Op_Z_natmul.
 Add Zify BinOp Op_Z_intmul.
 Add Zify BinOp Op_Z_scale.
 Add Zify BinOp Op_Z_exp.
+Add Zify UnOp Op_unitZ.
+Add Zify UnOp Op_Z_unit.
 Add Zify UnOp Op_invZ.
 Add Zify UnOp Op_Z_inv.
 Add Zify UnOp Op_Z_normr.

diff --git a/theories/zify_ssreflect.v b/theories/zify_ssreflect.v
@@ -27,7 +27,7 @@ Add Zify UnOp Op_nat_inj.
 (******************************************************************************)
 
 Instance Op_addb : BinOp addb :=
-  { TBOp x y := Bool.eqb x (negb y); TBOpInj := ltac:(by case=> [][]) }.
+  { TBOp x y := Bool.eqb x (~~ y); TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_addb.
 
 Instance Op_eqb : BinOp eqb :=
@@ -338,13 +338,11 @@ Instance Op_modn : BinOp modn :=
 Add Zify BinOp Op_modn.
 
 Instance Op_dvdn : BinOp dvdn :=
-  { TBOp x y := Z.eqb (modZ y x) 0%Z;
-    TBOpInj := ltac:(rewrite /dvdn; lia) }.
+  { TBOp x y := (modZ y x =? 0)%Z; TBOpInj := ltac:(rewrite /dvdn; lia) }.
 Add Zify BinOp Op_dvdn.
 
 Instance Op_odd : UnOp odd :=
-  { TUOp x := Z.eqb (modZ x 2) 1%Z;
-    TUOpInj n := ltac:(case: odd (modn2 n); lia) }.
+  { TUOp x := (modZ x 2 =? 1)%Z; TUOpInj n := ltac:(case: odd (modn2 n); lia) }.
 Add Zify UnOp Op_odd.
 
 Instance Op_half : UnOp half :=
@@ -384,7 +382,7 @@ Instance Op_lcmn : BinOp lcmn := { TBOp := Z.lcm; TBOpInj := Op_lcmn_subproof }.
 Add Zify BinOp Op_lcmn.
 
 Instance Op_coprime : BinOp coprime :=
-  { TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
+  { TBOp x y := (Z.gcd x y =? 1)%Z;
     TBOpInj := ltac:(rewrite /= /coprime; lia) }.
 Add Zify BinOp Op_coprime.
 
@@ -399,22 +397,22 @@ Instance Op_natdvd_le' : BinOp (>=^d%O : rel natdvd^d) := Op_dvdn.
 Add Zify BinOp Op_natdvd_le'.
 
 Instance Op_natdvd_ge : BinOp ((>=%O : rel natdvd) : nat -> nat -> bool) :=
-  { TBOp x y := Z.eqb (modZ x y) 0%Z; TBOpInj := ltac:(simpl; lia) }.
+  { TBOp x y := (modZ x y =? 0)%Z; TBOpInj := ltac:(simpl; lia) }.
 Add Zify BinOp Op_natdvd_ge.
 
 Instance Op_natdvd_ge' : BinOp (<=^d%O : rel natdvd^d) := Op_natdvd_ge.
 Add Zify BinOp Op_natdvd_ge'.
 
 Instance Op_natdvd_lt : BinOp ((<%O : rel natdvd) : nat -> nat -> bool) :=
-  { TBOp x y := negb (Z.eqb y x) && Z.eqb (modZ y x) 0%Z;
+  { TBOp x y := ~~ (y =? x)%Z && (modZ y x =? 0)%Z;
     TBOpInj _ _ := ltac:(rewrite /= sdvdEnat; lia) }.
 Add Zify BinOp Op_natdvd_lt.
 
 Instance Op_natdvd_lt' : BinOp (>^d%O : rel natdvd^d) := Op_natdvd_lt.
 Add Zify BinOp Op_natdvd_lt'.
 
 Instance Op_natdvd_gt : BinOp ((>%O : rel natdvd) : nat -> nat -> bool) :=
-  { TBOp x y := negb (Z.eqb x y) && Z.eqb (modZ x y) 0%Z;
+  { TBOp x y := ~~ (x =? y)%Z && (modZ x y =? 0)%Z;
     TBOpInj _ _ := ltac:(rewrite /= sdvdEnat; lia) }.
 Add Zify BinOp Op_natdvd_gt.