The right tactics for definitions using measures.

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

2 files changed, 73 insertions, 12 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 46121ff18..3734db855 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -75,23 +75,70 @@ Require Import Wf_nat.
 Require Import Lt.
 
 Section Well_founded_measure.
-Variable A : Type.
-Variable f : A -> nat.
-Definition R := fun x y => f x < f y.
+  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.
+    
+    Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
+      F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
+        (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
+    
+    Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
+  
+  End Acc.
 
-Section FixPoint.
+  Section FixPoint.
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig 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.
 
-Variable P : A -> Type.
+    Lemma Fix_measure_F_eq :
+      forall (x:A) (r:Acc lt (m x)),
+        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (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.
 
-Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
- 
-Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
-   F_sub x (fun y: { y : A | f y < f x}  => Fix_measure_F_sub (proj1_sig y) 
-   (Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
+    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.
 
-Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
+    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 FixPoint.
 
 End Well_founded_measure.
 
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
index 1a12ac824..07a19ab37 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -23,3 +23,17 @@ Proof.
   apply (fun_extensionality_dep _ _ _ _ H).
   rewrite H0 ; auto.
 Qed.
+
+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).
+  apply (fun_extensionality_dep _ _ _ _ H).
+  rewrite H0 ; auto.
+Qed.