Skip to content

Commit

Permalink
Minor cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@pi8027
pi8027 committed Sep 29, 2021
1 parent 3396bdc commit 9f46d94
Show file tree
Hide file tree
Showing 2 changed files with 55 additions and 59 deletions.
62 changes: 30 additions & 32 deletions theories/zify_algebra.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,20 +22,20 @@ Import Order.Theory GRing.Theory Num.Theory SsreflectZifyInstances.
(******************************************************************************)

Instance Inj_int_Z : InjTyp int Z :=
{ inj := Z_of_int; pred := fun => True; cstr := fun => I }.
{ inj := Z_of_int; pred _ := True; cstr _ := I }.
Add Zify InjTyp Inj_int_Z.

Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj := fun => erefl }.
Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj _ := erefl }.
Add Zify UnOp Op_Z_of_int.

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

Instance Op_Posz : UnOp Posz := { TUOp := id; TUOpInj := fun => erefl }.
Instance Op_Posz : UnOp Posz := { TUOp := id; TUOpInj _ := erefl }.
Add Zify UnOp Op_Posz.

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

Lemma Op_int_eq_subproof n m : n = m <-> Z_of_int n = Z_of_int m.
Expand Down Expand Up @@ -76,12 +76,11 @@ Instance Op_int_mulr : BinOp *%R := Op_mulz.
Add Zify BinOp Op_int_mulr.

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

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

Instance Op_int_scale : BinOp (@GRing.scale _ [lmodType int of int^o]) :=
Expand All @@ -96,7 +95,7 @@ Instance Op_int_exp : BinOp (@GRing.exp _ : int -> nat -> int) :=
Add Zify BinOp Op_int_exp.

Instance Op_invz : UnOp intUnitRing.invz :=
{ TUOp := id; TUOpInj := fun => erefl }.
{ TUOp := id; TUOpInj _ := erefl }.
Add Zify UnOp Op_invz.

Instance Op_int_inv : UnOp GRing.inv := Op_invz.
Expand Down Expand Up @@ -152,30 +151,30 @@ Instance Op_int_gt' : BinOp (<^d%O : rel int^d) := Op_int_gt.
Add Zify BinOp Op_int_gt'.

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

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

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

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

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

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

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

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

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

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

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

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

Lemma Op_Z_natmul_subproof (n : Z) (m : nat) : (n *+ m)%R = (n * Z.of_nat m)%Z.
Expand All @@ -227,24 +226,23 @@ 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_invZ : UnOp ZInstances.invZ :=
{ TUOp := id; TUOpInj := fun => erefl }.
Instance Op_invZ : UnOp ZInstances.invZ := { TUOp := id; TUOpInj _ := erefl }.
Add Zify UnOp Op_invZ.

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

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

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

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

Instance Op_Z_le' : BinOp (>=^d%O : rel Z^d) := Op_Z_le.
Expand All @@ -258,7 +256,7 @@ Instance Op_Z_ge' : BinOp (<=^d%O : rel Z^d) := Op_Z_ge.
Add Zify BinOp Op_Z_ge'.

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

Instance Op_Z_lt' : BinOp (>^d%O : rel Z^d) := Op_Z_lt.
Expand All @@ -272,30 +270,30 @@ Instance Op_Z_gt' : BinOp (<^d%O : rel Z^d) := Op_Z_gt.
Add Zify BinOp Op_Z_gt'.

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

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

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

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

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

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

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

Instance Op_Z_join' : BinOp (Order.meet : Z^d -> _) := Op_Z_max.
Expand All @@ -318,8 +316,8 @@ Instance Op_modz : BinOp modz :=
Add Zify BinOp Op_modz.

Instance Op_dvdz : BinOp dvdz :=
{ TBOp := fun n m => Z.eqb (modZ m n) 0%Z;
TBOpInj := ltac:(move=> ? ? /=; apply/dvdz_mod0P/idP; lia) }.
{ TBOp n m := Z.eqb (modZ m n) 0%Z;
TBOpInj _ _ := ltac:(apply/dvdz_mod0P/idP; lia) }.
Add Zify BinOp Op_dvdz.

Lemma Op_gcdz_subproof n m :
Expand All @@ -330,7 +328,7 @@ Instance Op_gcdz : BinOp gcdz := { TBOp := Z.gcd; TBOpInj := Op_gcdz_subproof }.
Add Zify BinOp Op_gcdz.

