Add the ssrZ library

that provides Z <-> int conversion and some structure instances for Z

Make

@@ -1,3 +1,4 @@
+theories/ssrZ.v
 theories/zify_ssreflect.v
 theories/zify_algebra.v
 theories/zify.v

theories/ssrZ.v

@@ -0,0 +1,137 @@
+From Coq Require Import ZArith ZifyClasses Zify ZifyInst ZifyBool.
+From Coq Require Export Lia.
+
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.
+From mathcomp Require Import order binomial ssralg countalg ssrnum ssrint.
+From mathcomp Require Import zify_ssreflect.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.Theory GRing.Theory Num.Theory.
+
+Definition int_of_Z (n : Z) : int :=
+  match n with
+  | Z0 => Posz 0
+  | Zpos p => Posz (Pos.to_nat p)
+  | Zneg p => Negz (Pos.to_nat p).-1
+  end.
+
+Definition Z_of_int (n : int) : Z :=
+  match n with
+  | Posz n => Z.of_nat n
+  | Negz n' => Z.opp (Z.of_nat (n' + 1))
+  end.
+
+Lemma int_of_ZK : cancel int_of_Z Z_of_int.
+Proof. by case=> //= p; lia. Qed.
+
+Lemma Z_of_intK : cancel Z_of_int int_of_Z.
+Proof.
+case=> [[|n]|n] //=.
+  congr Posz; lia.
+rewrite addnC /=; congr Negz; lia.
+Qed.
+
+Module ZInstances.
+
+Implicit Types (m n : Z).
+
+Fact eqZP : Equality.axiom Z.eqb.
+Proof. by move=> x y; apply: (iffP idP); lia. Qed.
+
+Canonical Z_eqType := EqType Z (EqMixin eqZP).
+Canonical Z_choiceType := ChoiceType Z (CanChoiceMixin int_of_ZK).
+Canonical Z_countType := CountType Z (CanCountMixin int_of_ZK).
+
+Definition Z_zmodMixin :=
+  ZmodMixin Zplus_assoc Zplus_comm Zplus_0_l Zplus_opp_l.
+Canonical Z_zmodType := ZmodType Z Z_zmodMixin.
+
+Definition Z_ringMixin :=
+  RingMixin
+    Zmult_assoc Zmult_1_l Zmult_1_r Zmult_plus_distr_l Zmult_plus_distr_r isT.
+Canonical Z_ringType := RingType Z Z_ringMixin.
+Canonical Z_comRingType := ComRingType Z Zmult_comm.
+
+Definition unitZ := [qualify a n : Z | (n == Z.pos xH) || (n == Z.neg xH)].
+Definition invZ n := n.
+
+Fact mulVZ : {in unitZ, left_inverse 1%R invZ *%R}.
+Proof. by move=> n /pred2P[] ->. Qed.
+
+Fact unitZPl m n : (n * m = 1)%R -> m \is a unitZ.
+Proof. case: m n => [|[m|m|]|[m|m|]] [|n|n] //= []; lia. Qed.
+
+Fact invZ_out : {in [predC unitZ], invZ =1 id}.
+Proof. exact. Qed.
+
+Fact idomain_axiomZ m n : (m * n = 0)%R -> (m == 0%R) || (n == 0%R).
+Proof. by case: m n => [|m|m] []. Qed.
+
+Canonical Z_unitRingType :=
+  UnitRingType Z (ComUnitRingMixin mulVZ unitZPl invZ_out).
+Canonical Z_comUnitRing := [comUnitRingType of Z].
+Canonical Z_idomainType := IdomainType Z idomain_axiomZ.
+
+Canonical Z_countZmodType := [countZmodType of Z].
+Canonical Z_countRingType := [countRingType of Z].
+Canonical Z_countComRingType := [countComRingType of Z].
+Canonical Z_countUnitRingType := [countUnitRingType of Z].
+Canonical Z_countComUnitRingType := [countComUnitRingType of Z].
+Canonical Z_countIdomainType := [countIdomainType of Z].
+
+Fact leZ_add m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m + n). Proof. lia. Qed.
+Fact leZ_mul m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m * n). Proof. lia. Qed.
+Fact leZ_anti m : Z.leb 0 m -> Z.leb m 0 -> m = Z0. Proof. lia. Qed.
+
+Lemma subZ_ge0 m n : Z.leb 0 (n - m)%R = Z.leb m n.
+Proof. by rewrite /GRing.add /GRing.opp /=; lia. Qed.
+
+Fact leZ_total m n : Z.leb m n || Z.leb n m. Proof. lia. Qed.
+
+Fact normZN m : Z.abs (- m) = Z.abs m. Proof. lia. Qed.
+
+Fact geZ0_norm m : Z.leb 0 m -> Z.abs m = m. Proof. lia. Qed.
+
+Fact ltZ_def m n : (Z.ltb m n) = (n != m) && (Z.leb m n).
+Proof. by rewrite eqE /=; lia. Qed.
+
+Definition Mixin : realLeMixin [idomainType of Z] :=
+  RealLeMixin
+    leZ_add leZ_mul leZ_anti subZ_ge0 (leZ_total 0) normZN geZ0_norm ltZ_def.
+
+Canonical Z_porderType := POrderType ring_display Z Mixin.
+Canonical Z_latticeType := LatticeType Z Mixin.
+Canonical Z_distrLatticeType := DistrLatticeType Z Mixin.
+Canonical Z_orderType := OrderType Z leZ_total.
+Canonical Z_numDomaZype := NumDomainType Z Mixin.
+Canonical Z_normedZmodType := NormedZmodType Z Z Mixin.
+Canonical Z_realDomaZype := [realDomainType of Z].
+
+End ZInstances.
+
+Canonical ZInstances.Z_eqType.
+Canonical ZInstances.Z_choiceType.
+Canonical ZInstances.Z_countType.
+Canonical ZInstances.Z_zmodType.
+Canonical ZInstances.Z_ringType.
+Canonical ZInstances.Z_comRingType.
+Canonical ZInstances.Z_unitRingType.
+Canonical ZInstances.Z_comUnitRing.
+Canonical ZInstances.Z_idomainType.
+Canonical ZInstances.Z_countZmodType.
+Canonical ZInstances.Z_countRingType.
+Canonical ZInstances.Z_countComRingType.
+Canonical ZInstances.Z_countUnitRingType.
+Canonical ZInstances.Z_countComUnitRingType.
+Canonical ZInstances.Z_countIdomainType.
+Canonical ZInstances.Z_porderType.
+Canonical ZInstances.Z_latticeType.
+Canonical ZInstances.Z_distrLatticeType.
+Canonical ZInstances.Z_orderType.
+Canonical ZInstances.Z_numDomaZype.
+Canonical ZInstances.Z_normedZmodType.
+Canonical ZInstances.Z_realDomaZype.

