勒柯克的測算風格的雙條件鏈

Question

我試圖證明勒柯克一個雙條件：

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.