Download Le Coq` Art (V8)

16.3. ** RÉCURSION GÉNÉRALE PAR ITÉRATION
469
intros n m h.
unfold div_it; case (div_it_terminates n m h).
intros v Hex1; case (div_it_terminates (n-m) m h).
intros v’ Hex2.
elim Hex2; elim Hex1; intros p Heq1 p’ Heq2.
rewrite <- Heq1 with
(k := S (S (max p p’)))(g := fun x y:nat ⇒ v).
rewrite <- Heq2 with (k := S (max p p’))
(g := fun x y:nat ⇒ v).
reflexivity.
eauto with arith.
eauto with arith.
Qed.
16.3.4
Utilisation de l’équation de point fixe
Maintenant que nous disposons de l’équation de point fixe, il est assez aisé
de démontrer que notre fonction de division satisfait la spécification usuelle de
la division. Nous ne montrons ici que la première partie de la spécification.
Cette démonstration se fait par récurrence bien fondée sur l’argument qui doit
décroître entre chaque appel. Après l’étape de récurrence, la démonstration suit
la structure de la fonction.
Theorem div_it_correct1 :
∀ (m n:nat)(h:0 < n),
m = fst (div_it m n h) * n + snd (div_it m n h).
Proof.
intros m; elim m using (well_founded_ind lt_wf).
intros m’ Hrec n h; rewrite div_it_fix_eqn.
case (le_gt_dec n m’); intros H; trivial.
pattern m’ at 1; rewrite (le_plus_minus n m’); auto.
pattern (m’-n) at 1.
rewrite Hrec with (m’-n) n h; auto with arith.
case (div_it (m’-n) n h); simpl; auto with arith.
Qed.
Exercice 16.16 * Démontrer la deuxième partie de la correction de div_it :
∀ (m n:nat)(h:0 < n), snd (div_it m n h) < n.
16.3.5
Discussion
La technique présentée dans cette section permet de travailler séparément
sur l’algorithme (représenté par la fonctionnelle F), la preuve de terminaison de
cet algorithme (représenté par la construction de la fonction f_terminates), et
la vérification que la fonction satisfait sa spécification, où l’équation de point
fixe joue un rôle important. Nous avons donné entièrement les démonstrations