Coq 中的析取三段论策略？

Question

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

我一辈子都想不出如何在 Coq 中做到这一点。假设我有：

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

我应该使用什么策略才能达到

H1 : B.

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

Answer 1

我想您可能对 Coq 的工作方式抱有错误的期望？证明这一点的一般方法本质上是关于不同可能性的真理-table：

Lemma it: forall a b, (a \/ b) /\ ~a -> b.
Proof.
  intuition.
  Show Proof.
Qed.

(fun (a b : Prop) (H : (a \/ b) /\ ~ a) =>
 and_ind
   (fun (H0 : a \/ b) (H1 : ~ a) =>
    or_ind (fun H2 : a => let H3 : False := H1 H2 in False_ind b H3)
      (fun H2 : b => H2) H0) H)

如果您查看生成的证明项，您会发现 Coq 本质上是将布尔值分解为构造函数。我们可以手动执行此操作并获得相同的证明项：

Lemma it: forall a b, (a \/ b) /\ ~a -> b.
Proof.
  intros a b H.
  induction H.
  induction H.
  contradict H. exact H0.
  exact H.
Qed.

而例如modus ponens 对应于 Coq 中的 apply，我认为这不是任何直接的 "built in"。

之后，您可以使用这个引理（我敢肯定在标准库中某处有相应的版本）通过apply推导出您的附加假设。

Answer 2

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.

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

Coq 中的析取三段论策略？

Disjunctive Syllogism tactic in Coq?

coq

coq-tactic