diff options
Diffstat (limited to 'theories/Wellfounded/Well_Ordering.v')
-rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v new file mode 100644 index 00000000..4a20c518 --- /dev/null +++ b/theories/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.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Cristina Cornes. + From: Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + +Require Import Eqdep. + +Section WellOrdering. +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 := + 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. + +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 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 |