Instance Op_coprimez : BinOp coprimez :=
{ TBOp := fun x y => Z.eqb (Z.gcd x y) 1%Z;
{ TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
TBOpInj := ltac:(rewrite /= /coprimez; lia) }.
Add Zify BinOp Op_coprimez.

Expand Down
52 changes: 25 additions & 27 deletions theories/zify_ssreflect.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Module SsreflectZifyInstances.
Import Order.Theory.

Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
{ TUOp := id; TUOpInj := fun => erefl }.
{ TUOp := id; TUOpInj _ := erefl }.
Add Zify UnOp Op_bool_inj.

Instance Op_nat_inj : UnOp (inj : nat -> Z) := Op_Z_of_nat.
Expand All @@ -27,7 +27,7 @@ Add Zify UnOp Op_nat_inj.
(******************************************************************************)

Instance Op_addb : BinOp addb :=
{ TBOp := fun x y => Bool.eqb x (negb y); TBOpInj := ltac:(by case=> [][]) }.
{ TBOp x y := Bool.eqb x (negb y); TBOpInj := ltac:(by case=> [][]) }.
Add Zify BinOp Op_addb.

Instance Op_eqb : BinOp eqb :=
Expand All @@ -45,21 +45,21 @@ Instance Op_bool_le' : BinOp (>=^d%O : rel bool^d) := Op_bool_le.
Add Zify BinOp Op_bool_le'.

Instance Op_bool_ge : BinOp (>=%O : bool -> bool -> bool) :=
{ TBOp := fun x y => implb y x; TBOpInj := ltac:(by case=> [][]) }.
{ TBOp x y := implb y x; TBOpInj := ltac:(by case=> [][]) }.
Add Zify BinOp Op_bool_ge.

Instance Op_bool_ge' : BinOp (<=^d%O : rel bool^d) := Op_bool_ge.
Add Zify BinOp Op_bool_ge'.

Instance Op_bool_lt : BinOp (<%O : bool -> bool -> bool) :=
{ TBOp := fun x y => ~~ x && y; TBOpInj := ltac:(by case=> [][]) }.
{ TBOp x y := ~~ x && y; TBOpInj := ltac:(by case=> [][]) }.
Add Zify BinOp Op_bool_lt.

Instance Op_bool_lt' : BinOp (>^d%O : rel bool^d) := Op_bool_lt.
Add Zify BinOp Op_bool_lt'.

Instance Op_bool_gt : BinOp (>%O : bool -> bool -> bool) :=
{ TBOp := fun x y => x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
{ TBOp x y := x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
Add Zify BinOp Op_bool_gt.

Instance Op_bool_gt' : BinOp (<^d%O : rel bool^d) := Op_bool_gt.
Expand Down Expand Up @@ -108,7 +108,7 @@ Instance Op_bool_top' : CstOp (0%O : bool^d) := Op_true.
Add Zify CstOp Op_bool_top'.

Instance Op_bool_sub : BinOp (Order.sub : bool -> bool -> bool) :=
{ TBOp := fun x y => x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
{ TBOp x y := x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
Add Zify BinOp Op_bool_sub.

Instance Op_bool_compl : UnOp (Order.compl : bool -> bool) := Op_negb.
Expand Down Expand Up @@ -159,19 +159,19 @@ Instance Op_gtn : BinOp (gtn : nat -> nat -> bool) :=
Add Zify BinOp Op_gtn.

Instance Op_minn : BinOp minn :=
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ?; case: leqP; lia) }.
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leqP; lia) }.
Add Zify BinOp Op_minn.

Instance Op_maxn : BinOp maxn :=
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ?; case: leqP; lia) }.
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leqP; lia) }.
Add Zify BinOp Op_maxn.

Instance Op_nat_of_bool : UnOp nat_of_bool :=
{ TUOp := Z.b2z; TUOpInj := ltac:(by case) }.
Add Zify UnOp Op_nat_of_bool.

Instance Op_double : UnOp double :=
{ TUOp := Z.mul 2; TUOpInj := ltac:(move=> ?; rewrite -muln2; lia) }.
{ TUOp := Z.mul 2; TUOpInj _ := ltac:(rewrite -muln2; lia) }.
Add Zify UnOp Op_double.

Lemma Op_expn_subproof n m : Z.of_nat (n ^ m) = (Z.of_nat n ^ Z.of_nat m)%Z.
Expand Down Expand Up @@ -212,14 +212,14 @@ Instance Op_nat_min : BinOp (Order.min : nat -> _) := Op_minn.
Add Zify BinOp Op_nat_min.

Instance Op_nat_min' : BinOp ((Order.max : nat^d -> _) : nat -> nat -> nat) :=
{ TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
{ TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP; lia) }.
Add Zify BinOp Op_nat_min'.

Instance Op_nat_max : BinOp (Order.max : nat -> _) := Op_maxn.
Add Zify BinOp Op_nat_max.

Instance Op_nat_max' : BinOp ((Order.min : nat^d -> _) : nat -> nat -> nat) :=
{ TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
{ TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP; lia) }.
Add Zify BinOp Op_nat_max'.

