Ajout lemmes; independance vis a vis noms variables liees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 117 insertions, 6 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 5507acdb2..e8f83fe1a 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -10,10 +10,9 @@
 
 Require Sumbool.
 
-Require fast_integer.
+Require BinInt.
 Require Zorder.
-Require zarith_aux.
-Require auxiliary.
+Require Zcompare.
 Require Zsyntax.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
@@ -35,11 +34,12 @@ Elim (Dcompare_inf (Zcompare x y)).
 Intro H. Elim H; Auto with arith. Auto with arith.
 Defined.
 
-
 Section decidability.
 
 Variables x,y : Z.
 
+(** Decidability of equality on binary integers *)
+
 Definition Z_eq_dec : {x=y}+{~x=y}.
 Proof.
 Apply Zcompare_rec with x:=x y:=y.
@@ -50,6 +50,8 @@ Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4.
   Rewrite (H2 H4) in H3. Discriminate H3.
 Defined. 
 
+(** Decidability of order on binary integers *)
+
 Definition Z_lt_dec : {(Zlt x y)}+{~(Zlt x y)}.
 Proof.
 Unfold Zlt.
@@ -91,6 +93,15 @@ Proof.
 Exact Z_lt_dec.
 Defined.
 
+V7only [ (* From Zextensions *) ].
+Lemma Z_lt_le_dec: {`x < y`}+{`y <= x`}.
+Proof.
+Intros.
+Elim Z_lt_ge_dec.
+Intros; Left; Assumption.
+Intros; Right; Apply Zge_le; Assumption.
+Qed.
+
 Definition Z_le_gt_dec : {`x <= y`}+{`x > y`}.
 Proof.
 Elim Z_le_dec; Auto with arith.
@@ -108,7 +119,6 @@ Elim Z_ge_dec; Auto with arith.
 Intro. Right. Apply not_Zge; Auto with arith.
 Defined.
 
-
 Definition Z_le_lt_eq_dec : `x <= y` -> {`x < y`}+{x=y}.
 Proof.
 Intro H.
@@ -118,9 +128,110 @@ Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith.
 Intro H1. Absurd `x > y`; Auto with arith.
 Defined.
 
-
 End decidability.
 
+(** Cotransitivity of order on binary integers *)
+
+Lemma Zlt_cotrans:(n,m:Z)`n<m`->(p:Z){`n<p`}+{`p<m`}.
+Proof.
+ Intros x y H z.
+ Case (Z_lt_ge_dec x z).
+ Intro.
+ Left.
+ Assumption.
+ Intro.
+ Right.
+ Apply Zle_lt_trans with m:=x.
+ Apply Zge_le.
+ Assumption.
+ Assumption.
+Defined.
+
+Lemma Zlt_cotrans_pos:(x,y:Z)`0<x+y`->{`0<x`}+{`0<y`}.
+Proof.
+ Intros x y H.
+ Case (Zlt_cotrans `0` `x+y` H x).
+ Intro.
+ Left.
+ Assumption.
+ Intro.
+ Right.
+ Apply Zsimpl_lt_plus_l with p:=`x`.
+ Rewrite Zero_right.
+ Assumption.
+Defined.
+
+Lemma Zlt_cotrans_neg:(x,y:Z)`x+y<0`->{`x<0`}+{`y<0`}.
+Proof.
+ Intros x y H;
+ Case (Zlt_cotrans `x+y` `0` H x);
+ Intro Hxy;
+ [ Right;
+   Apply Zsimpl_lt_plus_l with p:=`x`;
+   Rewrite Zero_right
+ | Left
+ ];
+ Assumption.
+Defined.
+
+Lemma not_Zeq_inf:(x,y:Z)`x<>y`->{`x<y`}+{`y<x`}.
+Proof.
+ Intros x y H.
+ Case Z_lt_ge_dec with x y.
+ Intro.
+ Left.
+ Assumption.
+ Intro H0.
+ Generalize (Zge_le ? ? H0).
+ Intro.
+ Case (Z_le_lt_eq_dec ? ? H1).
+ Intro.
+ Right.
+ Assumption.
+ Intro.
+ Apply False_rec.
+ Apply H.
+ Symmetry.
+ Assumption.
+Defined.
+
+Lemma Z_dec:(x,y:Z){`x<y`}+{`x>y`}+{`x=y`}.
+Proof.
+ Intros x y.
+ Case (Z_lt_ge_dec x y).
+ Intro H.
+ Left.
+ Left.
+ Assumption.
+ Intro H.
+ Generalize (Zge_le ? ? H).
+ Intro H0.
+ Case (Z_le_lt_eq_dec y x H0).
+ Intro H1.
+ Left.
+ Right.
+ Apply Zlt_gt.
+ Assumption.
+ Intro.
+ Right.
+ Symmetry.
+ Assumption.
+Defined.
+
+
+Lemma Z_dec':(x,y:Z){`x<y`}+{`y<x`}+{`x=y`}.
+Proof.
+ Intros x y.
+ Case (Z_eq_dec x y);
+ Intro H;
+ [ Right;
+   Assumption
+ | Left;
+   Apply (not_Zeq_inf ?? H)
+ ].
+Defined.
+
+
 
 Definition Z_zerop : (x:Z){(`x = 0`)}+{(`x <> 0`)}.
 Proof.