Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hello,

I have just noticed that ssrnum exports the following notations:

Notation ">%R" := lt : ring_scope.
Notation "<%R" := gt : ring_scope.
Notation ">=%R" := le : ring_scope.
Notation "<=%R" := ge : ring_scope.

It seems to me that lt/gt and le/ge should be permuted, because the
current mapping of these notations is misleading.  For instance,

Require Import ssreflect ssrfun ssrbool eqtype ssrnat ssralg ssrnum ssrint.
Open Scope ring_scope.
Eval compute in (<=%R) 0%:Z 1%:Z.

returns false. But in OCaml IIRC, the phrase (<=) 0 1;; is the same as
0 <= 1;; and will return true.

I enclose a small patch for this issue, in case you would like to fix
it for the pending release of MathComp.

Kind regards,

Erik

--
Érik Martin-Dorel
Post-doctorant, Équipe-projet Marelle
Inria Sophia Antipolis - Méditerranée
http://erik.martin-dorel.org/

diff -ru a/mathcomp-1.5/theories/ssrint.v b/mathcomp-1.5/theories/ssrint.v
--- a/mathcomp-1.5/theories/ssrint.v	2013-08-07 18:06:50.000000000 +0200
+++ b/mathcomp-1.5/theories/ssrint.v	2013-08-23 11:22:50.081618541 +0200
@@ -1195,14 +1195,14 @@
 Definition exprz_gte0 := (exprz_ge0, exprz_gt0).
 
 Lemma ler_wpiexpz2l x (x0 : 0 <= x) (x1 : x <= 1) :
-  {in >=%R 0 &, {homo (exprz x) : x y /~ x <= y}}.
+  {in <=%R 0 &, {homo (exprz x) : x y /~ x <= y}}.
 Proof.
 move=> [] m [] n; rewrite -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _.
 by rewrite lez_nat -?exprnP=> /ler_wiexpn2l; apply.
 Qed.
 
 Lemma ler_wniexpz2l x (x0 : 0 <= x) (x1 : x <= 1) :
-  {in <%R 0 &, {homo (exprz x) : x y /~ x <= y}}.
+  {in >%R 0 &, {homo (exprz x) : x y /~ x <= y}}.
 Proof.
 move=> [] m [] n; rewrite ?NegzE -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _.
 rewrite ler_opp2 lez_nat -?invr_expz=> hmn; move: (x0).
@@ -1211,14 +1211,14 @@
 Qed.
 
 Fact ler_wpeexpz2l x (x1 : 1 <= x) :
-  {in >=%R 0 &, {homo (exprz x) : x y / x <= y}}.
+  {in <=%R 0 &, {homo (exprz x) : x y / x <= y}}.
 Proof.
 move=> [] m [] n; rewrite -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _.
 by rewrite lez_nat -?exprnP=> /ler_weexpn2l; apply.
 Qed.
 
 Fact ler_wneexpz2l x (x1 : 1 <= x) :
-  {in <=%R 0 &, {homo (exprz x) : x y / x <= y}}.
+  {in >=%R 0 &, {homo (exprz x) : x y / x <= y}}.
 Proof.
 move=> m n hm hn /= hmn.
 rewrite -lef_pinv -?topredE /= ?exprz_gt0 ?(ltr_le_trans ltr01) //.
@@ -1250,7 +1250,7 @@
 Qed.
 
 Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
-  {in >=%R 0 &, {mono (exprz x) : x y /~ x <= y}}.
+  {in <=%R 0 &, {mono (exprz x) : x y /~ x <= y}}.
 Proof.
 apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)).
   by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF.
@@ -1258,11 +1258,11 @@
 Qed.
 
 Lemma ltr_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
-  {in >=%R 0 &, {mono (exprz x) : x y /~ x < y}}.
+  {in <=%R 0 &, {mono (exprz x) : x y /~ x < y}}.
 Proof. exact: (lerW_nmono_in (ler_piexpz2l _ _)). Qed.
 
 Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
-  {in <%R 0 &, {mono (exprz x) : x y /~ x <= y}}.
+  {in >%R 0 &, {mono (exprz x) : x y /~ x <= y}}.
 Proof.
 apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)).
   by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF.
@@ -1270,7 +1270,7 @@
 Qed.
 
 Lemma ltr_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
-  {in <%R 0 &, {mono (exprz x) : x y /~ x < y}}.
+  {in >%R 0 &, {mono (exprz x) : x y /~ x < y}}.
 Proof. exact: (lerW_nmono_in (ler_niexpz2l _ _)). Qed.
 
 Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x <= y}.
@@ -1284,17 +1284,17 @@
 Proof. exact: (lerW_mono (ler_eexpz2l _)). Qed.
 
 Lemma ler_wpexpz2r n (hn : 0 <= n) :
-{in >=%R 0 & , {homo ((@exprz R)^~ n) : x y / x <= y}}.
+{in <=%R 0 & , {homo ((@exprz R)^~ n) : x y / x <= y}}.
 Proof. by case: n hn=> // n _; apply: ler_expn2r. Qed.
 
 Lemma ler_wnexpz2r n (hn : n <= 0) :
