How to simulate an injection rule for implication in Coq?
I study natural inference and practice Coq.
Consider the 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 stick to the introduction rule for implication. I've tried this:
| intro_imp: forall p q, (Deriv p -> Deriv q) -> Deriv (Imp p q)
which clearly doesn't work because the inductive case appears in the negative position.
Introduction rule for implication:
[p]
.
.
q
-------
p ⊃ q
How would one model an injection rule for implication in Coq?
source to share
The as-is formulation of natural deduction is a little difficult to do directly in Coq, because the most natural formulation hides the premise. Thus, we cannot refer to the premise that we fulfill when introducing the implication.
I think the simplest solution is to make the hypotheses explicit in the judgment, i.e. Deriv
will be of type list P -> P -> Prop
. The idea is that which Deriv hs p
expresses what is p
provable under conditions hs
. This means abandoning the original Hilbert-style formulation of natural deduction, where the hypotheses are implicit (for example, the Wikipedia article ). Staying inside the snippet you gave it could lead to something like this (using a sequence with only one output):
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).
source to share