Move FunctionalExtensionality to Logic/ (someone please check that the

doc is ok). Rework the .v files in Program accordingly, adding some
documentation and proper headers. Integrate the development of an
elimination principle for measured functions in Program/Wf by Eelis van
der Weegen.


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

12 files changed, 307 insertions, 157 deletions

diff --git a/Makefile.common b/Makefile.common
index cefdfd4e19..4ca7e2e45b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -543,7 +543,7 @@ LOGICVO:=$(addprefix theories/Logic/, \
  EqdepFacts.vo            ProofIrrelevanceFacts.vo ClassicalEpsilon.vo 	\
  ClassicalUniqueChoice.vo DecidableType.vo         DecidableTypeEx.vo 	\
  Epsilon.vo               ConstructiveEpsilon.vo   Description.vo 	\
- IndefiniteDescription.vo SetIsType.vo )
+ IndefiniteDescription.vo SetIsType.vo             FunctionalExtensionality.vo )
 
 ARITHVO:=$(addprefix theories/Arith/, \
  Arith.vo	Gt.vo          	Between.vo	Le.vo         	\
@@ -740,8 +740,7 @@ CLASSESVO:=$(addprefix theories/Classes/, \
 
 PROGRAMVO:=$(addprefix theories/Program/, \
  Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
- Wf.vo 		Basics.vo	FunctionalExtensionality.vo 	\
- Combinators.vo	Syntax.vo 	Program.vo )
+ Wf.vo 		Basics.vo	Combinators.vo	Syntax.vo 	Program.vo )
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 91c417ce3d..b85d5d7d24 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -115,9 +115,8 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
 
   Solve Obligations using unfold complement, equiv ; program_simpl.
 
-(** Objects of function spaces with countable domains like bool have decidable equality. *)
-
-Require Import Coq.Program.FunctionalExtensionality.
+(** Objects of function spaces with countable domains like bool have decidable equality. 
+   Proving the reflection requires functional extensionality though. *)
 
 Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
   equiv_dec f g := 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 5b44f68481..8504a06f43 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -107,8 +107,6 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq
 
 (** Objects of function spaces with countable domains like bool have decidable equality. *)
 
-Require Import Coq.Program.FunctionalExtensionality.
-
 Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
new file mode 100644
index 0000000000..865a465534
--- /dev/null
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  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$ i*)
+
+(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
+   It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *)
+
+Set Manual Implicit Arguments.
+
+(** The converse of functional extensionality. *)
+
+Lemma equal_f : forall {A B : Type} {f g : A -> B}, 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
+
+(** Statements of functional extensionality for simple and dependent functions. *)
+
+Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, 
+  forall (f g : forall x : A, B x), 
+  (forall x, f x = g x) -> f = g.
+
+Lemma functional_extensionality {A B} (f g : A -> B) : 
+  (forall x, f x = g x) -> f = g.
+Proof.
+  intros ; eauto using @functional_extensionality_dep.
+Qed.
+
+(** Apply [functional_extensionality], introducing variable x. *)
+
+Tactic Notation "extensionality" ident(x) :=
+  match goal with
+    [ |- ?X = ?Y ] => 
+    (apply (@functional_extensionality _ _ X Y) || 
+     apply (@functional_extensionality_dep _ _ X Y)) ; intro x
+  end.
+
+(** Eta expansion follows from extensionality. *)
+
+Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) :
+  f = fun x => f x.
+Proof.
+  intros.
+  extensionality x.
+  reflexivity.
+Qed.
+  
+Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x.
+Proof.
+  intros A B f. apply (eta_expansion_dep f).
+Qed.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index d304b651f2..9335f48348 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -5,15 +5,15 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id$ *)
 
-(* Standard functions and combinators.
- * Proofs about them require functional extensionality and can be found in [Combinators].
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** Standard functions and combinators.
+   
+   Proofs about them require functional extensionality and can be found in [Combinators].
 
-(* $Id$ *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+   91405 Orsay, France *)
 
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index e267fbbe20..33ad3b556c 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -5,15 +5,16 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id$ *)
 
