证明OR与SSReflect是交换的

Question

我正在努力研究一些基本的逻辑知识，主要来自于使用Z:规范、精化、证明一书，但也试图了解更多关于Coq的知识。使用上面提到的Z的书中的第一个证明之一是逻辑-或者是可交换的，P \/ Q => Q \/ P。这本书使用了自然演绎树表示法，所以假设P，然后引入Q或P，或者假设Q或P，然后引入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参考资料，没有看到任何明显看起来它试图取代left和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来实现呢？

Answer 1

我会说，在SSReflect中，一个惯用的解决方案在策略和句法层面上都是这样的：

From Coq Require Import ssreflect.

Lemma disj_comm P Q : P \/ Q -> Q \/ P.
Proof. by case; [right | left]. Qed.