From 2a7a989025a5dde9a6f34792e1e1f2b4e3ad3108 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 2 Nov 2010 19:30:57 +0000
Subject: Add small utility lemmas about nat/P/Z/Q arithmetic.

 Initial patch by Eelis van der Weegen, minor adaptations by myself

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13613 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/PArith/BinPos.v |  6 +++++-
 theories/PArith/Pnat.v   | 23 +++++++++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)

(limited to 'theories/PArith')

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 663233c57..9c8775f82 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1025,6 +1025,11 @@ Proof.
   destruct ((p ?= q) Eq); intuition; discriminate.
 Qed.
 
+Lemma Ple_refl : forall p, Ple p p.
+Proof.
+ intros. unfold Ple. rewrite Pcompare_refl_id. discriminate.
+Qed.
+
 (** Strict order and operations *)
 
 Lemma Pplus_lt_mono_l : forall p q r, q<r <-> p+q < p+r.
@@ -1070,7 +1075,6 @@ Proof.
  apply Plt_trans with (p+q); auto using Plt_plus_r.
 Qed.
 
-
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 715c4484d..b3f2493b2 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -227,6 +227,13 @@ rewrite nat_of_P_compare_morphism.
 apply <- nat_compare_eq_iff; auto.
 Qed.
 
+(** Stating this bidirectionally lets us reason equationally with it: *)
+
+Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q.
+Proof.
+ split; intro. now apply nat_of_P_inj. now subst.
+Qed.
+
 (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
     from [compare] on [positive])
 
@@ -240,6 +247,22 @@ Proof.
  apply -> nat_compare_lt; auto.
 Qed.
 
+(** Again, stating this bidirectionally lets us reason equationally with it: *)
+
+Lemma Plt_lt : forall p q, Plt p q <-> lt (nat_of_P p) (nat_of_P q).
+Proof.
+ intros. unfold Plt. rewrite nat_of_P_compare_morphism.
+ apply iff_sym, nat_compare_lt.
+Qed.
+
+(** And the same for Ple *)
+
+Lemma Ple_le : forall p q, Ple p q <-> le (nat_of_P p) (nat_of_P q).
+Proof.
+ intros. unfold Ple. rewrite nat_of_P_compare_morphism.
+ apply iff_sym, nat_compare_le.
+Qed.
+
 (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
     from [compare] on [positive])
 
-- 
cgit v1.2.3