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 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.