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

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)

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.

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

actually it works if I use `rewrite -[Y != X]asboolb.`

but it feels a bit awkward to specify the pattern to match

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.

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

?

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:

I'm on master

Last updated: Feb 08 2023 at 04:04 UTC