Download Le Coq` Art (V8)

346
CHAPITRE 12. * ÉTUDE DE CAS
total de cet arbre en cas d’absence de l’information cherchée. Ce manque d’efficacité peut être évité si l’on restreint le test d’occurrence à une classe d’arbres
binaires possédant des propriétés qui rendent inutile un tel parcours complet.
Caractérisation des arbres de recherche
Nous pouvons définir de façon inductive le prédicat « être un arbre de recherche » :
– Toute feuille est un arbre de recherche,
– Si t1 et t2 sont des arbres de recherche, et si n est strictement supérieur
à toute étiquette de t1 et inférieur à toute étiquette de t2 , alors l’arbre de
racine n, de fils gauche t1 et de fils droit t2 est un arbre de recherche.
La formalisation en Coq se fait en trois étapes :
1. Définition d’un prédicat à deux places “ min z t ” : « z est inférieur à
toute étiquette de t »,
2. idem pour “ maj z t ” : « z est supérieur à toute étiquette de t »,
3. Définition inductive de search_tree: Z_btree → Prop, utilisant maj et
min comme prédicats auxiliaires.
Inductive min (n:Z)(t:Z_btree) : Prop :=
min_intro : (∀ p:Z, occ p t → n < p)→ min n t.
Inductive maj (n:Z)(t:Z_btree) : Prop :=
maj_intro : (∀ p:Z, occ p t → p < n)→ maj n t.
Inductive search_tree : Z_btree→Prop :=
| leaf_search_tree : search_tree Z_leaf
| bnode_search_tree :
∀ (n:Z)(t1 t2:Z_btree),
search_tree t1 → search_tree t2 → maj n t1 → min n t2 →
search_tree (Z_bnode n t1 t2).
Remarque 12.1 Il peut paraître surprenant que min et maj soient définies de
façon inductive ; le lecteur peut trouver plus naturelle une simple définition de
la forme suivante :
Definition min (n:Z)(t:Z_btree) : Prop :=
∀ p:Z, occ p t → n < p.
L’auteur de ce développement a préféré le confort d’un type inductif à un seul
constructeur, qui lui permet d’utiliser les tactiques split en introduction et
case en élimination, alors que la définition ci-dessus obligerait à contrôler la
δ-expansion de min par la tactique unfold ; d’autre part, une utilisation mal
maîtrisée d’unfold pourrait provoquer des expansions de min non voulues, et
perturber la lisibilité des buts. Avec la solution retenue, les constructions et