diff options
Diffstat (limited to 'theories/Arith/Compare_dec.v')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 116 |
1 files changed, 60 insertions, 56 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index d2eead86..e6dc7c46 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Compare_dec.v 8733 2006-04-25 22:52:18Z letouzey $ i*) +(*i $Id: Compare_dec.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Le. Require Import Lt. @@ -17,109 +17,113 @@ Open Local Scope nat_scope. Implicit Types m n x y : nat. -Definition zerop : forall n, {n = 0} + {0 < n}. -destruct n; auto with arith. +Definition zerop n : {n = 0} + {0 < n}. + destruct n; auto with arith. Defined. -Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}. -Proof. -induction n; simple destruct m; auto with arith. -intros m0; elim (IHn m0); auto with arith. -induction 1; auto with arith. +Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. + induction n; simple destruct m; auto with arith. + intros m0; elim (IHn m0); auto with arith. + induction 1; auto with arith. Defined. -Lemma gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}. -Proof lt_eq_lt_dec. +Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}. + exact lt_eq_lt_dec. +Defined. -Lemma le_lt_dec : forall n m, {n <= m} + {m < n}. -Proof. -induction n. -auto with arith. -induction m. -auto with arith. -elim (IHn m); auto with arith. +Definition le_lt_dec n m : {n <= m} + {m < n}. + induction n. + auto with arith. + induction m. + auto with arith. + elim (IHn m); auto with arith. Defined. -Definition le_le_S_dec : forall n m, {n <= m} + {S m <= n}. -Proof. -exact le_lt_dec. +Definition le_le_S_dec n m : {n <= m} + {S m <= n}. + exact le_lt_dec. Defined. -Definition le_ge_dec : forall n m, {n <= m} + {n >= m}. -Proof. -intros; elim (le_lt_dec n m); auto with arith. +Definition le_ge_dec n m : {n <= m} + {n >= m}. + intros; elim (le_lt_dec n m); auto with arith. Defined. -Definition le_gt_dec : forall n m, {n <= m} + {n > m}. -Proof. -exact le_lt_dec. +Definition le_gt_dec n m : {n <= m} + {n > m}. + exact le_lt_dec. Defined. -Definition le_lt_eq_dec : forall n m, n <= m -> {n < m} + {n = m}. -Proof. -intros; elim (lt_eq_lt_dec n m); auto with arith. -intros; absurd (m < n); auto with arith. +Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}. + intros; elim (lt_eq_lt_dec n m); auto with arith. + intros; absurd (m < n); auto with arith. Defined. (** Proofs of decidability *) Theorem dec_le : forall n m, decidable (n <= m). -intros x y; unfold decidable in |- *; elim (le_gt_dec x y); - [ auto with arith | intro; right; apply gt_not_le; assumption ]. +Proof. + intros x y; unfold decidable in |- *; elim (le_gt_dec x y); + [ auto with arith | intro; right; apply gt_not_le; assumption ]. Qed. Theorem dec_lt : forall n m, decidable (n < m). -intros x y; unfold lt in |- *; apply dec_le. +Proof. + intros x y; unfold lt in |- *; apply dec_le. Qed. Theorem dec_gt : forall n m, decidable (n > m). -intros x y; unfold gt in |- *; apply dec_lt. +Proof. + intros x y; unfold gt in |- *; apply dec_lt. Qed. Theorem dec_ge : forall n m, decidable (n >= m). -intros x y; unfold ge in |- *; apply dec_le. +Proof. + intros x y; unfold ge in |- *; apply dec_le. Qed. Theorem not_eq : forall n m, n <> m -> n < m \/ m < n. -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 ]. +Proof. + 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 ]. Qed. Theorem not_le : forall n m, ~ n <= m -> n > m. -intros x y H; elim (le_gt_dec x y); - [ intros H1; absurd (x <= y); assumption | trivial with arith ]. +Proof. + intros x y H; elim (le_gt_dec x y); + [ intros H1; absurd (x <= y); assumption | trivial with arith ]. Qed. Theorem not_gt : forall n m, ~ n > m -> n <= m. -intros x y H; elim (le_gt_dec x y); - [ trivial with arith | intros H1; absurd (x > y); assumption ]. +Proof. + intros x y H; elim (le_gt_dec x y); + [ trivial with arith | intros H1; absurd (x > y); assumption ]. Qed. Theorem not_ge : forall n m, ~ n >= m -> n < m. -intros x y H; exact (not_le y x H). +Proof. + intros x y H; exact (not_le y x H). Qed. Theorem not_lt : forall n m, ~ n < m -> n >= m. -intros x y H; exact (not_gt y x H). +Proof. + intros x y H; exact (not_gt y x H). Qed. (** A ternary comparison function in the spirit of [Zcompare]. *) Definition nat_compare (n m:nat) := - match lt_eq_lt_dec n m with - | inleft (left _) => Lt - | inleft (right _) => Eq - | inright _ => Gt - end. + match lt_eq_lt_dec n m with + | inleft (left _) => Lt + | inleft (right _) => Eq + | inright _ => Gt + end. Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m. Proof. - unfold nat_compare; intros. - simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto. + unfold nat_compare; intros. + simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto. Qed. Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m. @@ -188,11 +192,11 @@ Qed. Fixpoint leb (m:nat) : nat -> bool := match m with - | O => fun _:nat => true - | S m' => + | O => fun _:nat => true + | S m' => fun n:nat => match n with - | O => false - | S n' => leb m' n' + | O => false + | S n' => leb m' n' end end. |