From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 theories7/Wellfounded/Well_Ordering.v | 72 +++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)
 create mode 100644 theories7/Wellfounded/Well_Ordering.v

(limited to 'theories7/Wellfounded/Well_Ordering.v')

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.
-- 
cgit v1.2.3