(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                            Well_Ordering.v                               *)
(****************************************************************************)
(*                             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 .
 Induction 1.
 Intros.
 (Apply (H1 x0);Auto).
Qed.

End Characterisation_wf_relations.




(* $Id: Well_Ordering.v,v 1.6 1999/06/29 07:48:57 loiseleu Exp $ *)
