The question is about the mathcomp idiomaic way to destruct something as follows:
Goal forall (T: eqType) (a b: T), a = b \/ a <> b. Proof. move => T a b. move eq_ab : (a == b) => bool_ab. move : bool_ab eq_ab =>  /eqP => [->|Hneq_ab]. by left. by right. Qed
The real case analysis of (a==b) is not done in a single step but rather two
move eq_ab : (a == b) => bool_ab. move : bool_ab eq_ab =>  /eqP => [->|Hneq_ab].
Which takes longer time trying to understand what is going on as opposed to
destruct (a == b). But destruct does not give me
a = b and
a <> b
So what will be the way to achieve this kind of functionality without spitting the logic on two lines and having to do all the unneccsary bookkeeping (
You're looking for
case: eqP. In this case, since
a == b doesn't appear in the context you have to help it by including the arguments:
case: (@eqP _ a b).
perfect, I think I will end up at some point putting all those mini tricks in a cheat sheet.
walker has marked this topic as resolved.
I recommend using
case: eqVneq instead (in most cases)
eqVneq simultaneously replaces
x == y and
y == x:
Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y).
Last updated: Feb 08 2023 at 04:04 UTC