## Stream: math-comp users

### Topic: viewer <> as != in a goal ?

#### vlj (Oct 04 2020 at 10:53):

Hi,
I have the following goal: `(Y <> X /\ X `<=` Y) = (Y != X /\ X `<=` Y)` where Y and X are set T. Is it possible to prove it with a single tactic ? Currently I'm calling propeqE, splitting, and destructing the hypothesises in order to apply /eqP (eg `rewrite propeqE; split; by move => [] /eqP.`). This is because I don't know how to apply the /eqP view to either <> or != in the goal...

#### Paolo Giarrusso (Oct 04 2020 at 11:29):

Would “repeat f_equal” help (never tried with math-comp)? The other way would be to rewrite somehow with eqP, but I don’t know the right lemmas for that (if they even exist)

#### Christian Doczkal (Oct 04 2020 at 13:14):

The common thing to do when using `mathcomp` is to never introduce `_ <> _` for anything that has a decidable equality, at least when working without classical assumptions. Juddging from your use of `propeqE`, you are using the `analysis` library, which seems to be exporting the morphisms for setoid rewriting. Hence you can do `by rewrite propeqE (rwP eqP) (rwP negP).` Maybe @Cyril Cohen can comment on what's the best practice regarding boolean statements in the setting where `Prop` and `bool` are essentially the same.

#### vlj (Oct 04 2020 at 13:49):

It's not impossible that I misused some of the lemma in boolp, I wanted to transform `(Y != X) && `[< X `<=` Y >] = (X != Y /\ X `<=` Y)` into something with a `/\`, in boolp there is an `asbool_and` lemma but for some reason it doesn't want to apply on the initial goal, so I resorted to use asbool_neg which transform the inequality into a `[< X <> Y>]`

#### vlj (Oct 04 2020 at 13:51):

actually it works if I use `rewrite -[Y != X]asboolb.` but it feels a bit awkward to specify the pattern to match

#### Christian Doczkal (Oct 04 2020 at 14:29):

Hmm, `(Y != X) && `[< X `<=` Y >] = (X != Y /\ X `<=` Y)` is an equation between a boolean and a proposition and doesn't typecheck. And, looking at the lemmas in `boolp`, I'm surprised to not find something like

``````Lemma asboolEb (b : bool) : `[< b >] = b. Proof. by apply/asboolP/idP. Qed.
``````

I think you will need to wait for someone more familiar with this classical setting than me to comment on the best practices.

#### Reynald Affeldt (Oct 04 2020 at 14:36):

@Christian Doczkal Isn't it the lemma `asboolb`?

#### Christian Doczkal (Oct 04 2020 at 14:41):

Well, I installed the latest stable (0.3.2), because the question from @vlj had made me curious, and that version doesn't have `asboolb`. :shrug:

#### vlj (Oct 04 2020 at 15:53):

I'm on master

Last updated: Feb 08 2023 at 04:04 UTC