Download Preuves Constructives

21 janvier 2005
86
si ce n'est que la sorte n'est pas la même. Dans ce dernier cas, on a une disjonction dans
(un tiers-exclu pour le prédicat
Set,
eq)
Prop
alors que dans le précédent on a une disjonction dans
c'est-à-dire un programme décidant de l'égalité.
L'extraction de
sumbool
est un type isomorphe à
bool
:
Coq < Extraction sumbool.
type sumbool =
| Left
| Right
En pratique on peut indiquer à l'extraction de
lieu de
Left
et
Right
Coq d'utiliser directement les booléens de ML au
if-then-else dans le code extrait).
(permet notamment d'utiliser
Variante sumor
Il existe une variante à
sumbool
où les sortes ne sont pas les mêmes à gauche et à droite :
Coq < Inductive sumor (A : Set) (B : Prop) : Set :=
Coq <
| inleft : A -> A + {B}
Coq <
| inright : B -> A + {B}
Cet inductif permet de spécier une fonction ML qui retourne une valeur du type
le constructeur
inleft
inright
représente le cas
Some et lui
option de ML :
représente le cas
isomorphe au type
None
et lui associe la propriété
associe la spécication
A.
B,
α option
:
et le constructeur
De fait, l'extraction de
sumor
est
Coq < Extraction sumor.
type 'a sumor =
| Inleft of 'a
| Inright
On peut ainsi combiner
sumor
et
sig
pour spécier la fonction
min_elt
de la manière sui-
vante :
Coq < Definition min_elt :
Coq <
forall s, bst s ->
Coq <
{ m:Z | In m s /\ forall x, In x s -> m <= x } + { s=Empty }.
Il s'agit là de la version correspondant à une fonction ML rendue totale avec un type
On peut de même combiner
sumor
et
sumbool
option.
pour spécier notre fonction de comparaison
ternaire :
Coq < Hypothesis compare : forall x y, {x<y} + {x=y} + {x>y}.
On note que maintenant cette seule hypothèse remplace à elle seule l'inductif
hypothèses
compare
et
compare_spec.
order
et les deux
Reprenons l'exemple de la fonction de test d'appartenance dans un arbre binaire de recherche,
mem.
On peut maintenant la spécier à l'aide d'un type dépendant :
Coq < Definition mem :
Coq <
forall x s, bst s -> { In x s }+{ ~(In x s) }.