Как применить предложение вида P-> Q-> R к двум гипотезам P и Q одновременно в Coq?

Question

Я пытался доказать forall P Q R : Prop, P -> Q -> (P -> Q -> R) -> R. Мое доказательство заключается в следующем.

Goal forall P Q R : Prop, P -> Q -> (P -> Q -> R) -> R.
Proof.
  intros P Q R H1 H2 H3.
  apply H3 in H1.
  exact H1.
  exact H2.
Qed.

Когда примените H3 в H1, появятся две цели. Тем не менее, я хочу получить R более прямо как apply H3 in H1 and H2. Но я не мог найти такой способ. Как мне этого добиться?

Я уже знаю, что следующее тоже хорошо. Но это не то, что я хочу. Я не хочу увеличивать цели.

Goal forall P Q R : Prop, P -> Q -> (P -> Q -> R) -> R.
Proof.
  intros P Q R H1 H2 H3.
  apply H3.
  exact H1.
  exact H2.
Qed.

Answer 1

Вы можете непосредственно применить H1 и H2 к H3, не используя тактику apply.

Ваш H3 относится к типу P -> Q -> R (функция, которая принимает доказательстваP и Q и возвращает доказательство R). Итак, выражение H3 H1 H2 имеет тип R.

. Таким образом, вы можете упростить ваше доказательство до следующего:

Goal forall P Q R : Prop, P -> Q -> (P -> Q -> R) -> R.
Proof.
  intros P Q R H1 H2 H3.
  apply (H3 H1 H2).
Qed.

Фактически, ваше доказательство точно такое же, какодин выше, потому что вся тактика apply заключается в применении функции к аргументу.