Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

10 files changed, 601 insertions, 168 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index a1a78acc..29494069 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -5,19 +5,19 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id: Basics.v 11709 2008-12-20 11:42:15Z msozeau $ *)
 
-(* 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: Basics.v 11046 2008-06-03 22:48:06Z msozeau $ *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+   91405 Orsay, France *)
 
-(** The polymorphic identity function. *)
+(** The polymorphic identity function is defined in [Datatypes]. *)
 
-Definition id {A} := fun x : A => x.
+Implicit Arguments id [[A]].
 
 (** Function composition. *)
 
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index e267fbbe..ae9749de 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: Combinators.v 11709 2008-12-20 11:42:15Z msozeau $ *)
 
-(* 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/Equality.v b/theories/Program/Equality.v
index c776070a..99d54755 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U") -*- *)
+(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Equality.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -20,6 +20,10 @@ Require Import Coq.Program.Tactics.
 
 Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
 
+(** Notation for the single element of [x = x] *)
+
+Notation "'refl'" := (@refl_equal _ _).
+
 (** Do something on an heterogeneous equality appearing in the context. *)
 
 Ltac on_JMeq tac := 
@@ -30,7 +34,7 @@ Ltac on_JMeq tac :=
 (** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
 
 Ltac simpl_one_JMeq :=
-  on_JMeq ltac:(fun H => replace_hyp H (JMeq_eq H)).
+  on_JMeq ltac:(fun H => apply JMeq_eq in H).
 
 (** Repeat it for every possible hypothesis. *)
 
@@ -185,7 +189,6 @@ Ltac simplify_eqs :=
 (** A tactic that tries to remove trivial equality guards in induction hypotheses coming
    from [dependent induction]/[generalize_eqs] invocations. *)
 
-
 Ltac simpl_IH_eq H :=
   match type of H with
     | @JMeq _ ?x _ _ -> _ =>
@@ -224,9 +227,291 @@ Ltac do_simpl_IHs_eqs :=
 
 Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
 
-Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; 
+(** We split substitution tactics in the two directions depending on which 
+   names we want to keep corresponding to the generalization performed by the
+   [generalize_eqs] tactic. *)
+
+Ltac subst_left_no_fail :=
+  repeat (match goal with 
+            [ H : ?X = ?Y |- _ ] => subst X
+          end).
+
+Ltac subst_right_no_fail :=
+  repeat (match goal with 
+            [ H : ?X = ?Y |- _ ] => subst Y
+          end).
+
+Ltac inject_left H :=
+  progress (inversion H ; subst_left_no_fail ; clear_dups) ; clear H.
+
+Ltac inject_right H :=
+  progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H.
+
+Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
+Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
+
+Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+
+Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; 
   simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
 
+Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+
+(** Support for the [Equations] command.
+   These tactics implement the necessary machinery to solve goals produced by the 
+   [Equations] command relative to dependent pattern-matching. 
+   It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by
+   Goguen, McBride and McKinna. *)
+
+
+(** The NoConfusionPackage class provides a method for making progress on proving a property
+   [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given
+   [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where 
+   [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P].
+   This gives a general method for simplifying by discrimination or injectivity of constructors.
+   
+   Some actual instances are defined later in the file using the more primitive [discriminate] and
+   [injection] tactics on which we can always fall back.
+   *)
+  
+Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }.
+
+(** The [DependentEliminationPackage] provides the default dependent elimination principle to
+   be used by the [equations] resolver. It is especially useful to register the dependent elimination
+   principles for things in [Prop] which are not automatically generated. *)
+
+Class DependentEliminationPackage (A : Type) :=
+  { elim_type : Type ; elim : elim_type }.
+
+(** A higher-order tactic to apply a registered eliminator. *)
+
+Ltac elim_tac tac p := 
+  let ty := type of p in
+  let eliminator := eval simpl in (elim (A:=ty)) in
+    tac p eliminator.
+
+(** Specialization to do case analysis or induction. 
+   Note: the [equations] tactic tries [case] before [elim_case]: there is no need to register 
+   generated induction principles. *)
+
+Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
+Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
+
+(** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype,
+   allowing to talk about course-of-value recursion on it. *)
+
+Class BelowPackage (A : Type) := {
+  Below : A -> Type ;
+  below : Π (a : A), Below a }.
+
+(** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
+
+Class Recursor (A : Type) (BP : BelowPackage A) := 
+  { rec_type : A -> Type ; rec : Π (a : A), rec_type a }.
+
+(** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)
+
+Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x).
+Proof. intros; subst. apply X. Defined.
+
+Lemma solution_right : Π A (B : A -> Type) (t : A), B t -> (Π x, t = x -> B x).
+Proof. intros; subst; apply X. Defined.
+
+Lemma deletion : Π A B (t : A), B -> (t = t -> B).
+Proof. intros; assumption. Defined.
+
+Lemma simplification_heq : Π A B (x y : A), (x = y -> B) -> (JMeq x y -> B).
+Proof. intros; apply X; apply (JMeq_eq H). Defined.
+
+Lemma simplification_existT2 : Π A (P : A -> Type) B (p : A) (x y : P p),
+  (x = y -> B) -> (existT P p x = existT P p y -> B).
+Proof. intros. apply X. apply inj_pair2. exact H. Defined.
+
+Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q),
+  (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
+Proof. intros. injection H. intros ; auto. Defined.
+  
+Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p).
+Proof. intros. rewrite (UIP_refl A). assumption. Defined.
+
+(** This hint database and the following tactic can be used with [autosimpl] to 
+   unfold everything to [eq_rect]s. *)
+
+Hint Unfold solution_left solution_right deletion simplification_heq
+  simplification_existT1 simplification_existT2
+  eq_rect_r eq_rec eq_ind : equations.
+
+(** Simply unfold as much as possible. *)
+
+Ltac unfold_equations := repeat progress autosimpl with equations.
+
+(** The tactic [simplify_equations] is to be used when a program generated using [Equations] 
+   is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *) 
+
+Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). 
+
+(** We will use the [block_induction] definition to separate the goal from the 
+   equalities generated by the tactic. *)
+
+Definition block_dep_elim {A : Type} (a : A) := a.
+
+(** Using these we can make a simplifier that will perform the unification 
+   steps needed to put the goal in normalised form (provided there are only
+   constructor forms). Compare with the lemma 16 of the paper.
+   We don't have a [noCycle] procedure yet. *) 
+
+Ltac simplify_one_dep_elim_term c :=
+  match c with
+    | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
+    | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
+    | eq (existT _ _ _) (existT _ _ _) -> _ => 
+      refine (simplification_existT2 _ _ _ _ _ _ _) ||
+        refine (simplification_existT1 _ _ _ _ _ _ _ _)
+    | ?x = ?y -> _ => (* variables case *)
+      (let hyp := fresh in intros hyp ;
+        move hyp before x ;
+          generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) ||
+      (let hyp := fresh in intros hyp ;
+        move hyp before y ;
+          generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0)
+    | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P)
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
+    | ?t = ?u -> _ => let hyp := fresh in
+      intros hyp ; elimtype False ; discriminate
+    | ?x = ?y -> _ => let hyp := fresh in
+      intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
+        case hyp ; clear hyp
+    | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
+    | _ => intro
+  end.
+
+Ltac simplify_one_dep_elim :=
+  match goal with
+    | [ |- ?gl ] => simplify_one_dep_elim_term gl
+  end.
+
+(** Repeat until no progress is possible. By construction, it should leave the goal with
+   no remaining equalities generated by the [generalize_eqs] tactic. *)
+
+Ltac simplify_dep_elim := repeat simplify_one_dep_elim.
+
+(** To dependent elimination on some hyp. *)
+
+Ltac depelim id :=
+  generalize_eqs id ; destruct id ; simplify_dep_elim.
+
+(** Do dependent elimination of the last hypothesis, but not simplifying yet
+   (used internally). *)
+
+Ltac destruct_last :=
+  on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id).
+
+(** The rest is support tactics for the [Equations] command. *)
+
+(** Notation for inaccessible patterns. *)
+
+Definition inaccessible_pattern {A : Type} (t : A) := t.
+
+Notation "?( t )" := (inaccessible_pattern t).
+
+(** To handle sections, we need to separate the context in two parts:
+   variables introduced by the section and the rest. We introduce a dummy variable 
+   between them to indicate that. *)
+
+CoInductive end_of_section := the_end_of_the_section.
+
+Ltac set_eos := let eos := fresh "eos" in 
+  assert (eos:=the_end_of_the_section).
+
+(** We have a specialized [reverse_local] tactic to reverse the goal until the begining of the
+   section variables *)
+
+Ltac reverse_local :=
+  match goal with
+    | [ H : ?T |- _ ] => 
+      match T with
+        | end_of_section => idtac | _ => revert H ; reverse_local end
+    | _ => idtac
+  end.
+
+(** Do as much as possible to apply a method, trying to get the arguments right.
+   !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some 
+   non-dependent arguments of the method can remain after [apply]. *)
+
+Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m).
+
+(** Hopefully the first branch suffices. *)
+
+Ltac try_intros m :=
+  solve [ intros ; unfold block_dep_elim ; refine m || apply m ] ||
+  solve [ unfold block_dep_elim ; simpl_intros m ].
+
+(** To solve a goal by inversion on a particular target. *)
+
+Ltac solve_empty target :=
+  do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim.
+
+Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local.
+
+(** Solving a method call: we can solve it by splitting on an empty family member
+   or we must refine the goal until the body can be applied. *)
+    
+Ltac solve_method rec :=
+  match goal with
+    | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body)
+    | [ H := [ ?body ] : ?T |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros (body:T)
+  end.
+
+(** Impossible cases, by splitting on a given target. *)
+
+Ltac solve_split :=
+  match goal with 
+    | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x)
+  end.
+
+(** If defining recursive functions, the prototypes come first. *)
+
+Ltac intro_prototypes :=
+  match goal with 
+    | [ |- Π x : _, _ ] => intro ; intro_prototypes
+    | _ => idtac
+  end.
+
+Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
+Ltac do_ind p := induction p || elim_ind p.
+
+Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
+
+Ltac un_dep_elimify := unfold block_dep_elim in *.
+
+Ltac case_last := dep_elimify ;
+  on_last_hyp ltac:(fun p => 
+    let ty := type of p in
+      match ty with
+        | ?x = ?x => revert p ; refine (simplification_K _ x _ _)
+        | ?x = ?y => revert p
+        | _ => simpl in p ; generalize_eqs p ; do_case p
+      end).
+
+Ltac nonrec_equations := 
+  solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ]
+    || fail "Unnexpected equations goal".
+
+Ltac recursive_equations :=
+  solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ] 
+    || fail "Unnexpected recursive equations goal".
+
+(** The [equations] tactic is the toplevel tactic for solving goals generated
+   by [Equations]. *)
+
+Ltac equations := set_eos ;
+  match goal with 
+    | [ |- Π x : _, _ ] => intro ; recursive_equations
+    | _ => nonrec_equations
+  end.
+
 (** The following tactics allow to do induction on an already instantiated inductive predicate
    by first generalizing it and adding the proper equalities to the context, in a maner similar to 
    the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
@@ -235,43 +520,49 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ;
    and starts a dependent induction using this tactic. *)
 
 Ltac do_depind tac H :=
