CODEWITHSUNDEEP
coqproof
Martin Copes
Martin Copes

Reputation: 981

Coq calculational style biconditional chain

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.

Upvotes: 2

Views: 219

Answers (1)

Konstantin Weitz
Konstantin Weitz

Reputation: 6422

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.

Upvotes: 2

Related Questions