Coq расчетно стиль biconditional цепь

Question

Я пытаюсь доказать biconditional в 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.