(A -> B) /\ (B -> C) -> (A -> C) in Coq?

Question

I am learning Coq via the book software foundations, and have trouble proving the following lemma (which I require to prove other theorems.)

Lemma if_trans : 
  forall (P Q R: Prop),
    (P -> Q) /\ (Q -> R) -> (P ->R).
Proof.
  intros P Q R [E1 E2]. 
Admitted.

This is where I get stuck. I can't destruct on propositions, and I although I can apply E2 in E1, it generates two subgoals (I don't understand why), and the second subgoal is logically incorrect to prove. Please help. Also I know only the following tactics:

simpl , reflexivity, symmetry, destruct, induction, apply, replace, .. in , exfalso, discriminate, injection, split, left , right, intros, unfold, assert, rewrite.

Q2: Another question on somewhat similar lines. I need to use the above proved lemma for proving other theorems. So suppose I have two hypothesis H1: P -> Q and H2: Q -> R and the goal is P -> R. How can I use the above lemma to prove the goal in this case i.e. how can I combine H1 and H2 into a single hypothesis H : (P ->Q ) /\ (Q -> R)?

Usually it is best to refrain from asking several questions at once. Anyway what do you expect apply E2 in E1 to do? I would suggest to do one more introduction to have some p : P and try to prove R from it instead. — Théo Winterhalter
'apply E2 in E1': I thought this should be invalid as if E2 has the form A -> B and E1 has the form A, then above tactic replaces E1 with B. But here above tactic doesn't have this form, it should have worked iff E1 had the form (Q -> R) -> (P->R). How do I introduce an element of P? — Kaind

Théo Winterhalter Théo Winterhalter · Accepted Answer · 2020-03-09T17:47:56

You're trying to prove the following:

Lemma if_trans :
  forall (P Q R : Prop),
    (P -> Q) /\ (Q -> R) -> (P -> R).

but you only introduce P, Q, R the proof of P -> Q and that of Q -> R so it leaves you to prove P -> R. In the same way you can use intro p to get p : P as an extra assumption and then prove R.

To summarise you have

P, Q, R : Prop
E1 : P -> Q
E2 : Q -> R
p : P
===============
R

after the tactic

intros P Q R [E1 E2] p.

(notice the extra p).

Perhaps then it will appear clearer how to prove it.

When you use apply E2 in E1 it basically sees that E1 proves Q under the assumption that P holds, so it applies E2 : Q -> R in it to obtain R and asks on the side that you provide evidence for P.

For your second question, if you apply your lemma, it will ask for (P -> Q) /\ (Q -> P) which you can prove with split and then assumption. You should not try to combine P -> Q and Q -> R into (P -> Q) /\ (Q -> P) though, but if really you must you can use pose proof (conj H1 H2) as H.

(A -> B) /\ (B -> C) -> (A -> C) in Coq?

1 Answers