Coq 计算式双条件链

Question

我试图在 Coq 中证明双条件：

P <-> Q

我写下了一个具有这种结构的证明：

P 
<-> 
S 
<->
T
<->
Q
thus: P <-> Q

如何在 Coq 中模仿这种计算证明结构？

提前谢谢你。

Answer 1

这就是您在 Coq 中的表达方式。 intuition 是一种擅长解决像您这样的逻辑目标的策略。

Lemma lma P S T Q : (P <-> S) -> (S <-> T) -> (T <-> Q) -> (P <-> Q).
  intuition.
Qed.

如果您更喜欢明确地编写它，请执行：

Lemma lma P S T Q : (P <-> S) -> (S <-> T) -> (T <-> Q) -> (P <-> Q).
  intros [ps sp] [st ts] [tq qt].
  constructor.
  - intro p.
    apply tq.
    apply st.
    apply ps.
    apply p.
  - intro q.
    apply sp.
    apply ts.
    apply qt.
    apply q.
Qed.

Coq 计算式双条件链

Coq calculational style biconditional chain

coq

proof