Disclaimer: I'm trying to use a small library built on mathcomp for some pretty simple stuff. But, I've never used mathcomp itself, so I understand that the answer to this question might just be "read the mathcomp book" (in which case, please let me know).

I have a hypothesis of the form `H: x <> y`

, and an `if`

-statement of the form `if x == y then foo else bar`

. I figure I can use `ifN_eq : x != y -> (if x == y then vT else vF) = vF`

, but that requires me to prove `(x != y) = false`

. Try as I might, I'm having trouble proving this, as simple as it seems.

Hi @Joshua Grosso , usually you can use rewrite directly with this term

move/eqP: H will transform your hyp

ut

but

let me just check the code i send works

One solution would be to use contraposition, as in

```
Lemma foo (x y : nat) : x <> y -> x != y.
Proof. by apply: contraPneq => ->. Qed.
```

`rewrite (introF eqP H).`

does the trick

For positive equalities you can actually use the coercion so `rewrite (eqP H)`

works directly, likely there is a way to make this work directly

Only caveat of course you need your types to be an eqtype

but they already are

`negPf`

would also be useful in this case, e.g., `move/eqP/negPf: H`

.

Pierre Jouvelot said:

One solution would be to use contraposition, as in

`Lemma foo (x y : nat) : x <> y -> x != y. Proof. by apply: contraPneq => ->. Qed.`

That one you can just use the view, so `by move/eqP`

will also work

Emilio Jesús Gallego Arias said:

For positive equalities you can actually use the coercion so

`rewrite (eqP H)`

works directly, likely there is a way to make this work directly

Tho in this case you'll do instead `rewrite H eqxx`

, `rewrite (eqP H)`

is for the other direction, from x == y to x = y

"read the mathcomp book" (in which case, please let me know).

Since you are already familiar with Coq you should be able to go through the first chapter *very* quickly...

Enrico Tassi said:

"read the mathcomp book" (in which case, please let me know).

Since you are already familiar with Coq you should be able to go through the first chapter

veryquickly...

Good to know, I'll do that!

As an update to my original problem, I'm finding `rwP : forall (P : Prop) (b : bool), reflect P b -> P <-> b`

very useful in conjunction with e.g. `orP`

.

@Joshua Grosso indeed, note that this lemma does require setoid rewriting tho as to interpret `<->`

properly in `rewrite`

Last updated: Jun 14 2024 at 18:01 UTC