la référence n'a pas été trouvée dans l'environnement actuel

Question

Disclaimer: ceci est pour un devoir

Je suis un noob de coq, alors j'espère que ce n'est pas une question de répétition. J'ai/j'ai regardé this question, mais ma question semble toujours sans réponse.

j'ai les locaux suivants:

P \/ Q 
~Q 

je dois prouver:

P 

Mon code coq jusqu'à présent:

Section Q5. 

Variables Q : Prop. 
Goal P. 
Hypothesis premise1 : P \/ Q. 
Hypothesis premise2 : ~Q. 

Je reçois l'erreur suivante lorsque je tente pour exécuter la ligne Goal P.:

Error: The reference P was not found in the current environment.

Ce sont les solutions que j'ai pu venir avec:

1. Remplacer Variables Q : Prop. avec Variables P Q : Prop.. Le problème avec ceci est que P sera supposé comme une prémisse, ce qu'il n'est pas
2. Ajouter Variables P. avant la déclaration d'objectif. Cela entraîne une erreur de syntaxe.

Ai-je raté quelque chose? Je ne semble pas être capable de comprendre cela.

Answer 1

La bonne solution est 1, et le problème que vous attendez est faux.

Lorsque vous écrivez:

Variable P: Prop. 

Vous n'êtes pas en supposant que P est habité (ou, que « P détient »), mais seulement qu'il existe une proposition nommée P, une « déclaration » dont la validité est pas considéré ici.

Ceci est très différent de l'écriture:

Variable p: P. 

Ce qui suppose qu'il existe une preuve « p » que le type « P » est habité (si P est de type Prop, p est une preuve de la proposition P), et suppose donc que P est vrai.

---

En outre, la raison pour laquelle:

Variables P. 

résultats dans une erreur de syntaxe est que vous devez fournir un type pour chaque variable introduite (Coq ne peut pas le comprendre comme par magie quand il n'y a pas informations menant au moteur d'inférence de type).

---

Il est parfaitement bien pour commencer votre script:

Section Q5. 
Variables P Q : Prop. 
Hypothesis premise1 : P \/ Q. 
Hypothesis premise2 : ~Q. 
Goal P.