-(* Proofs about standard combinators, exports functional extensionality.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** Proofs about standard combinators, exports functional extensionality.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
 
 Require Import Coq.Program.Basics.
-Require Export Coq.Program.FunctionalExtensionality.
+Require Export FunctionalExtensionality.
 
 Open Scope program_scope.
 
@@ -40,7 +41,8 @@ Proof.
   reflexivity.
 Qed.
 
-Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core.
+Hint Rewrite @compose_id_left @compose_id_right : core.
+Hint Rewrite <- @compose_assoc : core.
 
 (** [flip] is involutive. *)
 
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
deleted file mode 100644
index 8bd2dfb905..0000000000
--- a/theories/Program/FunctionalExtensionality.v
+++ /dev/null
@@ -1,123 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
-(************************************************************************)
-(*  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$ i*)
-
-(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
-   It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. 
-
-   It also defines two lemmas for expansion of fixpoint defs using extensionnality and proof-irrelevance
-   to avoid a side condition on the functionals. *)
-   
-Require Import Coq.Program.Utils.
-Require Import Coq.Program.Wf.
-Require Import Coq.Program.Equality.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** The converse of functional extensionality. *)
-
-Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
-  f = g -> forall x, f x = g x.
-Proof.
-  intros.
-  rewrite H.
-  auto.
-Qed.
-
-(** Statements of functional extensionality for simple and dependent functions. *)
-
-Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), 
-  forall (f g : forall x : A, B x), 
-  (forall x, f x = g x) -> f = g.
-
-Lemma fun_extensionality : forall A B (f g : A -> B), 
-  (forall x, f x = g x) -> f = g.
-Proof.
-  intros ; apply fun_extensionality_dep.
-  assumption.
-Qed.
-
-Hint Resolve fun_extensionality fun_extensionality_dep : program.
-
-(** Apply [fun_extensionality], introducing variable x. *)
-
-Tactic Notation "extensionality" ident(x) :=
-  match goal with
-    [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x
-  end.
-
-(** Eta expansion follows from extensionality. *)
-
-Lemma eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), 
-  f = fun x => f x.
-Proof.
-  intros.
-  extensionality x.
-  reflexivity.
-Qed.
-  
-Lemma eta_expansion : forall A B (f : A -> B), 
-  f = fun x => f x.
-Proof.
-  intros ; apply eta_expansion_dep.
-Qed.
-
-(** The two following lemmas allow to unfold a well-founded fixpoint definition without
-   restriction using the functional extensionality axiom. *)
-
-(** For a function defined with Program using a well-founded order. *)
-
-Program Lemma fix_sub_eq_ext :
-  forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
-    (P : A -> Set)
-    (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
-    forall x : A,
-      Fix_sub A R Rwf P F_sub x =
-        F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y).
-Proof.
-  intros ; apply Fix_eq ; auto.
-  intros.
-  assert(f = g).
-  extensionality y ; apply H.
-  rewrite H0 ; auto.
-Qed.
-
-(** For a function defined with Program using a measure. *)
-
-Program Lemma fix_sub_measure_eq_ext :
-  forall (A : Type) (f : A -> nat) (P : A -> Type)
-    (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
-    forall x : A,
-      Fix_measure_sub A f P F_sub x =
-        F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).
-Proof.
-  intros ; apply Fix_measure_eq ; auto.
-  intros.
-  assert(f0 = g).
-  extensionality y ; apply H.
-  rewrite H0 ; auto.
-Qed.
-
-(** Tactics to fold/unfold definitions based on [Fix_measure_sub]. *)
-
-Ltac fold_sub f :=
-  match goal with
-    | [ |- ?T ] => 
-      match T with
-        appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => 
-        let app := context C [ f arg ] in
-         change app
-      end
-  end.
-
-Ltac unfold_sub f fargs := 
-  set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
-  rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index b6c3031e73..cdfc785837 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,3 +1,12 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+(* $Id$ *)
+
 Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
 Require Export Coq.Program.Equality.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index d021326a10..14dc473584 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -5,14 +5,15 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id$ *)
+
+(** Tactics related to subsets and proof irrelevance. *)
 
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
 Open Local Scope program_scope.
 
