diff options
Diffstat (limited to 'theories7/Wellfounded/Well_Ordering.v')
-rw-r--r-- | theories7/Wellfounded/Well_Ordering.v | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/theories7/Wellfounded/Well_Ordering.v b/theories7/Wellfounded/Well_Ordering.v new file mode 100644 index 00000000..5c2b2405 --- /dev/null +++ b/theories7/Wellfounded/Well_Ordering.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Well_Ordering.v,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ i*) + +(** Author: Cristina Cornes. + From: Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + +Require Eqdep. + +Section WellOrdering. +Variable A:Set. +Variable B:A->Set. + +Inductive WO : Set := + sup : (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)). + + +Theorem wf_WO : (well_founded WO 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). +Qed. + +End WellOrdering. + + +Section Characterisation_wf_relations. + +(** Wellfounded relations are the inverse image of wellordering types *) +(* in course of development *) + + +Variable A:Set. +Variable leA:A->A->Prop. + +Definition B:= [a:A] {x:A | (leA x a)}. + +Definition wof: (well_founded A 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. +Qed. + +End Characterisation_wf_relations. |