(A -> B) / \ (B -> C) -> (A -> C) в Coq? - PullRequest
Новая
       9

(A -> B) / \ (B -> C) -> (A -> C) в Coq?

0 голосов
/ 09 марта 2020

Я изучаю Coq через основы программного обеспечения книги, и мне трудно доказать следующую лемму (которая мне нужна для доказательства других теорем). 

Lemma if_trans : 
  forall (P Q R: Prop),
    (P -> Q) /\ (Q -> R) -> (P ->R).
Proof.
  intros P Q R [E1 E2]. 
Admitted.

Вот где я застреваю. Я не могу разрушать предложения, и хотя я могу apply E2 in E1, он генерирует две подзадачи (я не понимаю почему), а вторая подзадача логически неверна для доказательства. Пожалуйста помоги. Также я знаю только следующую тактику:

упрощение, рефлексивность, симметрия, разрушение, индукция, применение, замена, .. in, exfalso, дискриминация, инъекция, разделение, влево, вправо, вступления, развертывание, утверждение, переписать.

Q2: Еще один вопрос в несколько похожих строк. Мне нужно использовать доказанную выше лемму для доказательства других теорем. Итак, предположим, у меня есть две гипотезы H1: P -> Q и H2: Q -> R, а цель - P -> R. Как я могу использовать приведенную выше лемму для доказательства цели в этом случае, т.е. как я могу объединить H1 и H2 в одну гипотезу H : (P ->Q ) /\ (Q -> R)?

1 Ответ

1 голос
/ 09 марта 2020

Вы пытаетесь доказать следующее: 

Lemma if_trans :
  forall (P Q R : Prop),
    (P -> Q) /\ (Q -> R) -> (P -> R).

, но вы вводите P, Q, R доказательство P -> Q и Q -> R, поэтому вам остается доказать P -> R. Таким же образом вы можете использовать intro p, чтобы получить p : P в качестве дополнительного предположения, а затем доказать R.

Для суммирования у вас есть 

P, Q, R : Prop
E1 : P -> Q
E2 : Q -> R
p : P
===============
R

после такти c

intros P Q R [E1 E2] p.

(обратите внимание на дополнительные p).

Возможно, тогда будет понятнее, как это доказать.

Когда вы используете apply E2 in E1 он в основном видит, что E1 доказывает Q при условии, что P имеет место, поэтому он применяет E2 : Q -> R в нем для получения R и спрашивает на стороне, что вы предоставляете доказательства для P.

На ваш второй вопрос, если вы примените свою лемму, он попросит (P -> Q) /\ (Q -> P), которую вы можете доказать с помощью split, а затем assumption. Вы не должны пытаться объединить P -> Q и Q -> R в (P -> Q) /\ (Q -> P), но если вам действительно нужно, вы можете использовать pose proof (conj H1 H2) as H.

...