（（A-> B）/ \（B-> C）->（A-> C）in Coq？

Question

我正在通过书籍软件基础学习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，但它会生成两个子目标（我不明白为什么），而第二个子目标在逻辑上是不正确的。请帮忙。我也只知道以下策略：

简单，自反性，对称性，破坏，归纳，应用，替换，..中，扩展，区分，注入，拆分，左，右，前奏，展开，断言，重写。

Q2：另一个类似问题的问题。我需要使用以上证明的引理来证明其他定理。因此，假设我有两个假设H1: P -> Q和H2: Q -> R，目标是P -> R。在这种情况下，如何使用上述引理来证明目标，即如何将H1和H2合并为单个假设H : (P ->Q ) /\ (Q -> R)？

Answer 1

您正在尝试证明以下内容：