theories/zify_algebra.v

@@ -5,7 +5,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.
 From mathcomp Require Import order binomial ssralg countalg ssrnum ssrint rat.
 From mathcomp Require Import intdiv.
-From mathcomp Require Import zify_ssreflect.
+From mathcomp Require Import zify_ssreflect ssrZ.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
 
 Module AlgebraZifyInstances.
 
@@ -17,19 +21,16 @@ Import Order.Theory GRing.Theory Num.Theory SsreflectZifyInstances.
 (* ssrint                                                                     *)
 (******************************************************************************)
 
-Definition Z_of_int (n : int) : Z :=
-  match n with
-  | Posz n => Z.of_nat n
-  | Negz n' => Z.opp (Z.of_nat (n' + 1))
-  end.
-
 Instance Inj_int_Z : InjTyp int Z :=
   { inj := Z_of_int; pred := fun => True; cstr := fun => I }.
 Add Zify InjTyp Inj_int_Z.
 
 Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj := fun => 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 }.
 Add Zify UnOp Op_Posz.
 
@@ -46,7 +47,7 @@ Add Zify BinRel Op_int_eq.
 
 Instance Op_int_eq_op : BinOp (@eq_op int_eqType : int -> int -> bool) :=
   { TBOp := Z.eqb;
-    TBOpInj := ltac:(move=> [] ? [] ?; do 2 rewrite /eq_op /=; lia) }.
+    TBOpInj := ltac:(move=> [] ? [] ?; do 2 rewrite eqE /=; lia) }.
 Add Zify BinOp Op_int_eq_op.
 
 Instance Op_int_0 : CstOp (0%R : int) := { TCst := 0%Z; TCstInj := erefl }.
@@ -76,15 +77,15 @@ Add Zify BinOp Op_mulz.
 Instance Op_int_mulr : BinOp *%R := Op_mulz.
 Add Zify BinOp Op_int_mulr.
 
-Instance Op_int_intmul : BinOp ( *~%R%R : int -> int -> int) :=
-  { TBOp := Z.mul; TBOpInj := ltac:(move=> ? ?; rewrite /= mulrzz; lia) }.
-Add Zify BinOp Op_int_intmul.
-
 Instance Op_int_natmul : BinOp (@GRing.natmul _ : int -> nat -> int) :=
   { TBOp := Z.mul;
     TBOpInj := ltac:(move=> ? ?; 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) }.
+Add Zify BinOp Op_int_intmul.
+
 Instance Op_int_scale : BinOp (@GRing.scale _ [lmodType int of int^o]) :=
   Op_mulz.
 Add Zify BinOp Op_int_scale.
@@ -183,6 +184,126 @@ Add Zify BinOp Op_int_join.
 Instance Op_int_join' : BinOp (Order.meet : int^d -> _) := Op_int_max.
 Add Zify BinOp Op_int_join'.
 
