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.

Example from Ryan and Huth 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)).
  intro p.
  intro q.
  • $\begingroup$ Your url is bad. $\endgroup$
    – Jason Rute
    Jun 14, 2023 at 19:07
  • 2
    $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Jun 14, 2023 at 19:18
  • 1
    $\begingroup$ The simplest solution would be to use the assert or pose tactic to introduce p /\ q as a subgoal. $\endgroup$
    – Couchy
    Jun 15, 2023 at 6:44

1 Answer 1


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).
  intro Hp.
  intro Hq.
  (* ... *)

Or use the section mechanism.

Section ProofOfEx13.
 Variables p q r : Prop. 
 Hypothesis H : p /\ q -> r.
 Theorem Ex13: p -> q -> r. 
    intros Hp Hq. 
    (* ... *)
End ProofOfEx13.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.