diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-21 14:41:16 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-21 14:41:16 +0000 |
commit | 838ffd441e80aa324ffe731f2527dbb181654308 (patch) | |
tree | a4ab1228901f2b63f0638c9a5fa627d6036af625 /theories/Wellfounded/Transitive_Closure.v | |
parent | 78fb07846e6ca303417699d19beaeaf1a97f96af (diff) |
ajout de theories/Wellfounded
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Wellfounded/Transitive_Closure.v')
-rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v new file mode 100644 index 000000000..a97cadc27 --- /dev/null +++ b/theories/Wellfounded/Transitive_Closure.v @@ -0,0 +1,46 @@ + +(* $Id$ *) + +(****************************************************************************) +(* Bruno Barras *) +(****************************************************************************) + +Require Relation_Definitions. +Require Relation_Operators. + +Section Wf_Transitive_Closure. + Variable A: Set. + Variable R: (relation A). + + Syntactic Definition trans_clos := (clos_trans A R). + + Lemma incl_clos_trans: (inclusion A R trans_clos). + Red;Auto with sets. + Qed. + + Lemma Acc_clos_trans: (x:A)(Acc A R x)->(Acc A trans_clos x). + Induction 1. + Intros x0 H0 H1. + Apply Acc_intro. + Intros y H2. + Generalize H1 . + Elim H2;Auto with sets. + Intros x1 y0 z H3 H4 H5 H6 H7. + Apply Acc_inv with y0 ;Auto with sets. + Qed. + + Hints Resolve Acc_clos_trans. + + Lemma Acc_inv_trans: (x,y:A)(trans_clos y x)->(Acc A R x)->(Acc A R y). + Proof. + Induction 1;Auto with sets. + Intros x0 y0 H0 H1. + Apply Acc_inv with y0 ;Auto with sets. + Qed. + + Theorem wf_clos_trans: (well_founded A R) ->(well_founded A trans_clos). + Proof. + Unfold well_founded;Auto with sets. + Qed. + +End Wf_Transitive_Closure. |