diff --git a/examples/test_algebra.v b/examples/test_algebra.v index 2d26d0d..1b241ef 100644 --- a/examples/test_algebra.v +++ b/examples/test_algebra.v @@ -7,6 +7,42 @@ Unset Printing Implicit Defensive. Local Delimit Scope Z_scope with Z. +Fact test_zero_nat : Z.of_nat 0%R = 0%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_add_nat n m : Z.of_nat (n + m)%R = (Z.of_nat n + Z.of_nat m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_one_nat : Z.of_nat 1%R = 1%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_mul_nat n m : Z.of_nat (n * m)%R = (Z.of_nat n * Z.of_nat m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_natmul_nat n m : Z.of_nat (n *+ m)%R = (Z.of_nat n * Z.of_nat m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_exp_nat n m : Z.of_nat (n ^+ m)%R = (Z.of_nat n ^ Z.of_nat m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_zero_N : Z.of_N 0%R = 0%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_add_N n m : Z.of_N (n + m)%R = (Z.of_N n + Z.of_N m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_one_N : Z.of_N 1%R = 1%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_mul_N n m : Z.of_N (n * m)%R = (Z.of_N n * Z.of_N m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_natmul_N n m : Z.of_N (n *+ m)%R = (Z.of_N n * Z.of_nat m)%Z. +Proof. zify_op; reflexivity. Qed. + +Fact test_exp_N n m : Z.of_N (n ^+ m)%R = (Z.of_N n ^ Z.of_nat m)%Z. +Proof. zify_op; reflexivity. Qed. + Fact test_unit_int m : m \is a GRing.unit = (Z_of_int m =? 1)%Z || (Z_of_int m =? - 1)%Z. Proof. zify_pre_hook; zify_op; reflexivity. Qed. diff --git a/examples/test_ssreflect.v b/examples/test_ssreflect.v index 09deb5a..07e6ce4 100644 --- a/examples/test_ssreflect.v +++ b/examples/test_ssreflect.v @@ -63,6 +63,8 @@ Proof. zify_op; reflexivity. Qed. Fact test_dual_max_bool (b1 b2 : bool^d) : Order.dual_max b1 b2 = b1 && b2. Proof. zify_op; reflexivity. Qed. +(* FIXME: meet and join below are broken but the tests pass because they are *) +(* convertible anyway. *) Fact test_meet_bool b1 b2 : (b1 `&` b2)%O = b1 && b2. Proof. zify_op; reflexivity. Qed. @@ -75,17 +77,17 @@ Proof. zify_op; reflexivity. Qed. Fact test_dual_join_bool (b1 b2 : bool^d) : (b1 `|^d` b2)%O = b1 && b2. Proof. zify_op; reflexivity. Qed. -Fact test_bottom_bool : 0%O = false :> bool. +Fact test_bottom_bool : \bot%O = false :> bool. Proof. zify_op; reflexivity. Qed. -Fact test_top_bool : 1%O = true :> bool. +Fact test_top_bool : \top%O = true :> bool. Proof. zify_op; reflexivity. Qed. (* FIXME: Notations 0^d and 1^d are broken. *) -Fact test_dual_bottom_bool : 0%O = true :> bool^d. +Fact test_dual_bottom_bool : \bot%O = true :> bool^d. Proof. zify_op; reflexivity. Qed. -Fact test_dual_top_bool : 1%O = false :> bool^d. +Fact test_dual_top_bool : \top%O = false :> bool^d. Proof. zify_op; reflexivity. Qed. Fact test_sub_bool b1 b2 : (b1 `\` b2)%O = b1 && ~~ b2. @@ -235,7 +237,7 @@ Fact test_dual_join_nat (n m : nat^d) : Z.of_nat (n `|^d` m)%O = Z.min (Z.of_nat n) (Z.of_nat m). Proof. zify_op; reflexivity. Qed. -Fact test_bottom_nat : Z.of_nat 0%O = 0%Z. +Fact test_bottom_nat : Z.of_nat \bot%O = 0%Z. Proof. zify_op; reflexivity. Qed. (******************************************************************************) @@ -315,15 +317,14 @@ Fact test_dual_join_natdvd (n m : natdvd^d) : Z.of_nat (n `|` m)%O = Z.gcd (Z.of_nat n) (Z.of_nat m). Proof. zify_op; reflexivity. Qed. -Fact test_bottom_natdvd : Z.of_nat (0%O : natdvd) = 1%Z. +Fact test_bottom_natdvd : Z.of_nat (\bot%O : natdvd) = 1%Z. Proof. zify_op; reflexivity. Qed. -Fact test_top_natdvd : Z.of_nat (1%O : natdvd) = 0%Z. +Fact test_top_natdvd : Z.of_nat (\top%O : natdvd) = 0%Z. Proof. zify_op; reflexivity. Qed. -(* FIXME: Notations 0^d and 1^d are broken. *) -Fact test_dual_bottom_natdvd : Z.of_nat (0%O : natdvd^d) = 0%Z. +Fact test_dual_bottom_natdvd : Z.of_nat (\bot^d%O : natdvd^d) = 0%Z. Proof. zify_op; reflexivity. Qed. -Fact test_dual_top_natdvd : Z.of_nat (1%O : natdvd^d) = 1%Z. +Fact test_dual_top_natdvd : Z.of_nat (\top^d%O : natdvd^d) = 1%Z. Proof. zify_op; reflexivity. Qed. diff --git a/theories/ssrZ.v b/theories/ssrZ.v index d14c6b5..4456155 100644 --- a/theories/ssrZ.v +++ b/theories/ssrZ.v @@ -35,7 +35,78 @@ case=> [[|n]|n] //=. rewrite addnC /=; congr Negz; lia. Qed. -Module ZInstances. +Module Instances. + +(* Instances taken from math-comp/math-comp#1031, authored by Pierre Roux *) +(* TODO: remove them when we drop support for MathComp 2.0 *) +#[export] +HB.instance Definition _ := GRing.isNmodule.Build nat addnA addnC add0n. + +#[export] +HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build nat + mulnA mulnC mul1n mulnDl mul0n erefl. + +#[export] +HB.instance Definition _ (V : nmodType) (x : V) := + GRing.isSemiAdditive.Build nat V (GRing.natmul x) (mulr0n x, mulrnDr x). + +#[export] +HB.instance Definition _ (R : semiRingType) := + GRing.isMultiplicative.Build nat R (GRing.natmul 1) (natrM R, mulr1n 1). + +Fact Posz_is_semi_additive : semi_additive Posz. +Proof. by []. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build nat int Posz + Posz_is_semi_additive. + +Fact Posz_is_multiplicative : multiplicative Posz. +Proof. by []. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build nat int Posz + Posz_is_multiplicative. +(* end *) + +#[export] +HB.instance Definition _ := Countable.copy N (can_type nat_of_binK). + +#[export] +HB.instance Definition _ := GRing.isNmodule.Build N + Nplus_assoc Nplus_comm Nplus_0_l. + +#[export] +HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build N + Nmult_assoc Nmult_comm Nmult_1_l Nmult_plus_distr_r N.mul_0_l isT. + +Fact bin_of_nat_is_semi_additive : semi_additive bin_of_nat. +Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build nat N bin_of_nat + bin_of_nat_is_semi_additive. + +Fact nat_of_bin_is_semi_additive : semi_additive nat_of_bin. +Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build N nat nat_of_bin + nat_of_bin_is_semi_additive. + +Fact bin_of_nat_is_multiplicative : multiplicative bin_of_nat. +Proof. by split => // m n; rewrite /GRing.mul /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build nat N bin_of_nat + bin_of_nat_is_multiplicative. + +Fact nat_of_bin_is_multiplicative : multiplicative nat_of_bin. +Proof. exact: can2_rmorphism bin_of_natK nat_of_binK. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build N nat nat_of_bin + nat_of_bin_is_multiplicative. Implicit Types (m n : Z). @@ -121,7 +192,7 @@ HB.instance Definition _ := GRing.isAdditive.Build Z int int_of_Z int_of_Z_is_additive. Fact Z_of_int_is_multiplicative : multiplicative Z_of_int. -Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed. +Proof. by split => // m n; rewrite !Z_of_intE rmorphM. Qed. #[export] HB.instance Definition _ := GRing.isMultiplicative.Build int Z Z_of_int @@ -134,8 +205,36 @@ Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed. HB.instance Definition _ := GRing.isMultiplicative.Build Z int int_of_Z int_of_Z_is_multiplicative. +Fact Z_of_nat_is_semi_additive : semi_additive Z.of_nat. +Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build nat Z Z.of_nat + Z_of_nat_is_semi_additive. + +Fact Z_of_nat_is_multiplicative : multiplicative Z.of_nat. +Proof. by split => // m n; rewrite /GRing.mul /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build nat Z Z.of_nat + Z_of_nat_is_multiplicative. + +Fact Z_of_N_is_semi_additive : semi_additive Z.of_N. +Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build N Z Z.of_N + Z_of_N_is_semi_additive. + +Fact Z_of_N_is_multiplicative : multiplicative Z.of_N. +Proof. by split => // m n; rewrite /GRing.mul /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build N Z Z.of_N + Z_of_N_is_multiplicative. + Module Exports. HB.reexport. End Exports. -End ZInstances. +End Instances. -Export ZInstances.Exports. +Export Instances.Exports. diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v index 6aad53f..47215ff 100644 --- a/theories/zify_algebra.v +++ b/theories/zify_algebra.v @@ -17,6 +17,86 @@ Local Delimit Scope Z_scope with Z. Import Order.Theory GRing.Theory Num.Theory SsreflectZifyInstances. +(* TODO: remove natn below when we drop support for MathComp 2.0 *) +Local Lemma natn n : n%:R%R = n :> nat. +Proof. by elim: n => // n; rewrite mulrS => ->. Qed. + +(******************************************************************************) +(* nat *) +(******************************************************************************) + +#[global] +Instance Op_nat_0 : CstOp (0%R : nat) := ZifyInst.Op_O. +Add Zify CstOp Op_nat_0. + +#[global] +Instance Op_nat_add : BinOp (+%R : nat -> nat -> nat) := Op_addn. +Add Zify BinOp Op_nat_add. + +#[global] +Instance Op_nat_1 : CstOp (1%R : nat) := { TCst := 1%Z; TCstInj := erefl }. +Add Zify CstOp Op_nat_1. + +#[global] +Instance Op_nat_mul : BinOp ( *%R : nat -> nat -> nat) := Op_muln. +Add Zify BinOp Op_nat_mul. + +Fact Op_nat_natmul_subproof (n m : nat) : + Z.of_nat (n *+ m)%R = (Z.of_nat n * Z.of_nat m)%Z. +Proof. by rewrite raddfMn -mulr_natr -[m in RHS]natn rmorph_nat. Qed. + +#[global] +Instance Op_nat_natmul : BinOp (@GRing.natmul _ : nat -> nat -> nat) := + { TBOp := Z.mul; TBOpInj := Op_nat_natmul_subproof }. +Add Zify BinOp Op_nat_natmul. + +Fact Op_nat_exp_subproof (n : nat) (m : nat) : + Z_of_nat (n ^+ m)%R = (Z_of_int n ^ Z.of_nat m)%Z. +Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed. + +#[global] +Instance Op_nat_exp : BinOp (@GRing.exp _ : nat -> nat -> nat) := + { TBOp := Z.pow; TBOpInj := Op_nat_exp_subproof }. +Add Zify BinOp Op_nat_exp. + +(******************************************************************************) +(* N *) +(******************************************************************************) + +#[global] +Instance Op_N_0 : CstOp (0%R : N) := ZifyInst.Op_N_N0. +Add Zify CstOp Op_N_0. + +#[global] +Instance Op_N_add : BinOp (+%R : N -> N -> N) := ZifyInst.Op_N_add. +Add Zify BinOp Op_N_add. + +#[global] +Instance Op_N_1 : CstOp (1%R : N) := { TCst := 1%Z; TCstInj := erefl }. +Add Zify CstOp Op_N_1. + +#[global] +Instance Op_N_mul : BinOp ( *%R : N -> N -> N) := ZifyInst.Op_N_mul. +Add Zify BinOp Op_N_mul. + +Fact Op_N_natmul_subproof (n : N) (m : nat) : + Z.of_N (n *+ m)%R = (Z.of_N n * Z.of_nat m)%Z. +Proof. by rewrite raddfMn -mulr_natr -[m in RHS]natn rmorph_nat. Qed. + +#[global] +Instance Op_N_natmul : BinOp (@GRing.natmul _ : N -> nat -> N) := + { TBOp := Z.mul; TBOpInj := Op_N_natmul_subproof }. +Add Zify BinOp Op_N_natmul. + +Fact Op_N_exp_subproof (n : N) (m : nat) : + Z_of_N (n ^+ m)%R = (Z_of_N n ^ Z.of_nat m)%Z. +Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed. + +#[global] +Instance Op_N_exp : BinOp (@GRing.exp _ : N -> nat -> N) := + { TBOp := Z.pow; TBOpInj := Op_N_exp_subproof }. +Add Zify BinOp Op_N_exp. + (******************************************************************************) (* ssrint *) (******************************************************************************) @@ -287,7 +367,7 @@ Instance Op_Z_exp : BinOp (@GRing.exp _ : Z -> nat -> Z) := Add Zify BinOp Op_Z_exp. #[global] -Instance Op_unitZ : UnOp (has_quality 1 ZInstances.unitZ : Z -> bool) := +Instance Op_unitZ : UnOp (has_quality 1 Instances.unitZ : Z -> bool) := { TUOp x := (x =? 1)%Z || (x =? - 1)%Z; TUOpInj _ := erefl }. Add Zify UnOp Op_unitZ. @@ -296,7 +376,7 @@ Instance Op_Z_unit : UnOp (has_quality 1 GRing.unit : Z -> bool) := Op_unitZ. Add Zify UnOp Op_Z_unit. #[global] -Instance Op_invZ : UnOp ZInstances.invZ := { TUOp := id; TUOpInj _ := erefl }. +Instance Op_invZ : UnOp Instances.invZ := { TUOp := id; TUOpInj _ := erefl }. Add Zify UnOp Op_invZ. #[global] @@ -427,6 +507,18 @@ Instance Op_coprimez : BinOp coprimez := Add Zify BinOp Op_coprimez. Module Exports. +Add Zify CstOp Op_nat_0. +Add Zify BinOp Op_nat_add. +Add Zify CstOp Op_nat_1. +Add Zify BinOp Op_nat_mul. +Add Zify BinOp Op_nat_natmul. +Add Zify BinOp Op_nat_exp. +Add Zify CstOp Op_N_0. +Add Zify BinOp Op_N_add. +Add Zify CstOp Op_N_1. +Add Zify BinOp Op_N_mul. +Add Zify BinOp Op_N_natmul. +Add Zify BinOp Op_N_exp. Add Zify InjTyp Inj_int_Z. Add Zify UnOp Op_Z_of_int. Add Zify UnOp Op_Posz.