-  generalize_eqs_vars H ; tac H ; repeat progress simpl_depind.
+  (try intros until H) ; dep_elimify ; generalize_eqs_vars H ; tac H ; simplify_dep_elim ; un_dep_elimify.
 
 (** A variant where generalized variables should be given by the user. *)
 
 Ltac do_depind' tac H :=
-  generalize_eqs H ; tac H ; repeat progress simpl_depind.
+  (try intros until H) ; dep_elimify ; generalize_eqs H ; tac H ; simplify_dep_elim ; un_dep_elimify.
 
-(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *)
+(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
+   By default, we don't try to generalize the hyp by its variable indices.  *)
 
 Tactic Notation "dependent" "destruction" ident(H) := 
-  do_depind ltac:(fun hyp => destruct hyp ; intros) H ; subst*.
+  do_depind' ltac:(fun hyp => do_case hyp) H.
 
 Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
-  do_depind ltac:(fun hyp => destruct hyp using c ; intros) H.
+  do_depind' ltac:(fun hyp => destruct hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
 Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
-  do_depind' ltac:(fun hyp => revert l ; destruct hyp ; intros) H.
+  do_depind' ltac:(fun hyp => revert l ; do_case hyp) H.
 
 Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
-  do_depind' ltac:(fun hyp => revert l ; destruct hyp using c ; intros) H.
+  do_depind' ltac:(fun hyp => revert l ; destruct hyp using c) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
-   writting another wrapper calling do_depind. *)
+   writting another wrapper calling do_depind. We suppose the hyp has to be generalized before
+   calling [induction]. *)
 
 Tactic Notation "dependent" "induction" ident(H) := 
