Download Le Coq` Art (V8)

16.3. ** RÉCURSION GÉNÉRALE PAR ITÉRATION
465
toute valeur en entrée x une valeur v telle que “F k g x = v” ne dépende pas de g
(et on peut alors en déduire qu’elle ne dépend pas de k dès qu’il est assez grand).
Nous pourrons nous contenter de prouver l’existence de cette valeur. Ainsi on est
amené à construire une fonction f_terminates spécifiée de la façon suivante :
Fixpoint iter (A:Set)(n:nat)(F:A→A)(g:A){struct n} : A :=
match n with O ⇒ g | S p ⇒ F (iter A p F g) end.
Implicit Arguments iter [A].
Definition f_terminates:
(n:A)
{v: B| (Ex [p:nat]
(k:nat)(g:A→B)(iter (A→B) k F g x)=v)}.
Pour construire cette f_terminates nous procédons par preuve et cette
preuve est basée sur une récurrence bien fondée sur la variable qui décroît à
chaque appel. Ensuite la structure de la preuve suit exactement la structure de
la fonction F.
Par exemple, pour la fonction de division, on écrit de la façon suivante :
Definition div_it_terminates :
∀ n m:nat, 0 < m →
{v : nat * nat |
exists p : nat |
(∀ k:nat, p < k → ∀ g:nat → nat → nat * nat,
iter k div_it_F g n m = v)}.
intros n; elim n using (well_founded_induction lt_wf).
intros n’ Hrec m Hlt.
caseEq (le_gt_dec m n’); intros H Heq_test.
Comme nous avons suivi la structure de la fonctionnelle div_it_F, nous avons
effectué un traitement par cas sur la valeur de “le_gt_dec m n’.” Nous n’avons
pas effectué ce traitement directement avec la tactique case, mais avec la tactique caseEq que nous avons définie en section 7.2.7. En effet, nous aurons
plusieurs fois besoin de raisonner sur la façon dont ce traitement par cas se
réduit. Le premier des deux cas est exprimé par le but suivant :
...
H : m ≤ n’
Heq_test : le_gt_dec m n’ = left (m > n’) H
============================
{v:nat*nat |
∃ p:nat
| (∀ k:nat,
p<k→
∀ g:nat→nat→nat*nat, iter k div_it_F g n’ m = v)}