如何在Coq中对引入规则进行建模

Question

我正在学习自然演绎并练习Coq。

我们考虑一个公式：

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

现在我为可证明性添加一堆推理规则：

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
| ...

但我坚持引入规则的含义。我试过这个：

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

，

这显然不起作用，因为感应外壳出现在负位置。

含义的引入规则是：

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

如何模拟Coq中含义的引入规则？

Answer 1

按原样直接在Coq中制定自然演绎有点困难，因为最自然的公式可以隐藏前提。因此，在引入含义时，我们不能参考我们正在履行的前提。

我认为最简单的解决方案是在判断中明确假设，即 Deriv将具有类型 list P -> P -> Prop .这个想法是Deriv hs p表示p在假设hs下是可证明的。这意味着放弃原始的希尔伯特式的自然演绎公式，其中假设是隐含的（例如检查维基百科文章）。停留在你给出的片段中，这可能会导致这样的事情（使用只有一个结论的连续性）：

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).