From 859a9666923e657add7e972762af29a1872cc842 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Sep 2016 22:40:16 +0200
Subject: A couple of other useful properties about compare_cont.

Don't know if compare_cont is very useful to use, but, at least, these
extensions make sense.
---
 theories/Init/Datatypes.v |  5 +++++
 theories/PArith/BinPos.v  | 28 ++++++++++++++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 4e3f2e80f3..11d80dbc33 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -262,6 +262,11 @@ Inductive comparison : Set :=
   | Lt : comparison
   | Gt : comparison.
 
+Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
+Proof.
+  destruct c, c'; intro H; reflexivity || destruct H; discriminate.
+Qed.
+
 Definition CompOpp (r:comparison) :=
   match r with
     | Eq => Eq
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 7baf102aaa..d6385ee314 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -813,6 +813,34 @@ Proof.
   rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'.
 Qed.
 
+Lemma compare_cont_Lt_not_Lt p q :
+  compare_cont Lt p q <> Lt <-> p > q.
+Proof.
+  rewrite compare_cont_Lt_Lt.
+  unfold gt, le, compare.
+  now destruct compare_cont; split; try apply comparison_eq_stable.
+Qed.
+
+Lemma compare_cont_Lt_not_Gt p q :
+  compare_cont Lt p q <> Gt <-> p <= q.
+Proof.
+  apply not_iff_compat, compare_cont_Lt_Gt.
+Qed.
+
+Lemma compare_cont_Gt_not_Lt p q :
+  compare_cont Gt p q <> Lt <-> p >= q.
+Proof.
+  apply not_iff_compat, compare_cont_Gt_Lt.
+Qed.
+
+Lemma compare_cont_Gt_not_Gt p q :
+  compare_cont Gt p q <> Gt <-> p < q.
+Proof.
+  rewrite compare_cont_Gt_Gt.
+  unfold ge, lt, compare.
+  now destruct compare_cont; split; try apply comparison_eq_stable.
+Qed.
+
 (** We can express recursive equations for [compare] *)
 
 Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q).
-- 
cgit v1.2.3