diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:12:46 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:12:46 +0000 |
commit | a36fe20505fee708d8d88700aa7fedd4d4157364 (patch) | |
tree | e74a114ef70ae1e8509133f351fc02939d499039 /theories/Arith/Compare_dec.v | |
parent | bf289727d98418069ee3011917393a725d011349 (diff) |
Compare_dec : a few better proofs (and extracted terms), some more Defined
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12937 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Compare_dec.v')
-rw-r--r-- | theories/Arith/Compare_dec.v | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index d696360fd..38d1aef0e 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -18,21 +18,25 @@ Open Local Scope nat_scope. Implicit Types m n x y : nat. Definition zerop n : {n = 0} + {0 < n}. +Proof. destruct n; auto with arith. Defined. Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. - intros; induction n in m |- *; destruct m; auto with arith. +Proof. + induction n; destruct m; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}. +Proof. intros; apply lt_eq_lt_dec; assumption. Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. - intros; induction n in m |- *. +Proof. + induction n. auto with arith. destruct m. auto with arith. @@ -40,48 +44,53 @@ Definition le_lt_dec n m : {n <= m} + {m < n}. Defined. Definition le_le_S_dec n m : {n <= m} + {S m <= n}. +Proof. intros; exact (le_lt_dec n m). Defined. Definition le_ge_dec n m : {n <= m} + {n >= m}. +Proof. intros; elim (le_lt_dec n m); auto with arith. Defined. Definition le_gt_dec n m : {n <= m} + {n > m}. +Proof. intros; exact (le_lt_dec n m). Defined. Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}. +Proof. intros; destruct (lt_eq_lt_dec n m); auto with arith. intros; absurd (m < n); auto with arith. Defined. Theorem le_dec : forall n m, {n <= m} + {~ n <= m}. Proof. - intros x y; elim (le_gt_dec x y); - [ auto with arith | intro; right; apply gt_not_le; assumption ]. -Qed. + intros n m. destruct (le_gt_dec n m). + auto with arith. + right. apply gt_not_le. assumption. +Defined. Theorem lt_dec : forall n m, {n < m} + {~ n < m}. Proof. intros; apply le_dec. -Qed. +Defined. Theorem gt_dec : forall n m, {n > m} + {~ n > m}. Proof. intros; apply lt_dec. -Qed. +Defined. Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}. Proof. intros; apply le_dec. -Qed. +Defined. (** Proofs of decidability *) Theorem dec_le : forall n m, decidable (n <= m). Proof. - intros x y; destruct (le_dec x y); unfold decidable; auto. + intros n m; destruct (le_dec n m); unfold decidable; auto. Qed. Theorem dec_lt : forall n m, decidable (n < m). |