From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 theories/Wellfounded/Well_Ordering.v | 75 ++++++++++++++++++------------------
 1 file changed, 37 insertions(+), 38 deletions(-)

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

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