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/Wellfounded/Well_Ordering.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/Well_Ordering.v')
-rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 66 |
1 files changed, 33 insertions, 33 deletions
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index 49595dd2b..c4c7daa98 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -12,36 +12,36 @@ From: Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) -Require Eqdep. +Require Import Eqdep. Section WellOrdering. -Variable A:Set. -Variable B:A->Set. +Variable A : Set. +Variable B : A -> Set. Inductive WO : Set := - sup : (a:A)(f:(B a)->WO)WO. + sup : forall (a:A) (f:B a -> WO), WO. -Inductive le_WO : WO->WO->Prop := - le_sup : (a:A)(f:(B a)->WO)(v:(B a)) (le_WO (f v) (sup a f)). +Inductive le_WO : WO -> WO -> Prop := + le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f). -Theorem wf_WO : (well_founded WO le_WO ). +Theorem wf_WO : well_founded le_WO. Proof. - Unfold well_founded ;Intro. - Apply Acc_intro. - Elim a. - Intros. - Inversion H0. - Apply Acc_intro. - Generalize H4 ;Generalize H1 ;Generalize f0 ;Generalize v. - Rewrite -> H3. - Intros. - Apply (H v0 y0). - Cut (eq ? f f1). - Intros E;Rewrite -> E;Auto. - Symmetry. - Apply (inj_pair2 A [a0:A](B a0)->WO a0 f1 f H5). + unfold well_founded in |- *; intro. + apply Acc_intro. + elim a. + intros. + inversion H0. + apply Acc_intro. + generalize H4; generalize H1; generalize f0; generalize v. + rewrite H3. + intros. + apply (H v0 y0). + cut (f = f1). + intros E; rewrite E; auto. + symmetry in |- *. + apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5). Qed. End WellOrdering. @@ -53,20 +53,20 @@ Section Characterisation_wf_relations. (* in course of development *) -Variable A:Set. -Variable leA:A->A->Prop. +Variable A : Set. +Variable leA : A -> A -> Prop. -Definition B:= [a:A] {x:A | (leA x a)}. +Definition B (a:A) := {x : A | leA x a}. -Definition wof: (well_founded A leA)-> A-> (WO A B). +Definition wof : well_founded leA -> A -> WO A B. Proof. - Intros. - Apply (well_founded_induction A leA H [a:A](WO A B));Auto. - Intros. - Apply (sup A B x). - Unfold 1 B . - NewDestruct 1 as [x0]. - Apply (H1 x0);Auto. + intros. + apply (well_founded_induction H (fun a:A => WO A B)); auto. + intros. + apply (sup A B x). + unfold B at 1 in |- *. + destruct 1 as [x0]. + apply (H1 x0); auto. Qed. -End Characterisation_wf_relations. +End Characterisation_wf_relations.
\ No newline at end of file |