+(******************************************************************************)
+(* ssrZ                                                                       *)
+(******************************************************************************)
+
+Instance Op_Z_eq_op : BinOp (eq_op : Z -> Z -> bool) := Op_Zeqb.
+Add Zify BinOp Op_Z_eq_op.
+
+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 }.
+Add Zify BinOp Op_Z_add.
+
+Instance Op_Z_opp : UnOp (@GRing.opp _ : Z -> Z) :=
+  { TUOp := Z.opp; TUOpInj := fun => 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 }.
+Add Zify BinOp Op_Z_mulr.
+
+Lemma Op_Z_natmul_subproof (n : Z) (m : nat) : (n *+ m)%R = (n * Z.of_nat m)%Z.
+Proof. elim: m => [|m]; rewrite (mulr0n, mulrS); lia. Qed.
+
+Instance Op_Z_natmul : BinOp (@GRing.natmul _ : Z -> nat -> Z) :=
+  { TBOp := Z.mul; TBOpInj := Op_Z_natmul_subproof }.
+Add Zify BinOp Op_Z_natmul.
+
+Instance Op_Z_intmul : BinOp ( *~%R%R : Z -> int -> Z) :=
+  { TBOp := Z.mul; TBOpInj := ltac:(move=> n [] m; rewrite /intmul /=; lia) }.
+Add Zify BinOp Op_Z_intmul.
+
+Instance Op_Z_scale : BinOp (@GRing.scale _ [lmodType Z of Z^o]) := Op_Z_mulr.
+Add Zify BinOp Op_Z_scale.
+
+Lemma Op_Z_exp_subproof n m : (n ^+ m)%R = (n ^ Z.of_nat m)%Z.
+Proof. by rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS. Qed.
+
+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 }.
+Add Zify UnOp Op_invZ.
+
+Instance Op_Z_inv : UnOp (GRing.inv : Z -> Z) :=
+  { TUOp := id; TUOpInj := fun => erefl }.
+Add Zify UnOp Op_Z_inv.
+
+Instance Op_Z_normr : UnOp (Num.norm : Z -> Z) :=
+  { TUOp := Z.abs; TUOpInj := fun => 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 }.
+Add Zify BinOp Op_Z_le.
+
+Instance Op_Z_le' : BinOp (>=^d%O : rel Z^d) := Op_Z_le.
+Add Zify BinOp Op_Z_le'.
+
+Instance Op_Z_ge : BinOp (>=%O : Z -> Z -> bool) :=
+  { TBOp := Z.geb; TBOpInj := ltac:(simpl; lia) }.
+Add Zify BinOp Op_Z_ge.
+
+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 }.
+Add Zify BinOp Op_Z_lt.
+
+Instance Op_Z_lt' : BinOp (>^d%O : rel Z^d) := Op_Z_lt.
+Add Zify BinOp Op_Z_lt'.
+
+Instance Op_Z_gt : BinOp (>%O : Z -> Z -> bool) :=
+  { TBOp := Z.gtb; TBOpInj := ltac:(simpl; lia) }.
+Add Zify BinOp Op_Z_gt.
+
+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) }.
+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) }.
+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) }.
+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) }.
+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) }.
+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) }.
+Add Zify BinOp Op_Z_join.
+
+Instance Op_Z_join' : BinOp (Order.meet : Z^d -> _) := Op_Z_max.
+Add Zify BinOp Op_Z_join'.
+
 (******************************************************************************)
 (* intdiv                                                                     *)
 (******************************************************************************)
@@ -231,8 +352,8 @@ Add Zify UnOp Op_int_opp.
 Add Zify CstOp Op_int_1.
 Add Zify BinOp Op_mulz.
 Add Zify BinOp Op_int_mulr.
-Add Zify BinOp Op_int_intmul.
 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_invz.
@@ -259,6 +380,36 @@ Add Zify BinOp Op_int_meet.
 Add Zify BinOp Op_int_meet'.
 Add Zify BinOp Op_int_join.
 Add Zify BinOp Op_int_join'.
+Add Zify BinOp Op_Z_eq_op.
+Add Zify CstOp Op_Z_0.
+Add Zify BinOp Op_Z_add.
+Add Zify UnOp Op_Z_opp.
+Add Zify CstOp Op_Z_1.
+Add Zify BinOp Op_Z_mulr.
+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_invZ.
+Add Zify UnOp Op_Z_inv.
+Add Zify UnOp Op_Z_normr.
+Add Zify UnOp Op_Z_sgr.
+Add Zify BinOp Op_Z_le.
+Add Zify BinOp Op_Z_le'.
+Add Zify BinOp Op_Z_ge.
+Add Zify BinOp Op_Z_ge'.
+Add Zify BinOp Op_Z_lt.
+Add Zify BinOp Op_Z_lt'.
+Add Zify BinOp Op_Z_gt.
+Add Zify BinOp Op_Z_gt'.
+Add Zify BinOp Op_Z_min.
+Add Zify BinOp Op_Z_min'.
+Add Zify BinOp Op_Z_max.
+Add Zify BinOp Op_Z_max'.
+Add Zify BinOp Op_Z_meet.
+Add Zify BinOp Op_Z_meet'.
+Add Zify BinOp Op_Z_join.
+Add Zify BinOp Op_Z_join'.
 Add Zify BinOp Op_divz.
 Add Zify BinOp Op_modz.
 Add Zify BinOp Op_dvdz.