# Natural deduction in Coq

I am trying to verify the proofs by natural deduction from Ryan and Huth based on the information in Natural deduction with coq proof assistant. Here is Example 1.13 and its proof.

Step 4 is conjunction introduction, presumably using apply conj but I can't get it to work.

Import Coq.Init.Logic.
Theorem Ex13 : forall p q r: Prop, (p /\ q -> r) -> (p -> (q-> r)).
Proof.
intro p.
intro q.

• There isn’t a one-to-one correspondence with tactics and proof steps in the proof you showed. Instead, look at the goal at each step, the rules you have, and think how they may help. Also think about the big ideas in the proof. Hint: you likely want to use intro 4 times to even get to the same starting point as the proof you showed. The proof you have isn’t quantifying over p q r. Also it starts with |- instead of an implication. Those 4 intros will get you to that point. Another hint: you can’t apply conj until you have a conjunction as your goal. Jun 14, 2023 at 19:18
• The simplest solution would be to use the assert or pose tactic to introduce p /\ q as a subgoal.
– Couchy
Jun 15, 2023 at 6:44

If you want to translate accurately the sequent notation and the original proof (without additionnal explicit intros), you may write your proof as follows:

Theorem Ex13 (p q r: Prop) (H: p /\ q -> r): p -> (q-> r).
Proof.
intro Hp.
intro Hq.
(* ... *)
Qed.


Or use the section mechanism.

Section ProofOfEx13.
Variables p q r : Prop.
Hypothesis H : p /\ q -> r.

Theorem Ex13: p -> q -> r.
Proof.
intros Hp Hq.
(* ... *)
Qed.
End ProofOfEx13.