Preuve qui fait référence à la conclusion d'une preuve précédente en Coq

en supposant que je suis la preuve d'une relation d'équivalence:Preuve qui fait référence à la conclusion d'une preuve précédente en Coq

P <-> Q

et je suis parvenu à la preuve de la part d'implication:

P -> Q

mais lorsque je tente pour preuve l'autre sens, c'est

Q -> P

il se trouve que je devrai utiliser P -> Q. Puis-je demander quelle est la stratégie pour organiser la preuve qui nécessite une conclusion immédiate fait quelques lignes ci-dessus?

Source

2017-03-20 HuStmpHrrr

Voilà qui est intéressant ... Est-il possible pour vous de partager votre lemme? –

@AntonTrunov nvm. En fait, j'ai réalisé que je suis tombé dans un argument compliqué et j'ai trouvé un argument beaucoup plus facile pour passer à travers la preuve et il s'avère que ma pensée précédente était assez stupide. – HuStmpHrrr

C'est bon :) Mon train de pensée était comme ceci: supposons qu'on ait besoin d'un terme (appelons-le 'ptoq') de type' P -> Q' tout en prouvant l'autre sens, mais un usage non trivial de 'ptoq 'serait une application à un terme (' p') de type 'P' (qui correspond à la règle modus ponens), mais pour appliquer' ptoq' à 'p' il faut construire un tel' p', qui est le objectif global à ce stade de la preuve. De tout ce qui précède, nous n'avons pas besoin de 'ptoq' pour prouver l'autre direction. –

Vous pouvez commencer avec un assert avant de se séparer de l'équivalence P <-> Q:

Goal forall P Q, P <-> Q. 
Proof. 
intros P Q. 
assert (PimpliesQ : P -> Q). 
{ admit. (* your proof *) 
} 
split; [assumption|].

Source

2017-03-20 13:20:01 gallais

Preuve qui fait référence à la conclusion d'une preuve précédente en Coq

Répondre

Questions connexes