Question technique : prédicats sur types inductifs en Coq
Par David Monniaux le lundi, janvier 16 2012, 18:24 - Théorie - Lien permanent
Lorsqu'en Coq, on a une propriété à définir sur un type inductif T, faut-il mieux définir une fonction T->Prop par point fixe, ou définir un prédicat inductif T->Prop? Le premier cas n'est évidemment pas applicable si la décision du cas à appliquer n'est pas (quasi) déterministe en fonction du constructeur de T rencontré à la racine. Le second cas oblige à utiliser des inversions, qui peuvent parfois poser problème.
Sylvain Boulmé me suggère de faire les deux en démontrant une équivalence... D'ailleurs, est-ce que ça marche bien, la réécriture Setoid par l'équivalence logique ? Je l'ai utilisée sur quelques exemples, mais y a-t-il des problèmes cachés ? Est-ce fondamentalement plus complexe ou piège que la réécriture par l'égalité de Leibniz ?
Commentaires
Si tu peux le faire par récurrence, c'est souvent mieux (ça évite tous les problèmes d'inversion un peu pénibles). Si tu dois en faire un inductif, essaie d'avoir l'argument en paramètre (définir Inductive blah (x:T) : Prop, plutôt que Inductive blah : T -> Prop). Quand ça marche, ça a généralement de meilleurs principes d'induction.
Et la (mal nommée) réécriture setoïde marche très bien avec l'équivalence logique. La réécriture setoïde a des pièges dans les coins que la réécriture avec l'égalité de Leibniz n'a pas, mais il y a peu de chance que ça arrive quand il s'agit de l'équivalence. De toute façon, il y a peu de chance que tu aies besoin des deux définitions (à moins qu'elle n'aient pas la même structure).