Library Coq.Numbers.Natural.Abstract.NStrongRec
This file defined the strong (course-of-value, well-founded) recursion
and proves its properties
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.
For convenience, we use in proofs an intermediate definition
between recursion and strong_rec.
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...
... and that first argument of strong_rec is always arbitrary.