Instance Op_nat_meet : BinOp (Order.meet : nat -> _) := Op_minn.
Expand Down Expand Up @@ -254,10 +254,10 @@ Definition divZ (m d : Z) : Z :=

Definition modZ (m d : Z) : Z := (m - divZ m d * d)%Z.

Instance Op_divZ : BinOp divZ := { TBOp := divZ; TBOpInj := fun _ _ => erefl }.
Instance Op_divZ : BinOp divZ := { TBOp := divZ; TBOpInj _ _ := erefl }.
Add Zify BinOp Op_divZ.

Instance Op_modZ : BinOp modZ := { TBOp := modZ; TBOpInj := fun _ _ => erefl }.
Instance Op_modZ : BinOp modZ := { TBOp := modZ; TBOpInj _ _ := erefl }.
Add Zify BinOp Op_modZ.

(* Reimplementation of Z.div_mod_to_equations (PreOmega.v) for divZ and modZ: *)
Expand Down Expand Up @@ -334,27 +334,25 @@ Instance Op_divn : BinOp divn := { TBOp := divZ; TBOpInj := Op_divn_subproof }.
Add Zify BinOp Op_divn.

Instance Op_modn : BinOp modn :=
{ TBOp := modZ; TBOpInj := ltac:(move=> n m; move: (divn_eq n m); lia) }.
{ TBOp := modZ; TBOpInj n m := ltac:(move: (divn_eq n m); lia) }.
Add Zify BinOp Op_modn.

Instance Op_dvdn : BinOp dvdn :=
{ TBOp := fun x y => Z.eqb (modZ y x) 0%Z;
{ TBOp x y := Z.eqb (modZ y x) 0%Z;
TBOpInj := ltac:(rewrite /dvdn; lia) }.
Add Zify BinOp Op_dvdn.

Instance Op_odd : UnOp odd :=
{ TUOp := fun x => Z.eqb (modZ x 2) 1%Z;
TUOpInj := ltac:(move=> n; case: odd (modn2 n); lia) }.
{ TUOp x := Z.eqb (modZ x 2) 1%Z;
TUOpInj n := ltac:(case: odd (modn2 n); lia) }.
Add Zify UnOp Op_odd.

Instance Op_half : UnOp half :=
{ TUOp := fun x => divZ x 2;
TUOpInj := ltac:(move=> ?; rewrite -divn2; lia) }.
{ TUOp x := divZ x 2; TUOpInj _ := ltac:(rewrite -divn2; lia) }.
Add Zify UnOp Op_half.

Instance Op_uphalf : UnOp uphalf :=
{ TUOp := fun x => divZ (x + 1)%Z 2;
TUOpInj := ltac:(move=> ?; rewrite uphalf_half; lia) }.
{ TUOp x := divZ (x + 1)%Z 2; TUOpInj _ := ltac:(rewrite uphalf_half; lia) }.
Add Zify UnOp Op_uphalf.

Lemma Op_gcdn_subproof n m :
Expand Down Expand Up @@ -386,7 +384,7 @@ Instance Op_lcmn : BinOp lcmn := { TBOp := Z.lcm; TBOpInj := Op_lcmn_subproof }.
Add Zify BinOp Op_lcmn.

Instance Op_coprime : BinOp coprime :=
{ TBOp := fun x y => Z.eqb (Z.gcd x y) 1%Z;
{ TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
TBOpInj := ltac:(rewrite /= /coprime; lia) }.
Add Zify BinOp Op_coprime.

Expand All @@ -401,23 +399,23 @@ 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 := fun x y => Z.eqb (modZ x y) 0%Z; TBOpInj := ltac:(simpl; lia) }.
{ TBOp x y := Z.eqb (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 := fun x y => negb (Z.eqb y x) && Z.eqb (modZ y x) 0%Z;
TBOpInj := ltac:(move=> ? ? /=; rewrite sdvdEnat; lia) }.
{ TBOp x y := negb (Z.eqb y x) && Z.eqb (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 := fun x y => negb (Z.eqb x y) && Z.eqb (modZ x y) 0%Z;
TBOpInj := ltac:(move=> ? ? /=; rewrite sdvdEnat; lia) }.
{ TBOp x y := negb (Z.eqb x y) && Z.eqb (modZ x y) 0%Z;
TBOpInj _ _ := ltac:(rewrite /= sdvdEnat; lia) }.
Add Zify BinOp Op_natdvd_gt.

Instance Op_natdvd_gt' : BinOp (<^d%O : rel natdvd^d) := Op_natdvd_gt.
Expand Down

0 comments on commit 9f46d94

Please sign in to comment.