Как использовать приложение для извлечения импликации в Coq

Я проиллюстрирую это на примере.

H : R -> P -> Q

H0 : R

Подцель:

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

поэтому мой вопрос в том, как мне извлечь (P-> Q). У меня уже есть R, но когда я «применяю H в H0», он оценивает все и дает мне Q.


logic coq proof coq-tactic
person some1fromhell    schedule 08.02.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете сделать любое из:

specialize (H H0).

заменить H на H: P -> Q, или:

pose proof (H H0) as H1

представить H1: P -> Q

Вы также можете пойти вперед:

right. exact (H H0).
person Ptival    schedule 08.02.2016