Questionnements pour gallinacés
Par David Monniaux le dimanche, août 28 2011, 15:39 - Recherche scientifique - Lien permanent
Pour la preuve de programmes en Coq, qu'apporte concrètement la contrainte de ne pas utiliser le tiers-exclu (dans Prop ; dans Set je comprends parfaitement), l'égalité extensionnelle et l'indifférence à la preuve ?
Commentaires
D'un point de vue pratique, le principal intérêt de ne pas avoir d'axiome dans Prop, c'est pour que les programmes qui utilisent la coercion de type (eq_rec) et la récurrence bien fondée (acc_rec) se réduisent. Sinon il restent bloqués sur les éventuels axiomes que tu as utilisé pour les prouver.
Cela étant dit, je ne suis pas trop convaincu de l'utilisation de eq_rec et acc_rec quand ils utilisent des preuves non triviales. C'est d'un intérêt discutable d'avoir preuve de terminaison de la fonction qui coûte plus cher que le calcul qui t'intéresse. Donc faut voir.
Après si tu n'aimes pas les maths constructives (auquel cas tu as drôlement tort), éviter le tiers-exclu ne te sert pas des masses. À moins que tu comptes distribuer une bibliothèque, auquel cas tu peux vouloir être utilisable par les constructivistes.
Pour les principes d'extensionnalité, comme la règle d'extensionnalité sur les fonctions où l'indiscernabilité des preuves, ben… ça ne change pas grand chose à la vie, il n'y a personne, à ma connaissance, qui ait spécifiquement eu besoin d'un système dont ils étaient absents.
@Arnaud Spiwack: J'ai déjà défini des programmes par récurrence sur le terme de preuve justifiant leur terminaison; à l'extraction, toute la partie « preuve » saute. Quel problème y a-t-il donc d'utiliser une preuve complexe ? Et je ne vois pas non plus où il y aurait blocage, sachant qu'à l'extraction l'axiome sautera car dans Prop ? Ou alors veux-tu parler de l'évaluation dans Coq lui-même ?
Pour le tiers-exclu et le constructivisme, je retiens la méthode de Georges Gonthier pour tout ce qui est structures finies et plus généralement propriétés décidables : pour prouver A->F, d'une part tu donnes une procédure qui teste F (autrement dit retourne { F } + { ~F }), d'autre part tu prouves A->~~F, et tu conclus...
Sinon, toujours dans le même style, je comprends qu'on ajoute l'indiscernabilité pour pouvoir manipuler des objets { x | P(x) } comme si seule la première composante importait, en revanche je ne vois pas l'intérêt de l'axiome K de Streicher, qui est plus faible... (c'est l'axiome qui dit que les preuves d'égalité sont indiscernables).
Oui, bien sûr, l'éxécution dans Coq même. Si tu es plutôt intéressé par l'extraction, tu auras moins ce genre de problème (tu te retrouves éventuellement avec des types qui ne sont pas convertibles, mais je devine que ton style n'utilise pas trop de types dépendents, et que tu n'auras pas ce genre de soucis).
L'axiome K a des utilités pratiques (évidemment, si tu as proof irrelevance, tu as K, au moins dans un sens Coq-ien des deux principes). Si tu le rajoutes comme axiomes tu vas gagner la possibilité d'utiliser les égalités dites "dépendentes" ou "John Major" ou affiliées de manière substitutive.
Une autre utilité plus technique c'est la redécoration de typage. Imagine tu as une fonction sur les listes, et tu veux la relever aux vecteurs (définis typiquement comme Inductive Vec (A:Type) : nat -> Type := nil : Vec A 0 | Cons (x:A) (l:Vec A n) : Vec A (S n) ). Une solution pour faire ça peut être d'effacer l'annotation de taille des vecteurs en entrée, lancer la fonction sur les listes, reconstruire les annotations en sortie. Ce genre de truc est rarement possible à faire sans K.
Si en plus tu as la règle de réduction associée à K, tu peux, si je ne m'abuse, largement simplifier la tactique "inversion" qui produirait des termes de preuves plus rapides à vérifier.