Coq calculational style biconditional chain

Question

I am trying to prove a biconditional in Coq:

P <-> Q

And I wrote down a proof that has this structure:

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

How can I mimic this calculational proof structure in Coq?

Thank you in advance.

Answer 1

This is how you can express this in Coq. intuition is a tactic that is good at solving logical goals like yours.

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

If you prefer writing it explicitly, do:

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.