diff options
author | 2003-11-29 17:28:49 +0000 | |
---|---|---|
committer | 2003-11-29 17:28:49 +0000 | |
commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Wellfounded/Transitive_Closure.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/Wellfounded/Transitive_Closure.v')
-rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index c650d4675..b2af4dd85 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -10,38 +10,38 @@ (** Author: Bruno Barras *) -Require Relation_Definitions. -Require Relation_Operators. +Require Import Relation_Definitions. +Require Import Relation_Operators. Section Wf_Transitive_Closure. - Variable A: Set. - Variable R: (relation A). + Variable A : Set. + Variable R : relation A. Notation trans_clos := (clos_trans A R). - Lemma incl_clos_trans: (inclusion A R trans_clos). - Red;Auto with sets. + Lemma incl_clos_trans : inclusion A R trans_clos. + red in |- *; auto with sets. Qed. - Lemma Acc_clos_trans: (x:A)(Acc A R x)->(Acc A trans_clos x). - NewInduction 1 as [x0 _ H1]. - Apply Acc_intro. - Intros y H2. - NewInduction H2;Auto with sets. - Apply Acc_inv with y ;Auto with sets. + Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x. + induction 1 as [x0 _ H1]. + apply Acc_intro. + intros y H2. + induction H2; auto with sets. + apply Acc_inv with y; auto with sets. Qed. - Hints Resolve Acc_clos_trans. + Hint Resolve Acc_clos_trans. - Lemma Acc_inv_trans: (x,y:A)(trans_clos y x)->(Acc A R x)->(Acc A R y). + Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. Proof. - NewInduction 1 as [|x y];Auto with sets. - Intro; Apply Acc_inv with y; Assumption. + induction 1 as [| x y]; auto with sets. + intro; apply Acc_inv with y; assumption. Qed. - Theorem wf_clos_trans: (well_founded A R) ->(well_founded A trans_clos). + Theorem wf_clos_trans : well_founded R -> well_founded trans_clos. Proof. - Unfold well_founded;Auto with sets. + unfold well_founded in |- *; auto with sets. Qed. -End Wf_Transitive_Closure. +End Wf_Transitive_Closure.
\ No newline at end of file |