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

Question

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

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

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

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

H1 : B.

另外，如果有人能与我分享基本推理规则的 Coq 策略等价物，例如模式收费或分离式介绍等，我会很高兴。是否有我可以使用的插件？

Answer 1

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.

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