1 files changed, 154 insertions, 77 deletions
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index c6a6da48..cbbcdbff 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -8,123 +8,200 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NStrongRec.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** This file defined the strong (course-of-value, well-founded) recursion
 and proves its properties *)
 
 Require Export NSub.
 
-Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NSubPropMod := NSubPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Module NStrongRecPropFunct (Import N : NAxiomsSig').
+Include NSubPropFunct N.
 
 Section StrongRecursion.
 
-Variable A : Set.
+Variable A : Type.
 Variable Aeq : relation A.
+Variable Aeq_equiv : Equivalence Aeq.
+
+(** [strong_rec] allows to define a recursive function [phi] given by
+    an equation [phi(n) = F(phi)(n)] where recursive calls to [phi]
+    in [F] are made on strictly lower numbers than [n].
+
+    For [strong_rec a F n]:
+    - Parameter [a:A] is a default value used internally, it has no
+      effect on the final result.
+    - Parameter [F:(N->A)->N->A] is the step function:
+      [F f n] should return [phi(n)] when [f] is a function
+      that coincide with [phi] for numbers strictly less than [n].
+*)
 
-Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity).
+Definition strong_rec (a : A) (f : (N.t -> A) -> N.t -> A) (n : N.t) : A :=
+ recursion (fun _ => a) (fun _ => f) (S n) n.
 
-Hypothesis Aeq_equiv : equiv A Aeq.
+(** For convenience, we use in proofs an intermediate definition
+    between [recursion] and [strong_rec]. *)
 
-Add Relation A Aeq
- reflexivity proved by (proj1 Aeq_equiv)
- symmetry proved by (proj2 (proj2 Aeq_equiv))
- transitivity proved by (proj1 (proj2 Aeq_equiv))
-as Aeq_rel.
+Definition strong_rec0 (a : A) (f : (N.t -> A) -> N.t -> A) : N.t -> N.t -> A :=
+ recursion (fun _ => a) (fun _ => f).
 
-Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A :=
-recursion
-  (fun _ : N => a)
-  (fun (m : N) (p : N -> A) (k : N) => f k p)
-  (S n)
-  n.
+Lemma strong_rec_alt : forall a f n,
+ strong_rec a f n = strong_rec0 a f (S n) n.
+Proof.
+reflexivity.
+Qed.
 
-Theorem strong_rec_wd :
-forall a a' : A, a ==A a' ->
-  forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' ->
-    forall n n', n == n' ->
-      strong_rec a f n ==A strong_rec a' f' n'.
+(** We need a result similar to [f_equal], but for setoid equalities. *)
+Lemma f_equiv : forall f g x y,
+ (N.eq==>Aeq)%signature f g -> N.eq x y -> Aeq (f x) (g y).
+Proof.
+auto.
+Qed.
+
+Instance strong_rec0_wd :
+ Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> N.eq ==> Aeq)
+  strong_rec0.
+Proof.
+unfold strong_rec0.
+repeat red; intros.
+apply f_equiv; auto.
+apply recursion_wd; try red; auto.
+Qed.
+
+Instance strong_rec_wd :
+ Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> Aeq) strong_rec.
 Proof.
 intros a a' Eaa' f f' Eff' n n' Enn'.
