Agda : Fonction pour l'égalité propositionnelle

Question

J'ai travaillé sur les fondements du langage de programmation dans Agda, et je suis actuellement à "Decidable : Les booléens et les procédures de décision". Il semble que, au moins pour l'exemple donné en détail, une fonction pour décider si quelque chose est vrai est similaire en structure à un objet de preuve qui démontre pourquoi c'est vrai. Plus précisément, le type de preuve

data __ :     Set where
  zn :  {n : }  zero  n
  ss :  {m n : }  m  n  suc m  suc n

a la même structure que la fonction de décision

__ :     Bool
zero  n       =  true
suc m  zero   =  false
suc m  suc n  =  m  n

sauf que cette dernière a un cas supplémentaire car elle doit fonctionner lorsque la réponse est fausse alors que la première ne doit fonctionner que lorsque la réponse est vraie.

Mais cette similitude ne semble pas tenir dans le cas de l'égalité propositionnelle. La preuve qu'une valeur est égale à elle-même s'écrit refl pour n'importe quel type -- d'après ce que je comprends, le travail difficile est fait pour nous par le vérificateur de type qui réduit tout à la forme canonique pour nous. Cependant, d'après ce que je sais (corrigez-moi si je me trompe), une fonction

__ : {A : Set}  A  A  Bool

qui décide de l'égalité pour les valeurs d'un type arbitraire n'est pas définissable en Agda.

Ma question est double :

1. Comment les tests d'égalité sont-ils généralement mis en œuvre ? Une fonction distincte est-elle définie pour chaque type de données ?
2. En particulier, existe-t-il un moyen de définir un test d'égalité entre les fonctions ? Disons que je veux définir une fonction qui prend comme argument un opérateur binaire _op_ : et retourne 42 si _op_ _+_ y 3 op 4 autrement. Cela semble nécessiter un moyen de tester l'égalité des fonctions, mais je n'arrive pas à trouver comment le faire. Une telle chose est-elle possible ?

En vérifiant la bibliothèque standard, je remarque que le test d'égalité pour est défini comme suit

_==_ : Nat  Nat  Bool
zero  == zero  = true
suc n == suc m = n == m
_     == _     = false

ce qui suggère que la réponse à ma première question est qu'une fonction d'égalité distincte est effectivement définie pour chaque type de données, comme je le pensais. Je n'ai rien trouvé qui suggère une réponse à ma deuxième question.

Answer 1

Dans le chapitre Isomorphisme dans le livre PLFA, l'égalité des fonctions est postulée via l'extensionnalité : Deux fonctions peuvent être considérées comme égales, si elles produisent le même résultat pour toutes les entrées. En utilisant l'extensionnalité, pour prouver l'égalité de deux fonctions (ou non), il suffit d'invoquer l'un des éléments suivants pour obtenir le résultat souhaité :

open import Data.Nat.Base using (; _+_)
open import Relation.Binary.PropositionalEquality using (__; __)
open import Data.Sum using (__; inj; inj)

foo : (op :     )  {(op  _+_)  (op  _+_)}  
foo _op_ {inj  eq} = 42
foo _op_ {inj neq} = 3 op 4

-- Test call with +
foo+ : foo _+_ {inj refl}  42
foo+ = refl

Donc fonction foo prend un tel opérateur binaire en entrée ainsi qu'une preuve d'égalité avec _+_ ou l'inégalité à _+_ . J'ai fait de la preuve un argument implicite ici afin qu'Agda puisse être capable de déduire une valeur par lui-même. Cependant, cela n'a pas fonctionné quand j'ai essayé avec foo+ ci-dessus.

Je ne pense pas qu'il soit possible d'écrire cette fonction sans prendre les preuves en paramètre car alors les preuves devraient être calculées dans la fonction elle-même, probablement pendant l'exécution, ce qui est difficilement automatisable.

J'espère que cela vous aidera. :)