1 files changed, 171 insertions, 0 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
new file mode 100755
index 00000000..7ab3723d
--- /dev/null
+++ b/theories/Init/Wf.v
@@ -0,0 +1,171 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Set Implicit Arguments.
+
+(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+
+(** This module proves the validity of
+    - well-founded recursion (also called course of values)
+    - well-founded induction
+
+   from a well-founded ordering on a given set *)
+
+Require Import Notations.
+Require Import Logic.
+Require Import Datatypes.
+
+(** Well-founded induction principle on Prop *)
+
+Section Well_founded.
+
+ Variable A : Set.
+ Variable R : A -> A -> Prop.
+
+ (** The accessibility predicate is defined to be non-informative *)
+
+ Inductive Acc : A -> Prop :=
+     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
+
+ Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
+  destruct 1; trivial.
+ Defined.
+
+  (** the informative elimination :
+     [let Acc_rec F = let rec wf x = F x wf in wf] *)
+
+ Section AccRecType.
+  Variable P : A -> Type.
+  Variable
+    F :
+      forall x:A,
+        (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
+
+  Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
+    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).
+
+ End AccRecType.
+
+ Definition Acc_rec (P:A -> Set) := Acc_rect P.
+
+ (** A simplified version of Acc_rec(t) *)
+
+ Section AccIter.
+  Variable P : A -> Type. 
+  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
+
+  Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
+    F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).
+
+ End AccIter.
+
+ (** A relation is well-founded if every element is accessible *)
+
+ Definition well_founded := forall a:A, Acc a.
+
+ (** well-founded induction on Set and Prop *)
+
+ Hypothesis Rwf : well_founded.
+
+ Theorem well_founded_induction_type :
+  forall P:A -> Type,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+ Proof.
+  intros; apply (Acc_iter P); auto.
+ Defined.
+
+ Theorem well_founded_induction :
+  forall P:A -> Set,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+ Proof.
+  exact (fun P:A -> Set => well_founded_induction_type P).
+ Defined.
+
+ Theorem well_founded_ind :
+  forall P:A -> Prop,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+ Proof.
+  exact (fun P:A -> Prop => well_founded_induction_type P).
+ Defined.
+
+(** Building fixpoints  *) 
+
+Section FixPoint.
+
+Variable P : A -> Set.
+Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
+
+Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
+  F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).
+
+Definition Fix (x:A) := Fix_F (Rwf x).
+
+(** Proof that [well_founded_induction] satisfies the fixpoint equation. 
+    It requires an extra property of the functional *)
+
+Hypothesis
+  F_ext :
+    forall (x:A) (f g:forall y:A, R y x -> P y),
+      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
+
+Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+
+Lemma Fix_F_eq :
+ forall (x:A) (r:Acc x),
+   F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
+destruct r using Acc_inv_dep; auto.
+Qed.
+
+Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
+intro x; induction (Rwf x); intros.
+rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
+apply F_ext; auto.
+Qed.
+
+
+Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
+intro x; unfold Fix in |- *.
+rewrite <- (Fix_F_eq (x:=x)).
+apply F_ext; intros.
+apply Fix_F_inv.
+Qed.
+
+End FixPoint.
+
+End Well_founded. 
+
+(** A recursor over pairs *)
+
+Section Well_founded_2.
+
+  Variables A B : Set.
+  Variable R : A * B -> A * B -> Prop.
+
+  Variable P : A -> B -> Type. 
+  Variable
+    F :
+      forall (x:A) (x':B),
+        (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
+
+  Fixpoint Acc_iter_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
+   P x x' :=
+    F
+      (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
+         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+
+  Hypothesis Rwf : well_founded R.
+
+  Theorem well_founded_induction_type_2 :
+   (forall (x:A) (x':B),
+      (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
+   forall (a:A) (b:B), P a b.
+  Proof.
+   intros; apply Acc_iter_2; auto.
+  Defined.
+
+End Well_founded_2.