Variable
Contexte
On peut représenter une formule "pour tout" par
- "forAll f" , sans variable, où f est une fonction. Dans ce cas pour l'application, on déduira f +f x pour n'importe quelle formule x.
- "forAll x ;; f", où x est une variable pouvant être utilisée par f. Dans ce cas pour l'application, on déduira f où l'on aura remplacé x par une formule quelconque.
Question
Quelle est la meilleur manière de représenter une formule "pour tout" ?
Étude
Critère "isClean"
Ce critère ne fonctionne pas avec "distribute" (sauf s'il n'y a plus de "imply). Par contre on peut l'utiliser avec les notations de fonction. Donc pour la première forme, ça ne pose pas de problème si on passe par les notations de fonction.
Donc pour la première forme il faut définir avant la notation pour les fonctions.
En tant que "mot clé"
Pour la deuxième forme on n'a plus vraiement un mot clé, les deux arguments sont spéciaux, la formule aussi car ellle est dans une autre mathématique (celle avec la variable).
La déduction d'ajout
Pour la première forme il faut en argument un nom de variable x, la formule clea f et une preuve p de f x.
La déduction d'application
Pour la première forme on déduit f a pour n'importe quel a, pour la deuxième, il faut faire un remplacement dans f.
La recherche de la déduction d'ajout
Cela devient plus compliqué du fait qu'il faut des théorèmes plus complexes.
Réponse
Il faut une version de "forAll" sans variable. La notation de fonction permet de rassembler sous une forme simple la gestion des formules à variable. On la notera ∀ x | f car le symbole ";" a le même sens que la virgule en lazy, de plus on pourra avoir des syntaxes complexes pour assigner des variables de sous-structure (comme pour les arguments de fonctions).