-  do_depind ltac:(fun hyp => induction hyp ; intros) H.
+  do_depind ltac:(fun hyp => do_ind hyp) H.
 
 Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
-  do_depind ltac:(fun hyp => induction hyp using c ; intros) H.
+  do_depind ltac:(fun hyp => induction hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
-  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp ; intros) H.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
-  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
 
+Ltac simplify_IH_hyps := repeat
+  match goal with
+    | [ hyp : _ |- _ ] => specialize_hypothesis hyp
+  end.
\ No newline at end of file
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
deleted file mode 100644
index b5ad5b4d..00000000
--- a/theories/Program/FunctionalExtensionality.v
+++ /dev/null
@@ -1,109 +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: FunctionalExtensionality.v 10739 2008-04-01 14:45:20Z herbelin $ 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 equality. *)
-
-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 equality 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.
-
-
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index b6c3031e..7d0c3948 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: Program.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+
 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 d021326a..3d551281 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: Subset.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+
+(** 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 6cd75257..222b5c8d 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: Syntax.v 11823 2009-01-21 15:32:37Z msozeau $ *)
 
-(* 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.
@@ -53,7 +53,7 @@ Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))
 Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
   (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
 
-Tactic Notation "exist" constr(x) := exists x.
-Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
-Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
-Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+Tactic Notation "exists" constr(x) := exists x.
+Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y.
+Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
+Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index bb5054b4..499629a6 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -6,11 +6,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: Tactics.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
 
 (** This module implements various tactics used to simplify the goals produced by Program,
    which are also generally useful. *)
 
+(** The [do] tactic but using a Coq-side nat. *)
+
+Ltac do_nat n tac :=
+  match n with
+    | 0 => idtac
+    | S ?n' => tac ; do_nat n' tac
+  end.
+
+(** Do something on the last hypothesis, or fail *)
+
+Ltac on_last_hyp tac :=
+  match goal with [ H : _ |- _ ] => tac H || fail 1 end.
+
 (** Destructs one pair, without care regarding naming. *)
 
 Ltac destruct_one_pair :=
@@ -80,7 +93,7 @@ Ltac clear_dup :=
         | [ H' : ?Y |- _ ] =>
           match H with
             | H' => fail 2
-            | _ => conv X Y ; (clear H' || clear H)
+            | _ => unify X Y ; (clear H' || clear H)
           end
       end
   end.
@@ -91,7 +104,7 @@ Ltac clear_dups := repeat clear_dup.
 
 Ltac subst_no_fail :=
   repeat (match goal with 
-            [ H : ?X = ?Y |- _ ] => subst X || subst Y                  
+            [ H : ?X = ?Y |- _ ] => subst X || subst Y
           end).
 
 Tactic Notation "subst" "*" := subst_no_fail.
@@ -108,6 +121,26 @@ Ltac on_application f tac T :=
     | context [f ?x ?y] => tac (f x y) 
     | context [f ?x] => tac (f x)
   end.
+
+(** A variant of [apply] using [refine], doing as much conversion as necessary. *)
+
+Ltac rapply p := 
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
   
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 
@@ -154,13 +187,14 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i
 
 (** Try to inject any potential constructor equality hypothesis. *)
 
-Ltac autoinjection :=
-  let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in
-    match goal with
-      | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
-    end.
+Ltac autoinjection tac :=
+  match goal with
+    | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+  end.
+
+Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H.
 
-Ltac autoinjections := repeat autoinjection.
+Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject).
 
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)
 
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index fcd85f41..b08093bf 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Utils.v 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: Utils.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
+
+(** Various syntaxic shortands that are useful with [Program]. *)
 
 Require Export Coq.Program.Tactics.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index b6ba5d44..12bdf3a7 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: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+
+(** 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.