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

1 files changed, 205 insertions, 2 deletions

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index b6ba5d44e..5d005d273 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.