diff options
Diffstat (limited to 'theories/Wellfounded/Well_Ordering.v')
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 75 |
1 files changed, 37 insertions, 38 deletions
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index e9a18e74..69617de2 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Well_Ordering.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Well_Ordering.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory @@ -15,58 +15,57 @@ Require Import Eqdep. Section WellOrdering. -Variable A : Set. -Variable B : A -> Set. - -Inductive WO : Set := + Variable A : Set. + Variable B : A -> Set. + + Inductive WO : Set := sup : forall (a:A) (f:B a -> WO), WO. -Inductive le_WO : WO -> WO -> Prop := + 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 le_WO. -Proof. - 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. + Theorem wf_WO : well_founded le_WO. + Proof. + 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. Section Characterisation_wf_relations. -(** Wellfounded relations are the inverse image of wellordering types *) -(* in course of development *) + (** Wellfounded relations are the inverse image of wellordering types *) + (* 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 leA -> A -> WO A B. -Proof. - 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. + Definition wof : well_founded leA -> A -> WO A B. + Proof. + 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.
\ No newline at end of file |