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).