Rewrite of Program Fixpoint to overcome the previous limitations:

- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments. 
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.


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

1 files changed, 50 insertions, 133 deletions

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 5d005d273..497e60205 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -85,78 +85,6 @@ End Well_founded.
 
 Extraction Inline Fix_F_sub Fix_sub.
 
-Require Import Wf_nat.
-Require Import Lt.
-
-Section Well_founded_measure.
-  Variable A : Type.
-  Variable m : A -> nat.
-  
-  Section Acc.
-    
-    Variable P : A -> Type.
-    
-    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
-    
-    Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
-      F_sub x (fun (y : A | m y < m x)  => Fix_measure_F_sub y
-        (@Acc_inv _ _ _ r (m y) (proj2_sig y))).
-    
-    Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
-  
-  End Acc.
-
-  Section FixPoint.
-    Variable P : A -> Type.
-    
-    Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x.
-    
-    Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
-    
-    Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
-    
-    Hypothesis
-      F_ext :
-      forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
-        (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
-
-    Program Lemma Fix_measure_F_eq :
-      forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r.
-    Proof.
-      intros x.
-      set (y := m x).
-      unfold Fix_measure_F_sub.
-      intros r ; case r ; auto.
-    Qed.
-    
-    Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
-    Proof.
-      intros x r s.
-      rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
-    Qed.
-
-    Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
-    Proof.
-      intro x; unfold Fix_measure in |- *.
-      rewrite <- (Fix_measure_F_eq ).
-      apply F_ext; intros.
-      apply Fix_measure_F_inv.
-    Qed.
-
-    Lemma fix_measure_sub_eq : forall x : A,
-      Fix_measure_sub P F_sub x =
-        let f_sub := F_sub in
-          f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
-      exact Fix_measure_eq.
-    Qed.
-
- End FixPoint.
-
-End Well_founded_measure.
-
-Extraction Inline Fix_measure_F_sub Fix_measure_sub.
-
 Set Implicit Arguments.
 
 (** Reasoning about well-founded fixpoints on measures. *)
@@ -165,7 +93,7 @@ Section Measure_well_founded.
 
   (* Measure relations are well-founded if the underlying relation is well-founded. *)
 
-  Variables T M: Set.
+  Variables T M: Type.
   Variable R: M -> M -> Prop.
   Hypothesis wf: well_founded R.
   Variable m: T -> M.
@@ -189,38 +117,41 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
-Section Fix_measure_rects.
+Hint Resolve measure_wf.
+
+Section Fix_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.
+  Variable R : A -> A -> Prop.
+  Variable Rwf : well_founded R.
+  Variable f: forall (x : A), (forall y: { y: A | R y 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))).
+    Fix_F_sub A R P f x r =
+    f (fun y => Fix_F_sub A R 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
+  (* Fix_F_sub_rect lets one prove a property of
+  functions defined using Fix_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
+  Lemma Fix_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).
+     (forall (y: A) (H: R y x) (a: Acc R y),
+        Q y (Fix_F_sub A R P f y a)) ->
+        forall (a: Acc R x),
+          Q x (f (fun y: {y: A | R y x} =>
+            Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
+    : forall x a, Q _ (Fix_F_sub A R 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.
+    set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)).
+    cut (forall x, R' x)...
+    apply (well_founded_induction_type Rwf).
+    subst R'.
     simpl.
     intros.
     rewrite F_unfold...
@@ -229,29 +160,29 @@ Section Fix_measure_rects.
   (* 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
+  In preparation of lemma similar to Fix_F_sub_rect, but
+  for Fix_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')) ->
+    forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)),
+    (forall x p p', g (exist (fun y: A => R y 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
+   [Fix_F_sub A R 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'.
+  Lemma eq_Fix_F_sub x (a a': Acc R x):
+    Fix_F_sub A R P f x a =
+    Fix_F_sub A R 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.
+    pattern x, (Fix_F_sub A R P f x a).
+    apply Fix_F_sub_rect.
     intros.
     rewrite F_unfold.
     apply equiv_lowers.
@@ -260,32 +191,34 @@ Section Fix_measure_rects.
     assumption.
   Qed.
 
-  (* Finally, Fix_measure_F_rect lets one prove a property of
-  functions defined using Fix_measure_F by showing that
+  (* Finally, Fix_F_rect lets one prove a property of
+  functions defined using Fix_F by showing that
   property to be invariant over single application of the function
   body (f). *)
 
-  Lemma Fix_measure_sub_rect
+  Lemma Fix_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).
+      (H: forall (y: A), R y x -> Q y (Fix_sub A R Rwf P f y))
+      (a: Acc R x),
+        Q x (f (fun y: {y: A | R y x} => Fix_sub A R Rwf P f (proj1_sig y))))
+    : forall x, Q _ (Fix_sub A R Rwf P f x).
   Proof with auto.
-    unfold Fix_measure_sub.
+    unfold Fix_sub.
     intros.
-    apply Fix_measure_F_sub_rect.
+    apply Fix_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))))...
+    assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf 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))))...
+    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => 
+      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) 
+    (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
     intros.
-    apply eq_Fix_measure_F_sub.
+    apply eq_Fix_F_sub.
   Qed.
 
-End Fix_measure_rects.
+End Fix_rects.
 
 (** Tactic to fold a definitions based on [Fix_measure_sub]. *)
 
@@ -293,7 +226,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] => 
       match T with
-        appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => 
+        appcontext C [ @Fix_sub _ _ _ _ ?arg ] => 
         let app := context C [ f arg ] in
           change app
       end
@@ -325,27 +258,11 @@ Module WfExtensionality.
     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]. *)
+  (** Tactic to unfold once a definition based on [Fix_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.
+      rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
 
 End WfExtensionality.