diff options
Diffstat (limited to 'theories7/ZArith/ZArith_dec.v')
-rw-r--r-- | theories7/ZArith/ZArith_dec.v | 243 |
1 files changed, 0 insertions, 243 deletions
diff --git a/theories7/ZArith/ZArith_dec.v b/theories7/ZArith/ZArith_dec.v deleted file mode 100644 index 985f7601..00000000 --- a/theories7/ZArith/ZArith_dec.v +++ /dev/null @@ -1,243 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: ZArith_dec.v,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ i*) - -Require Sumbool. - -Require BinInt. -Require Zorder. -Require Zcompare. -Require Zsyntax. -V7only [Import Z_scope.]. -Open Local Scope Z_scope. - -Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}. -Proof. -Induction r; Auto with arith. -Defined. - -Lemma Zcompare_rec : - (P:Set)(x,y:Z) - ((Zcompare x y)=EGAL -> P) -> - ((Zcompare x y)=INFERIEUR -> P) -> - ((Zcompare x y)=SUPERIEUR -> P) -> - P. -Proof. -Intros P x y H1 H2 H3. -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. -Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith. -Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4. - Rewrite (H2 H4) in H3. Discriminate H3. -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. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Right. Rewrite H. Discriminate. -Left; Assumption. -Right. Rewrite H. Discriminate. -Defined. - -Definition Z_le_dec : {(Zle x y)}+{~(Zle x y)}. -Proof. -Unfold Zle. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Left. Rewrite H. Discriminate. -Left. Rewrite H. Discriminate. -Right. Tauto. -Defined. - -Definition Z_gt_dec : {(Zgt x y)}+{~(Zgt x y)}. -Proof. -Unfold Zgt. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Right. Rewrite H. Discriminate. -Right. Rewrite H. Discriminate. -Left; Assumption. -Defined. - -Definition Z_ge_dec : {(Zge x y)}+{~(Zge x y)}. -Proof. -Unfold Zge. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Left. Rewrite H. Discriminate. -Right. Tauto. -Left. Rewrite H. Discriminate. -Defined. - -Definition Z_lt_ge_dec : {`x < y`}+{`x >= y`}. -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. -Intro. Right. Apply not_Zle; Auto with arith. -Defined. - -Definition Z_gt_le_dec : {`x > y`}+{`x <= y`}. -Proof. -Exact Z_gt_dec. -Defined. - -Definition Z_ge_lt_dec : {`x >= y`}+{`x < y`}. -Proof. -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. -Apply Zcompare_rec with x:=x y:=y. -Intro. Right. Elim (Zcompare_EGAL x y); Auto with arith. -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. -Exact [x:Z](Z_eq_dec x ZERO). -Defined. - -Definition Z_notzerop := [x:Z](sumbool_not ? ? (Z_zerop x)). - -Definition Z_noteq_dec := [x,y:Z](sumbool_not ? ? (Z_eq_dec x y)). |