## Stream: math-comp users

### Topic: ✔ How to destruct a non existent mathcomp equality.

#### walker (Nov 05 2022 at 15:21):

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`)

#### Ana de Almeida Borges (Nov 05 2022 at 15:32):

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

#### walker (Nov 05 2022 at 15:34):

perfect, I think I will end up at some point putting all those mini tricks in a cheat sheet.

#### Notification Bot (Nov 05 2022 at 15:34):

walker has marked this topic as resolved.

#### Cyril Cohen (Nov 07 2022 at 17:51):

I recommend using `case: eqVneq` instead (in most cases)

Huh. Why?

#### Cyril Cohen (Nov 07 2022 at 21:18):

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

#### Ana de Almeida Borges (Nov 07 2022 at 21:27):

Oh, cool!

Last updated: Jul 25 2024 at 15:02 UTC