# Library Coq.Numbers.Natural.Abstract.NStrongRec

This file defined the strong (course-of-value, well-founded) recursion and proves its properties
Require Export NSub.
Module NStrongRecPropFunct (Import N : NAxiomsSig').
Include NSubPropFunct N.
Section StrongRecursion.
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.

Definition strong_rec (a : A) (f : (N.t -> A) -> N.t -> A) (n : N.t) : A :=
recursion (fun _ => a) (fun _ => f) (S n) n.
For convenience, we use in proofs an intermediate definition between recursion and strong_rec.
Definition strong_rec0 (a : A) (f : (N.t -> A) -> N.t -> A) : N.t -> N.t -> A :=
recursion (fun _ => a) (fun _ => f).
Lemma strong_rec_alt : forall a f n,
strong_rec a f n = strong_rec0 a f (S n) 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).
Instance strong_rec0_wd :
Proper (Aeq ==> (( N.eq ==> Aeq ) ==> N.eq ==> Aeq ) ==> N.eq ==> N.eq ==> Aeq)
strong_rec0.
Instance strong_rec_wd :
Proper (Aeq ==> (( N.eq ==> Aeq ) ==> N.eq ==> Aeq ) ==> N.eq ==> Aeq) strong_rec.
Section FixPoint.
Variable f : (N.t -> A) -> N.t -> A.
Variable f_wd : Proper (( N.eq ==> Aeq )==> N.eq ==> Aeq) f.
Lemma strong_rec0_0 : forall a m,
( strong_rec0 a f 0 m ) = a.
Lemma strong_rec0_succ : forall a n m,
Aeq (strong_rec0 a f (S n) m) (f (strong_rec0 a f n) m).
Lemma strong_rec_0 : forall a,
Aeq (strong_rec a f 0) (f (fun _ => a) 0).
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).
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).
Theorem strong_rec_fixpoint : forall (a : A) (n : N.t),
Aeq (strong_rec a f n) (f (strong_rec a f) n).
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...
Theorem strong_rec_0_any : forall (a : A)(any : N.t->A),
Aeq (strong_rec a f 0) (f any 0).
... 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).
End FixPoint.
End StrongRecursion.
Implicit Arguments strong_rec [A].
End NStrongRecPropFunct.