-(** Tactics related to subsets and proof irrelevance. *)
-
 (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to 
    factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
 
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 6cd75257b8..f45511823d 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,14 +5,15 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id$ *)
 
-(* Custom notations and implicits for Coq prelude definitions.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** Custom notations and implicits for Coq prelude definitions.
 
-(** Notations for the unit type and value. *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(** Notations for the unit type and value à la Haskell. *)
 
 Notation " () " := Datatypes.unit : type_scope.
 Notation " () " := tt.
@@ -42,7 +42,7 @@ Notation " [ ] " := nil : list_scope.
 Notation " [ x ] " := (cons x nil) : list_scope.
 Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
-(** n-ary exists *)
+(** Treating n-ary exists *)
 
 Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
   (at level 200, x ident, y ident, right associativity) : type_scope.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index a4eb8bbcc0..fbf0b03cf8 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -8,6 +8,8 @@
 
 (*i $Id$ i*)
 
+(** Various syntaxic shortands that are useful with [Program]. *)
+
 Require Export Coq.Program.Tactics.
 
 Set Implicit Arguments.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index b6ba5d44ec..5d005d2739 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+(* $Id$ *)
+
+(** Reformulation of the Wf module using subsets where possible, providing
+   the support for [Program]'s treatment of well-founded definitions. *)
+
 Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
@@ -6,8 +18,6 @@ Open Local Scope program_scope.
 
 Implicit Arguments Acc_inv [A R x y].
 
-(** Reformulation of the Wellfounded module using subsets where possible. *)
-
 Section Well_founded.
   Variable A : Type.
   Variable R : A -> A -> Prop.
@@ -146,3 +156,196 @@ Section Well_founded_measure.
 End Well_founded_measure.
 
 Extraction Inline Fix_measure_F_sub Fix_measure_sub.
+
+Set Implicit Arguments.
+
+(** Reasoning about well-founded fixpoints on measures. *)
+
+Section Measure_well_founded.
+
+  (* Measure relations are well-founded if the underlying relation is well-founded. *)
+
+  Variables T M: Set.
+  Variable R: M -> M -> Prop.
+  Hypothesis wf: well_founded R.
+  Variable m: T -> M.
+
+  Definition MR (x y: T): Prop := R (m x) (m y).
+
+  Lemma measure_wf: well_founded MR.
+  Proof with auto.
+    unfold well_founded.
+    cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a).
+      intros.
+      apply (H (m a))...
+    apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
+    intros.
+    apply Acc_intro.
+    intros.
+    unfold MR in H1.
+    rewrite H0 in H1.
+    apply (H (m y))...
+  Defined.
+
+End Measure_well_founded.
+
+Section Fix_measure_rects.
+
+  Variable A: Set.
+  Variable m: A -> nat.
+  Variable P: A -> Type.
+  Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
+  
+  Lemma F_unfold x r:
+    Fix_measure_F_sub A m P f x r =
+    f (fun y => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv r (proj2_sig y))).
+  Proof. intros. case r; auto. Qed.
+
+  (* Fix_measure_F_sub_rect lets one prove a property of
+  functions defined using Fix_measure_F_sub by showing
+  that property to be invariant over single application of the
+  function body (f in our case). *)
+
+  Lemma Fix_measure_F_sub_rect
+    (Q: forall x, P x -> Type)
+    (inv: forall x: A,
+     (forall (y: A) (H: MR lt m y x) (a: Acc lt (m y)),
+        Q y (Fix_measure_F_sub A m P f y a)) ->
+        forall (a: Acc lt (m x)),
+          Q x (f (fun y: {y: A | m y < m x} =>
+            Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
+    : forall x a, Q _ (Fix_measure_F_sub A m P f x a).
+  Proof with auto.
+    intros Q inv.
+    set (R := fun (x: A) => forall a, Q _ (Fix_measure_F_sub A m P f x a)).
+    cut (forall x, R x)...
+    apply (well_founded_induction_type (measure_wf lt_wf m)).
+    subst R.
+    simpl.
+    intros.
+    rewrite F_unfold...
+  Qed.
+
+  (* Let's call f's second parameter its "lowers" function, since it
+  provides it access to results for inputs with a lower measure.
+
+  In preparation of lemma similar to Fix_measure_F_sub_rect, but
+  for Fix_measure_sub, we first
+  need an extra hypothesis stating that the function body has the
+  same result for different "lowers" functions (g and h below) as long
+  as those produce the same results for lower inputs, regardless
+  of the lt proofs. *)
+
+  Hypothesis equiv_lowers:
+    forall x0 (g h: forall x: {y: A | m y < m x0}, P (proj1_sig x)),
+    (forall x p p', g (exist (fun y: A => m y < m x0) x p) = h (exist _ x p')) ->
+      f g = f h.
+
+  (* From equiv_lowers, it follows that
+   [Fix_measure_F_sub A m P f x] applications do not not
+  depend on the Acc proofs. *)
+
+  Lemma eq_Fix_measure_F_sub x (a a': Acc lt (m x)):
+    Fix_measure_F_sub A m P f x a =
+    Fix_measure_F_sub A m P f x a'.
+  Proof.
+    intros x a.
+    pattern x, (Fix_measure_F_sub A m P f x a).
+    apply Fix_measure_F_sub_rect.
+    intros.
+    rewrite F_unfold.
+    apply equiv_lowers.
+    intros.
+    apply H.
+    assumption.
+  Qed.
+
+  (* Finally, Fix_measure_F_rect lets one prove a property of
+  functions defined using Fix_measure_F by showing that
+  property to be invariant over single application of the function
+  body (f). *)
+
+  Lemma Fix_measure_sub_rect
+    (Q: forall x, P x -> Type)
+    (inv: forall
+      (x: A)
+      (H: forall (y: A), MR lt m y x -> Q y (Fix_measure_sub A m P f y))
+      (a: Acc lt (m x)),
+        Q x (f (fun y: {y: A | m y < m x} => Fix_measure_sub A m P f (proj1_sig y))))
+    : forall x, Q _ (Fix_measure_sub A m P f x).
+  Proof with auto.
+    unfold Fix_measure_sub.
+    intros.
+    apply Fix_measure_F_sub_rect.
+    intros.
+    assert (forall y: A, MR lt m y x0 -> Q y (Fix_measure_F_sub A m P f y (lt_wf (m y))))...
+    set (inv x0 X0 a). clearbody q.
+    rewrite <- (equiv_lowers (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (lt_wf (m (proj1_sig y)))) (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
+    intros.
+    apply eq_Fix_measure_F_sub.
+  Qed.
+
+End Fix_measure_rects.
+
+(** Tactic to fold a definitions based on [Fix_measure_sub]. *)
+
+Ltac fold_sub f :=
+  match goal with
+    | [ |- ?T ] => 
+      match T with
+        appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => 
+        let app := context C [ f arg ] in
+          change app
+      end
+  end.
+
+(** This module provides the fixpoint equation provided one assumes
+   functional extensionality. *)
+
+Module WfExtensionality.
+
+  Require Import FunctionalExtensionality.
+
+  (** The two following lemmas allow to unfold a well-founded fixpoint definition without
+     restriction using the functional extensionality axiom. *)
+  
+  (** For a function defined with Program using a well-founded order. *)
+
+  Program Lemma fix_sub_eq_ext :
+    forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Set)
+      (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y).
+  Proof.
+    intros ; apply Fix_eq ; auto.
+    intros.
+    assert(f = g).
+    extensionality y ; apply H.
+    rewrite H0 ; auto.
+  Qed.
+
+  (** For a function defined with Program using a measure. *)
+  
+  Program Lemma fix_sub_measure_eq_ext :
+    forall (A : Type) (f : A -> nat) (P : A -> Type)
+      (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
+      forall x : A,
+        Fix_measure_sub A f P F_sub x =
+          F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).
+  Proof.
+    intros ; apply Fix_measure_eq ; auto.
+    intros.
+    assert(f0 = g).
+    extensionality y ; apply H.
+    rewrite H0 ; auto.
+  Qed.
+  
+  (** Tactic to unfold once a definition based on [Fix_measure_sub]. *)
+  
+  Ltac unfold_sub f fargs := 
+    set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
+      rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
+
+End WfExtensionality.