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)

Ana de Almeida Borges (Nov 07 2022 at 20:15):

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: Feb 08 2023 at 04:04 UTC