0

我正在尝试研究一些基础逻辑的东西，主要来自《使用 Z：规范、改进、证明》一书，但也试图了解更多关于 Coq 的信息。上面提到的《使用 Z》一书中的第一个证明之一是逻辑或是可交换的， P \/ Q => Q \/ P. 这本书使用自然演绎树表示法，所以假设 P，然后引入 Q 或 P，或者假设 Q，然后引入 Q 或 P，我已经将它翻译成 Coq，无论你如何称呼标准库，如下所示：

Theorem disj_comm : forall P Q : Prop, P \/ Q -> Q \/ P.
Proof.
  intros P Q H.
  destruct H. right. apply H.
  left. apply H.
Qed.

你在这里看到类似的东西。无论如何，试图把它翻译成 SSReflect，我有点卡住了：

Theorem disj_comm' : forall P Q : Prop, P \/ Q -> Q \/ P.
Proof.
  move => P Q H.
  case H.
  right. (* isn't there a better approach here? *)
Abort.

我查看了我找到的 SSReflect 参考资料，没有看到任何明显看起来像是在尝试替换leftand的内容right。在 SSReflect 中编码这个证明的正确方法是什么？

编辑：我现在使用 SSreflect 有以下证明：

(* And here's disj_comm in ssreflect *)
Theorem disj_comm' : forall P Q : Prop, P \/ Q -> Q \/ P.
Proof.
  move => P Q H.
  destruct H.
  right.
  by [].
  left.
  by [].
Qed.

感觉这个比较啰嗦。有没有更好的方法来用 SSreflect 做到这一点？

4

1 回答 1

2

我想说 SSReflect 中的惯用解决方案在战术和句法层面上看起来都像这样：

From Coq Require Import ssreflect.

Lemma disj_comm P Q : P \/ Q -> Q \/ P.
Proof. by case; [right | left]. Qed.
于 2019-12-11T23:21:11.263 回答