-{in >%R 0 & , {homo ((@exprz R)^~ n) : x y /~ x <= y}}.
+{in <%R 0 & , {homo ((@exprz R)^~ n) : x y /~ x <= y}}.
 Proof.
 move=> x y /= hx hy hxy; rewrite -lef_pinv ?[_ \in _]exprz_gt0 //.
 by rewrite !invr_expz ler_wpexpz2r  ?[_ \in _]ltrW // oppr_cp0.
 Qed.
 
-Lemma pexpIrz n (n0 : n != 0) : {in >=%R 0 &, injective ((@exprz R)^~ n)}.
+Lemma pexpIrz n (n0 : n != 0) : {in <=%R 0 &, injective ((@exprz R)^~ n)}.
 Proof.
 move=> x y; rewrite ![_ \in _]le0r=> /orP [/eqP-> _ /eqP|hx].
   by rewrite exp0rz ?(negPf n0) eq_sym expfz_eq0=> /andP [_ /eqP->].
@@ -1306,7 +1306,7 @@
 by rewrite (can2_eq (mulrVK _) (mulrK _)) ?unitfE ?(gtr_eqF hy) // mul1r=> /eqP.
 Qed.
 
-Lemma nexpIrz n (n0 : n != 0) : {in <=%R 0 &, injective ((@exprz R)^~ n)}.
+Lemma nexpIrz n (n0 : n != 0) : {in >=%R 0 &, injective ((@exprz R)^~ n)}.
 Proof.
 move=> x y; rewrite ![_ \in _]ler_eqVlt => /orP [/eqP -> _ /eqP|hx].
   by rewrite exp0rz ?(negPf n0) eq_sym expfz_eq0=> /andP [_ /eqP->].
@@ -1319,7 +1319,7 @@
 Qed.
 
 Lemma ler_pexpz2r n (hn : 0 < n) :
-  {in >=%R 0 & , {mono ((@exprz R)^~ n) : x y / x <= y}}.
+  {in <=%R 0 & , {mono ((@exprz R)^~ n) : x y / x <= y}}.
 Proof.
 apply: homo_mono_in (homo_inj_in_lt _ _).
   by move=> x y hx hy /=; apply: pexpIrz; rewrite // gtr_eqF.
@@ -1327,11 +1327,11 @@
 Qed.
 
 Lemma ltr_pexpz2r n (hn : 0 < n) :
-  {in >=%R 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
+  {in <=%R 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
 Proof. exact: lerW_mono_in (ler_pexpz2r _). Qed.
 
 Lemma ler_nexpz2r n (hn : n < 0) :
-  {in >%R 0 & , {mono ((@exprz R)^~ n) : x y /~ x <= y}}.
+  {in <%R 0 & , {mono ((@exprz R)^~ n) : x y /~ x <= y}}.
 Proof.
 apply: nhomo_mono_in (nhomo_inj_in_lt _ _); last first.
   by apply: ler_wnexpz2r; rewrite ltrW.
@@ -1339,7 +1339,7 @@
 Qed.
 
 Lemma ltr_nexpz2r n (hn : n < 0) :
-  {in >%R 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.
+  {in <%R 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.
 Proof. exact: lerW_nmono_in (ler_nexpz2r _). Qed.
 
 Lemma eqr_expz2 n x y : n != 0 -> 0 <= x -> 0 <= y ->
diff -ru a/mathcomp-1.5/theories/ssrnum.v b/mathcomp-1.5/theories/ssrnum.v
--- a/mathcomp-1.5/theories/ssrnum.v	2013-08-05 18:52:25.000000000 +0200
+++ b/mathcomp-1.5/theories/ssrnum.v	2013-08-23 11:20:59.836394246 +0200
@@ -244,10 +244,10 @@
 
 Notation "`| x |" := (norm x) : ring_scope.
 
-Notation ">%R" := lt : ring_scope.
-Notation "<%R" := gt : ring_scope.
-Notation ">=%R" := le : ring_scope.
-Notation "<=%R" := ge : ring_scope.
+Notation "<%R" := lt : ring_scope.
+Notation ">%R" := gt : ring_scope.
+Notation "<=%R" := le : ring_scope.
+Notation ">=%R" := ge : ring_scope.
 Notation "<?=%R" := lerif : ring_scope.
 
 Notation "x < y"  := (lt x y) : ring_scope.
@@ -1096,7 +1096,7 @@
 
 (* Ordered ring properties. *)
 
-Lemma ler_asym : antisymmetric (>=%R : rel R).
+Lemma ler_asym : antisymmetric (<=%R : rel R).
 Proof.
 move=> x y; rewrite !ler_def distrC -opprB -addr_eq0 => /andP[/eqP->].
 by rewrite -mulr2n -mulr_natl mulf_eq0 subr_eq0 pnatr_eq0 => /eqP.