Merge PR #18729: zify Nat.double and Nat.div2

Reviewed-by: fajb Co-authored-by: fajb <fajb@users.noreply.github.com>
coq · Apr 16, 2024 · c1f50fd · c1f50fd
2 parents 5caa30f + 8c8c7bb
commit c1f50fd
Show file tree

Hide file tree

Showing 5 changed files with 30 additions and 2 deletions.
diff --git a/doc/changelog/04-tactics/18729-zify-nat-double-halve.rst b/doc/changelog/04-tactics/18729-zify-nat-double-halve.rst
@@ -0,0 +1,4 @@
+- **Added:** support for :g:`Nat.double` and :g:`Nat.div2` to :g:`zify` and
+  :g:`lia`
+  (`#18729 <https://github.com/coq/coq/pull/18729>`_,
+  by Andres Erbsen).
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
@@ -143,8 +143,14 @@ Proof.
   lia.
 Qed.
 
+Goal forall n, Nat.double n = n + n.
+Proof. lia. Qed.
+
 Open Scope Z_scope.
 
+Goal forall n, Z.of_nat (Nat.div2 n) = Z.of_nat n / 2.
+Proof. lia. Qed.
+
 Goal forall p,
     False ->
     (Pos.to_nat p)  = 0%nat.

diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
@@ -324,10 +324,11 @@ Proof.
     apply Rmult_le_reg_l with (Rsqr (INR (Nat.div2 (S N)))).
     { apply Rsqr_pos_lt.
       apply not_O_INR; red; intro.
-      lia. }
+      PreOmega.zify; PreOmega.Z.to_euclidean_division_equations; lia. }
     repeat rewrite <- Rmult_assoc.
     rewrite Rinv_r.
-    2:{ unfold Rsqr; apply prod_neq_R0; apply not_O_INR;lia. }
+    2:{ unfold Rsqr; apply prod_neq_R0; apply not_O_INR;
+      PreOmega.zify; PreOmega.Z.to_euclidean_division_equations; lia. }
     rewrite Rmult_1_l.
     change 4 with (Rsqr 2).
     rewrite <- Rsqr_mult.

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.mul 2 ; TUOpInj := Nat2Z.inj_double |}.
+Add Zify UnOp Op_nat_double.
+
 (** Support for positive *)
 
 #[global]