Nettoyage Wf.v et unification (suite remarques faites sur cocorico)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10712 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 32 insertions, 39 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 39df213281..ff079a0eee 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -8,10 +8,9 @@
 
 (*i $Id$ i*)
 
-(** This module proves the validity of
-    - well-founded recursion (also called course of values)
+(** * This module proves the validity of
+    - well-founded recursion (also known as course of values)
     - well-founded induction
-
     from a well-founded ordering on a given set *)
 
 Set Implicit Arguments.
@@ -40,6 +39,7 @@ Section Well_founded.
      [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.
@@ -51,17 +51,6 @@ Section Well_founded.
 
  Definition Acc_rec (P:A -> Set) := Acc_rect P.
 
- (** A simplified version of [Acc_rect] *)
-
- 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 (Acc_inv a h)).
-
- End AccIter.
-
  (** A relation is well-founded if every element is accessible *)
 
  Definition well_founded := forall a:A, Acc a.
@@ -74,7 +63,7 @@ Section Well_founded.
   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.
+  intros; apply Acc_rect; auto.
  Defined.
 
  Theorem well_founded_induction :
@@ -91,16 +80,26 @@ Section Well_founded.
   exact (fun P:A -> Prop => well_founded_induction_type P).
  Defined.
 
-(** Building fixpoints  *) 
+(** Well-founded fixpoints *) 
 
  Section FixPoint.
 
   Variable P : A -> Type.
   Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-  Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *)
+  Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x :=
+    F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
+
+  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 (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
+  Proof. 
+   destruct r using Acc_inv_dep; auto.
+  Qed.
 
-  Definition Fix (x:A) := Acc_iter P F (Rwf x).
+  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 *)
@@ -110,16 +109,7 @@ Section Well_founded.
       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 y (Acc_inv r p)) = Fix_F x r.
-  Proof. 
-   destruct r using Acc_inv_dep; auto.
-  Qed.
-
-  Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
+  Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
   Proof.
    intro x; induction (Rwf x); intros.
    rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
@@ -129,7 +119,7 @@ Section Well_founded.
   Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
   Proof.
    intro x; unfold Fix in |- *.
-   rewrite <- (Fix_F_eq (x:=x)).
+   rewrite <- Fix_F_eq.
    apply F_ext; intros.
    apply Fix_F_inv.
   Qed.
@@ -138,7 +128,7 @@ Section Well_founded.
 
 End Well_founded. 
 
-(** A recursor over pairs *)
+(** Well-founded fixpoints over pairs *)
 
 Section Well_founded_2.
 
@@ -147,18 +137,20 @@ Section Well_founded_2.
 
   Variable P : A -> B -> Type. 
 
-  Section Acc_iter_2.
+  Section FixPoint_2.
+
   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} : 
+  Fixpoint Fix_F_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)).
-  End Acc_iter_2.
+         Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
+
+  End FixPoint_2.
 
   Hypothesis Rwf : well_founded R.
 
@@ -167,9 +159,10 @@ Section Well_founded_2.
       (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.
+   intros; apply Fix_F_2; auto.
   Defined.
 
 End Well_founded_2.
 
-Notation Fix_F := Acc_iter (only parsing). (* compatibility *)
+Notation Acc_iter   := Fix_F   (only parsing). (* compatibility *)
+Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *)
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 36ff2681b5..322f2d9be9 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -20,14 +20,14 @@ show [{n : nat | P n}]. However, one can perform a recursion on an
 inductive predicate in sort [Prop] so that the returning type of the
 recursion is in [Set]. This trick is described in Coq'Art book, Sect.
 14.2.3 and 15.4. In particular, this trick is used in the proof of
-[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an
+[Fix_F] in the module Coq.Init.Wf. There, recursion is done on an
 inductive predicate [Acc] and the resulting type is in [Type].
 
 The predicate [Acc] delineates elements that are accessible via a
 given relation [R]. An element is accessible if there are no infinite
 [R]-descending chains starting from it.
 
-To use [Acc_iter], we define a relation R and prove that if [exists n,
+To use [Fix_F], we define a relation R and prove that if [exists n,
 P n] then 0 is accessible with respect to R. Then, by induction on the
 definition of [Acc R 0], we show [{n : nat | P n}]. *)
 
@@ -79,7 +79,7 @@ Defined.
 
 Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
 Proof.
-intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption].
+intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption].
 clear Acc_0; intros x IH.
 destruct (P_decidable x) as [Px | not_Px].
 exists x; simpl; assumption.