zify Nat.double and Nat.div2

coq · Feb 28, 2024 · 2f227a4 · 2f227a4
1 parent de96efa
commit 2f227a4
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 1 deletion.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
@@ -14,7 +14,7 @@ Require Import SeqSeries.
 Require Import Rtrigo1.
 Require Import Ranalysis1.
 Require Import PSeries_reg.
-Require Import Lia Lra.
+Require Import Lia ZifyNat Lra.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 

diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
@@ -768,6 +768,12 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_pow, N2Z.inj_pow.
 Qed.
 
+Lemma inj_div2 n : Z.of_nat (Nat.div2 n) = Z.div2 (Z.of_nat n).
+Proof. rewrite Nat.div2_div, Z.div2_div, inj_div; trivial. Qed.
+
+Lemma inj_double n : Z.of_nat (Nat.double n) = Z.double (Z.of_nat n).
+Proof. rewrite Nat.double_twice, Z.double_spec, inj_mul; trivial. Qed.
+
 End Nat2Z.
 
 Module Z2Nat.

diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
@@ -119,6 +119,17 @@ Instance Op_Z_abs_nat : UnOp  Z.abs_nat :=
   { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }.
 Add Zify UnOp Op_Z_abs_nat.
 
+#[global]
+Instance Op_nat_div2 : UnOp Nat.div2 :=
+  { TUOp x := x / 2 ;
+    TUOpInj x := ltac:(now rewrite Nat2Z.inj_div2, Z.div2_div) }.
+Add Zify UnOp Op_nat_div2.
+
+#[global]
+Instance Op_nat_double : UnOp Nat.double :=
+  {| TUOp := Z.double ; TUOpInj := Nat2Z.inj_double |}.
+Add Zify UnOp Op_nat_double.
+
 (** Support for positive *)
 
 #[global]