Stream: Coq users

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


view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

move/eqP: H will transform your hyp

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

ut

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

but

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:01):

let me just check the code i send works

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:03):

rewrite (introF eqP H). does the trick

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 21:05):

but they already are

view this post on Zulip Kazuhiko Sakaguchi (May 12 2021 at 21:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 12 2021 at 21:43):

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

view this post on Zulip Joshua Grosso (May 12 2021 at 21:45):

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

Good to know, I'll do that!

view this post on Zulip 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.

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC