Proving OR is commutative with SSReflect

Question

I'm trying to work through some foundational logic stuff, mainly from the book Using Z: Specification, Refinement, Proof but also trying to learn more about Coq. One of the first proofs in the book Using Z mentioned above is that logical-or is commutative, P \/ Q => Q \/ P. The book uses natural deduction tree notation, so it suffices to assume P, then introduce Q or P, or else assume Q and then introduce Q or P. I have translated this to Coq with whatever you'd call the standard library like so:

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.

You see something similar here. Anyway, trying to translate this to SSReflect, I got kind of stuck:

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.

I looked through the SSReflect reference I found and didn't see anything that obviously looked like it was trying to replace use of left and right. What's the right way to encode this proof in SSReflect?

Edit: I have the following proof now using 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.

I feel like this is rather wordy. Is there a better way to do this with SSreflect?

I feel like the ssreflect way would be to apply the proper constructor: apply or_introl. But there's no reason not to use left/right in such cases. — Ptival
@Ptival how would I discover or_introl while attempting the proof? (Actually, in trying to apply your advice, I still got stuck, so if you have time to give a more detailed answer, I would appreciate it!) — Daniel Lyons
left and right are idiomatic in SSReflect proofs, or_into(l/r) are not. — Anton Trunov
@AntonTrunov with the edit, do you find my new proof to be idiomatic of SSreflect? — Daniel Lyons
@DanielLyons To answer your question about finding the constructors: first you can use Locate "\/". which will tell you that it stands for "Logic.or". Then you can Print Logic.or. which will show you the definition, including the two constructors. — Ptival

Anton Trunov Anton Trunov · Accepted Answer · 2019-12-11T23:21:11

I would say an idiomatic solution in SSReflect would look both on tactic and syntactic level like so:

From Coq Require Import ssreflect.

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

Proving OR is commutative with SSReflect

1 Answers