diff options
Diffstat (limited to 'theories/Arith/Compare_dec.v')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 99c7415e..360d760a 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Compare_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Le. Require Import Lt. Require Import Gt. @@ -22,21 +20,21 @@ Proof. destruct n; auto with arith. Defined. -Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}. +Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n; destruct m; auto with arith. + induction n in m |- *; 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 : forall n m, {m > n} + {n = m} + {n > m}. +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 : forall n m, {n <= m} + {m < n}. +Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n. + induction n in m |- *. auto with arith. destruct m. auto with arith. @@ -200,7 +198,8 @@ Proof. apply -> nat_compare_lt; auto. Qed. -Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y). +Lemma nat_compare_spec : + forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y). Proof. intros. destruct (nat_compare x y) as [ ]_eqn; constructor. @@ -209,7 +208,6 @@ Proof. apply <- nat_compare_gt; auto. Qed. - (** Some projections of the above equivalences. *) Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m. |