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类型为 list P -> P -> Prop .这个想法是Deriv hs p表示 p在假设下是可证明的 hs .这意味着放弃自然演绎的原始希尔伯特式公式，其中假设是隐含的(检查例如 the Wikipedia article )。留在你给出的片段中，这可能会导致这样的事情(使用只有一个结论的序列):

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