diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Arith/Compare.v | |
parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) |
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Compare.v')
-rwxr-xr-x | theories/Arith/Compare.v | 43 |
1 files changed, 21 insertions, 22 deletions
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 88055f11e..b5afebd94 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -9,7 +9,6 @@ (*i $Id$ i*) (** Equality is decidable on [nat] *) -V7only [Import nat_scope.]. Open Local Scope nat_scope. (* @@ -19,42 +18,42 @@ Hints Immediate not_eq_sym : arith. *) Notation not_eq_sym := sym_not_eq. -Implicit Variables Type m,n,p,q:nat. +Implicit Types m n p q : nat. -Require Arith. -Require Peano_dec. -Require Compare_dec. +Require Import Arith. +Require Import Peano_dec. +Require Import Compare_dec. Definition le_or_le_S := le_le_S_dec. -Definition compare := gt_eq_gt_dec. +Definition Pcompare := gt_eq_gt_dec. -Lemma le_dec : (n,m:nat) {le n m} + {le m n}. +Lemma le_dec : forall n m, {n <= m} + {m <= n}. Proof le_ge_dec. -Definition lt_or_eq := [n,m:nat]{(gt m n)}+{n=m}. +Definition lt_or_eq n m := {m > n} + {n = m}. -Lemma le_decide : (n,m:nat)(le n m)->(lt_or_eq n m). +Lemma le_decide : forall n m, n <= m -> lt_or_eq n m. Proof le_lt_eq_dec. -Lemma le_le_S_eq : (p,q:nat)(le p q)->((le (S p) q)\/(p=q)). +Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m. Proof le_lt_or_eq. (* By special request of G. Kahn - Used in Group Theory *) -Lemma discrete_nat : (m, n: nat) (lt m n) -> - (S m) = n \/ (EX r: nat | n = (S (S (plus m r)))). +Lemma discrete_nat : + forall n m, n < m -> S n = m \/ ( exists r : nat | m = S (S (n + r))). Proof. -Intros m n H. -LApply (lt_le_S m n); Auto with arith. -Intro H'; LApply (le_lt_or_eq (S m) n); Auto with arith. -NewInduction 1; Auto with arith. -Right; Exists (minus n (S (S m))); Simpl. -Rewrite (plus_sym m (minus n (S (S m)))). -Rewrite (plus_n_Sm (minus n (S (S m))) m). -Rewrite (plus_n_Sm (minus n (S (S m))) (S m)). -Rewrite (plus_sym (minus n (S (S m))) (S (S m))); Auto with arith. +intros m n H. +lapply (lt_le_S m n); auto with arith. +intro H'; lapply (le_lt_or_eq (S m) n); auto with arith. +induction 1; auto with arith. +right; exists (n - S (S m)); simpl in |- *. +rewrite (plus_comm m (n - S (S m))). +rewrite (plus_n_Sm (n - S (S m)) m). +rewrite (plus_n_Sm (n - S (S m)) (S m)). +rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith. Qed. Require Export Wf_nat. -Require Export Min. +Require Export Min.
\ No newline at end of file |