Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for GRing.unit #27

Merged
merged 2 commits into from
Sep 30, 2021
Merged

Add support for GRing.unit #27

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fe208d7
Add support for GRing.unit
pi8027 Sep 30, 2021
1dd2f42
Minor syntactic cleanup
pi8027 Sep 30, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 20 additions & 2 deletions theories/zify_algebra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand All @@ -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.

Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
16 changes: 7 additions & 9 deletions theories/zify_ssreflect.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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 :=
Expand Down Expand Up @@ -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.

Expand All @@ -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.

Expand Down