logic - 如何为 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具有 type 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).