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 (`bool_ab`

and `eq_ab`

)

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)

Huh. Why?

`eqVneq`

simultaneously replaces `x == y`

and `y == x`

:

`Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y).`

Oh, cool!

Last updated: Jul 25 2024 at 15:02 UTC