1 files changed, 205 insertions, 2 deletions
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.