## Stream: Coq users

### Topic: Convert SSReflect `!=` to `<>`?

#### Joshua Grosso (May 12 2021 at 20:49):

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.

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

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

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

move/eqP: H will transform your hyp

ut

but

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

let me just check the code i send works

#### Pierre Jouvelot (May 12 2021 at 21:03):

One solution would be to use contraposition, as in

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

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:03):

`rewrite (introF eqP H).` does the trick

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:04):

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

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:05):

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

#### Kazuhiko Sakaguchi (May 12 2021 at 21:05):

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

#### Emilio Jesús Gallego Arias (May 12 2021 at 21:06):

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 (May 12 2021 at 21:11):

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

#### Enrico Tassi (May 12 2021 at 21:43):

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

#### Joshua Grosso (May 12 2021 at 21:45):

Enrico Tassi said:

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

Good to know, I'll do that!

#### Joshua Grosso (May 13 2021 at 21:06):

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

#### Emilio Jesús Gallego Arias (May 14 2021 at 13:42):

@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