Comment utiliser apply pour "extraire" une implication dans Coq

Question

Je vais illustrer en utilisant un exemple.

H : R -> P -> Q 

H0 : R 

subgoal:

(Q -> P) \/(P -> Q) 

donc ma question est de savoir comment puis-je en extraire (P-> Q). Je R déjà, mais quand je fais 'appliquer H dans H0', il évalue tout et me donne Q.

Answer 1

Vous pouvez effectuer:

specialize (H H0). 

pour remplacer H avec H: P -> Q, ou:

pose proof (H H0) as H1 

à introduire H1: P -> Q

Vous pouvez également aller de l'avant:

right. exact (H H0).