How to model introduction rule for implication in Coq?

Question

I am learning natural deductions and practicing Coq.

We consider a formula:

Inductive P :=
| ...
| And: P -> P -> P
| Imp: P -> P -> P. (* implication *)

Now I add a bunch of inference rules for provability:

Inductive Deriv: P -> Prop :=
| ...
| intro_and: forall p q, Deriv p -> Deriv q -> Deriv (And p q)
| elim_and1: forall p q, Deriv (And p q) -> Deriv p
| elim_and2: forall p q, Deriv (And p q) -> Deriv q
| ...

But I am stuck with the introduction rule for implication. I tried this:

| intro_imp: forall p q, (Deriv p -> Deriv q) -> Deriv (Imp p q)

, which clearly does not work, because the inductive case appears in a negative position.

The introduction rule for implication is:

[p]
 .
 .
 q
-------
p ⊃ q

How would one model the introduction rule for implication in Coq?

Answer 1

Formulating natural deduction as-is is a little bit difficult to do directly in Coq, because the most natural formulation keeps the premises hidden. Thus, we can't refer to the premise we're discharging when introducing the implication.

I think the simplest solution is to make the hypotheses explicit in the judgement, i.e. Deriv would have the type list P -> P -> Prop. The idea is that Deriv hs p expresses that p is provable under hypotheses hs. This means abandoning the original Hilbert-style formulation of natural deduction, where hypotheses are implicit (check e.g. the Wikipedia article). Staying within the fragment that you gave, this could result in something like this (using a sequent with just one conclusion):

Inductive Deriv : list P -> P -> Prop :=
(* How to use a hypothesis *)
| premise_intro hs p : In p hs -> Deriv hs p

(* In most rules, we just maintain the list of hypotheses *)
| and_intro hs p1 p2 : Deriv hs p1 -> Deriv hs p2 -> Deriv hs (And p1 p2)
| and_elim1 hs p1 p2 : Deriv hs (And p1 p2) -> Deriv hs p1
| and_elim2 hs p1 p2 : Deriv hs (And p1 p2) -> Deriv hs p2
| imp_elim hs p1 p2 : Deriv hs (Imp p1 p2) -> Deriv hs p1 -> Deriv hs p2

(* When introducing an implication, we remove the hypothesis from our list *)
| imp_intro hs p1 p2 : Deriv (p1 :: hs) p2 -> Deriv hs (Imp p1 p2).