add Proper instances for some number theorems to improve rewriting wi…

…th inequalities
haansn08 · Apr 17, 2024 · 569b187 · 569b187
1 parent 3964411
commit 569b187
Show file tree

Hide file tree

Showing 10 changed files with 38 additions and 0 deletions.
diff --git a/doc/changelog/11-standard-library/16792-proper_instances1.rst b/doc/changelog/11-standard-library/16792-proper_instances1.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Add :g:`Proper` instances for some number theorems to improve rewriting with inequalities.
+  (`#16792 <https://github.com/coq/coq/pull/16792>`_,
+  by Stefan Haan with help from Jason Gross, Andrej Dudenhefner and Paolo G. Giarrusso).
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
@@ -1254,6 +1254,10 @@ Infix "?=" := Nat.compare (at level 70) : nat_scope.
 Infix "/" := Nat.div : nat_scope.
 Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
 
+(** Re-export [Nat] hints *)
+
+Export (hints) Nat.
+
 #[global] Hint Unfold Nat.le : core.
 #[global] Hint Unfold Nat.lt : core.
 

diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
@@ -59,6 +59,9 @@ apply le_trans with (m + p);
 [now apply add_le_mono_r | now apply add_le_mono_l].
 Qed.
 
+#[export] Instance _add_le_mono: Proper (le ==> le ==> le) add.
+Proof. now simpl_relation; apply add_le_mono. Qed.
+
 Theorem add_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.

diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
@@ -188,6 +188,9 @@ Proof.
    apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos.
 Qed.
 
+#[export] Instance _log2_le_mono: Proper (le ==> le) log2.
+Proof. simpl_relation. now apply log2_le_mono. Qed.
+
 (** No reverse result for <=, consider for instance log2 3 <= log2 2 *)
 
 Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b.
@@ -641,6 +644,9 @@ Proof.
    rewrite 2 lt_succ_pred with 1; order.
 Qed.
 
+#[export] Instance _log2_up_le_mono: Proper (le ==> le) log2_up.
+Proof. simpl_relation. now apply log2_up_le_mono. Qed.
+
 (** No reverse result for <=, consider for instance log2_up 4 <= log2_up 3 *)
 
 Lemma log2_up_lt_cancel : forall a b, log2_up a < log2_up b -> a < b.

diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
@@ -547,6 +547,9 @@ Proof.
    apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order.
 Qed.
 
+#[export] Instance _sqrt_up_le_mono: Proper (le ==> le) sqrt_up.
+Proof. simpl_relation. now apply sqrt_up_le_mono. Qed.
+
 (** No reverse result for <=, consider for instance √°3 <= √°2 *)
 
 Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b.

diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -56,6 +56,9 @@ Proof.
 intros; apply mul_le_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
+#[export] Instance _mul_le_mono: Proper (le ==> le ==> le) mul.
+Proof. now simpl_relation; apply mul_le_mono. Qed.
+
 Theorem lt_0_mul' : forall n m, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].

diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -213,6 +213,9 @@ intros n m H; elim H using le_ind_rel.
 - intros p q H1 _; now do 2 rewrite pred_succ.
 Qed.
 
+#[export] Instance _pred_le_mono: Proper (le ==> le) pred.
+Proof. simpl_relation. now apply pred_le_mono. Qed.
+
 Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m).
 Proof.
 intros n m H1; split; intro H2.

diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
@@ -77,6 +77,9 @@ Proof. wrap pow_lt_mono_l. Qed.
 Lemma pow_le_mono_l : forall a b c, a<=b -> a^c <= b^c.
 Proof. wrap pow_le_mono_l. Qed.
 
+#[export] Instance _pow_le_mono_l: Proper (le ==> eq ==> le) pow.
+Proof. intros a b H _ c ->. now apply pow_le_mono_l. Qed.
+
 Lemma pow_gt_1 : forall a b, 1<a -> b~=0 -> 1<a^b.
 Proof. wrap pow_gt_1. Qed.
 

diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -33,6 +33,9 @@ Proof. wrap sqrt_square. Qed.
 Definition sqrt_le_mono : forall a b, a<=b -> √a <= √b
  := sqrt_le_mono.
 
+#[export] Instance _sqrt_le_mono: Proper (le ==> le) sqrt.
+Proof. simpl_relation. now apply sqrt_le_mono. Qed.
+
 Definition sqrt_lt_cancel : forall a b, √a < √b -> a < b
  := sqrt_lt_cancel.
 

diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
@@ -228,12 +228,18 @@ Proof.
  - apply sub_add_le.
 Qed.
 
+#[export] Instance _sub_le_mono_r: Proper (le ==> eq ==> le) sub.
+Proof. intros x x' Hx y y' Hy. rewrite Hy. now apply sub_le_mono_r. Qed.
+
 Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n.
 Proof.
  intros n m p. rewrite le_sub_le_add_r.
  transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l].
 Qed.
 
+#[export] Instance _sub_le_mono_l: Proper (eq ==> le --> le) sub.
+Proof. intros x x' Hx y y' Hy. rewrite Hx. now apply sub_le_mono_l. Qed.
+
 (** Sub and mul *)
 
 Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.