viewer <> as != in a goal ? · math-comp users

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 (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:

Stream: math-comp users

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

vlj (Oct 04 2020 at 10:53):