diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-08 17:18:57 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-08 17:18:57 +0000 |
commit | d41db01560cb49974af197d22dabc367c71a64ed (patch) | |
tree | 75517698617653da2fd0a522cda1942421baa023 /theories/Arith/Compare_dec.v | |
parent | 509940521cda3057455adb0f0af8b16d88b73df6 (diff) |
ajout des lemmes Zimmerman
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Compare_dec.v')
-rwxr-xr-x | theories/Arith/Compare_dec.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 8ef796eef..72baafe3a 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -10,6 +10,8 @@ Require Le. Require Lt. +Require Gt. +Require Decidable. Theorem zerop : (n:nat){n=O}+{lt O n}. Destruct n; Auto with arith. @@ -52,3 +54,49 @@ Proof. Intros; Elim (lt_eq_lt_dec n m); Auto with arith. Intros; Absurd (lt m n); Auto with arith. Qed. + +(* Proofs of decidability *) + +Theorem dec_le:(x,y:nat)(decidable (le x y)). +Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [ + Auto with arith +| Intro; Right; Apply gt_not_le; Assumption]. +Save. + +Theorem dec_lt:(x,y:nat)(decidable (lt x y)). +Intros x y; Unfold lt; Apply dec_le. +Save. + +Theorem dec_gt:(x,y:nat)(decidable (gt x y)). +Intros x y; Unfold gt; Apply dec_lt. +Save. + +Theorem dec_ge:(x,y:nat)(decidable (ge x y)). +Intros x y; Unfold ge; Apply dec_le. +Save. + +Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x). +Intros x y H; Elim (lt_eq_lt_dec x y); [ + Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption] +| Auto with arith]. +Save. + + +Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y). +Intros x y H; Elim (le_gt_dec x y); + [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ]. +Save. + +Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y). +Intros x y H; Elim (le_gt_dec x y); + [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption]. +Save. + +Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y). +Intros x y H; Exact (not_le y x H). +Save. + +Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y). +Intros x y H; Exact (not_gt y x H). +Save. + |