-(* First we prove that recursion (which is on type N -> A) returns
-extensionally equal functions, and then we use the fact that n == n' *)
-assert (H : fun_eq Neq Aeq
-  (recursion
-    (fun _ : N => a)
-    (fun (m : N) (p : N -> A) (k : N) => f k p)
-    (S n))
-  (recursion
-    (fun _ : N => a')
-    (fun (m : N) (p : N -> A) (k : N) => f' k p)
-    (S n'))).
-apply recursion_wd with (Aeq := fun_eq Neq Aeq).
-unfold fun_eq; now intros.
-unfold fun2_eq. intros y y' Eyy' p p' Epp'. unfold fun_eq. auto.
+rewrite !strong_rec_alt.
+apply strong_rec0_wd; auto.
 now rewrite Enn'.
-unfold strong_rec.
-now apply H.
 Qed.
 
-(*Section FixPoint.
-
-Variable a : A.
-Variable f : N -> (N -> A) -> A.
+Section FixPoint.
 
-Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f.
+Variable f : (N.t -> A) -> N.t -> A.
+Variable f_wd : Proper ((N.eq==>Aeq)==>N.eq==>Aeq) f.
 
-Let g (n : N) : A := strong_rec a f n.
+Lemma strong_rec0_0 : forall a m,
+ (strong_rec0 a f 0 m) = a.
+Proof.
+intros. unfold strong_rec0. rewrite recursion_0; auto.
+Qed.
 
-Add Morphism g with signature Neq ==> Aeq as g_wd.
+Lemma strong_rec0_succ : forall a n m,
+ Aeq (strong_rec0 a f (S n) m) (f (strong_rec0 a f n) m).
 Proof.
-intros n1 n2 H. unfold g. now apply strong_rec_wd.
+intros. unfold strong_rec0.
+apply f_equiv; auto with *.
+rewrite recursion_succ; try (repeat red; auto with *; fail).
+apply f_wd.
+apply recursion_wd; try red; auto with *.
 Qed.
 
-Theorem NtoA_eq_sym : symmetric (N -> A) (fun_eq Neq Aeq).
+Lemma strong_rec_0 : forall a,
+ Aeq (strong_rec a f 0) (f (fun _ => a) 0).
 Proof.
-apply fun_eq_sym.
-exact (proj2 (proj2 NZeq_equiv)).
-exact (proj2 (proj2 Aeq_equiv)).
+intros. rewrite strong_rec_alt, strong_rec0_succ.
+apply f_wd; auto with *.
+red; intros; rewrite strong_rec0_0; auto with *.
 Qed.
 
-Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq).
+(* We need an assumption saying that for every n, the step function (f h n)
+calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
+coincide on values < n, then (f h1 n) coincides with (f h2 n) *)
+
+Hypothesis step_good :
+  forall (n : N.t) (h1 h2 : N.t -> A),
+    (forall m : N.t, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f h1 n) (f h2 n).
+
+Lemma strong_rec0_more_steps : forall a k n m, m < n ->
+ Aeq (strong_rec0 a f n m) (strong_rec0 a f (n+k) m).
 Proof.
-apply fun_eq_trans.
-exact (proj1 NZeq_equiv).
-exact (proj1 (proj2 NZeq_equiv)).
-exact (proj1 (proj2 Aeq_equiv)).
+ intros a k n. pattern n.
+ apply induction; clear n.
+
+ intros n n' Hn; setoid_rewrite Hn; auto with *.
+
+ intros m Hm. destruct (nlt_0_r _ Hm).
+
+ intros n IH m Hm.
+ rewrite lt_succ_r in Hm.
+ rewrite add_succ_l.
+ rewrite 2 strong_rec0_succ.
+ apply step_good.
+ intros m' Hm'.
+ apply IH.
+ apply lt_le_trans with m; auto.
 Qed.
 
-Add Relation (N -> A) (fun_eq Neq Aeq)
- symmetry proved by NtoA_eq_sym
- transitivity proved by NtoA_eq_trans
-as NtoA_eq_rel.
+Lemma strong_rec0_fixpoint : forall (a : A) (n : N.t),
+ Aeq (strong_rec0 a f (S n) n) (f (fun n => strong_rec0 a f (S n) n) n).
+Proof.
+intros.
+rewrite strong_rec0_succ.
+apply step_good.
+intros m Hm.
+symmetry.
+setoid_replace n with (S m + (n - S m)).
+apply strong_rec0_more_steps.
+apply lt_succ_diag_r.
+rewrite add_comm.
+symmetry.
+apply sub_add.
+rewrite le_succ_l; auto.
+Qed.
 
-Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph.
+Theorem strong_rec_fixpoint : forall (a : A) (n : N.t),
+ Aeq (strong_rec a f n) (f (strong_rec a f) n).
 Proof.
-apply f_wd.
+intros.
+transitivity (f (fun n => strong_rec0 a f (S n) n) n).
+rewrite strong_rec_alt.
+apply strong_rec0_fixpoint.
+apply f_wd; auto with *.
+intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *.
 Qed.
 
-(* We need an assumption saying that for every n, the step function (f n h)
-calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
-coincide on values < n, then (f n h1) coincides with (f n h2) *)
+(** NB: without the [step_good] hypothesis, we have proved that
+    [strong_rec a f 0] is [f (fun _ => a) 0]. Now we can prove
+    that the first argument of [f] is arbitrary in this case...
+*)
 
-Hypothesis step_good :
-  forall (n : N) (h1 h2 : N -> A),
-    (forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f n h1) (f n h2).
+Theorem strong_rec_0_any : forall (a : A)(any : N.t->A),
+ Aeq (strong_rec a f 0) (f any 0).
+Proof.
+intros.
+rewrite strong_rec_fixpoint.
+apply step_good.
+intros m Hm. destruct (nlt_0_r _ Hm).
+Qed.
 
-(* Todo:
-Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g).
+(** ... and that first argument of [strong_rec] is always arbitrary. *)
+
+Lemma strong_rec_any_fst_arg : forall a a' n,
+ Aeq (strong_rec a f n) (strong_rec a' f n).
 Proof.
-apply induction.
-unfold predicate_wd, fun_wd.
-intros x y H. rewrite H. unfold fun_eq; apply g_wd.
-reflexivity.
-unfold g, strong_rec.
-*)
+intros a a' n.
+generalize (le_refl n).
+set (k:=n) at -2. clearbody k. revert k. pattern n.
+apply induction; clear n.
+(* compat *)
+intros n n' Hn. setoid_rewrite Hn; auto with *.
+(* 0 *)
+intros k Hk. rewrite le_0_r in Hk.
+rewrite Hk, strong_rec_0. symmetry. apply strong_rec_0_any.
+(* S *)
+intros n IH k Hk.
+rewrite 2 strong_rec_fixpoint.
+apply step_good.
+intros m Hm.
+apply IH.
+rewrite succ_le_mono.
+apply le_trans with k; auto.
+rewrite le_succ_l; auto.
+Qed.
 
-End FixPoint.*)
+End FixPoint.
 End StrongRecursion.
 
 Implicit Arguments strong_rec [A].