时间戳

首页 > 解决方案 > Coq中的析取三段论策略？

coq - Coq中的析取三段论策略？

问题描述

我正在学习命题逻辑和推理规则。析取三段论规则指出，如果我们的前提中有（P 或 Q），并且还有（不是 P）；然后我们可以到达Q。

我一生都无法弄清楚如何在 Coq 中做到这一点。假设我有：

H : A \/ B
H0 : ~ A
______________________________________(1/1)

我应该使用什么策略来达到

H1 : B.

另外，如果有人可以与我分享基本推理规则的 Coq 策略等价物，我会很高兴，比如 modus tollens 或 disjunctive Introduction 等。是否有我可以使用的插件？

标签： coqcoq-tactic

解决方案

Coq 没有内置这种策略，但幸运的是您可以定义自己的策略。请注意

destruct H as [H1 | H1]; [contradiction |].

H1 : B就像你问的那样，放在上下文中。所以你可以为这个组合策略创建一个别名：

Ltac disj_syllogism AorB notA B :=
  destruct AorB as [? | B]; [contradiction |].

现在我们可以很容易地模仿析取三段论规则，如下所示：

Section Foo.
Context (A B : Prop) (H : A \/ B) (H0 : ~ A).
Goal True.
  disj_syllogism H H0 H1.
End Foo.

让我展示一些自动化程度较低的方法：

Ltac disj_syllogism AorB notA B :=
  let A := fresh "A" in
  destruct AorB as [A | B]; [contradiction (notA A) |].

这种方法不要求 Coq 找到矛盾，它直接提供给contradiction策略（notA A术语）。或者我们可以在策略中使用一个明确的术语pose proof：

Ltac disj_syllogism AorB notA B :=
  pose proof (match AorB with
              | or_introl a => False_ind _ (notA a)
              | or_intror b => b
              end) as B.

我希望这有帮助。我不确定是否需要一些额外的解释——请随时要求澄清，我会更新我的答案。

推荐阅读