Stream: Coq users

Topic: When to use `==` and when to use `=` in ssreflect


view this post on Zulip walker (Oct 19 2022 at 07:50):

I am moving some code from normal coq to ssreflect. and I had a lemma that says:

Lemma close_open_rec: forall t1 t2 idx lvl,
    lvl  fv t1 -> t2 = open_rec t1 idx (fvar lvl) -> t1 = close_rec t2 lvl idx.

The content of the lemma is not that important but this is one of the cases where I was not sure if I should use == instead of =.

note that both open_rec and close_rec are functions.

In the current implementation I had to destruct an expression as follows:

case idx_eq_i: (idx == i).

and at some point I had the following:

i, idx: nat
idx_eq_i: (idx == i) = true
=====================
idx = i

I couldn't find anything that link the two statements together in eqtype the closest thing I could find is

  forall [I : eqType] [T_ : I -> eqType] [u v : {i : I & T_ i}],
  u == v -> ssrfun.tag u = ssrfun.tag v

But I dont use this ssrfun.tag thing so it does not look relevant.

view this post on Zulip Julien Puydt (Oct 19 2022 at 07:56):

@walker Well, if you try:

From mathcomp Require Import all_ssreflect.

Check (_ == _).
Check (_ = _).

then you'll see one is bool and the other Prop, so basically it depends if you're considering a computable equality or a logical one.

view this post on Zulip walker (Oct 19 2022 at 07:58):

As per my understanding, all of _ == _ i s coerced to is_true(_ == _) so my question is more about when is it preferable rather than when can I.

view this post on Zulip Julien Puydt (Oct 19 2022 at 07:59):

If it's computable, boolean is preferable afaik.

view this post on Zulip walker (Oct 19 2022 at 07:59):

It is not clear to me when should I consider computable equality (other than the basic example of numbers equality.

Also I don't know how to convert between the two notions.

view this post on Zulip Meven Lennon-Bertrand (Oct 19 2022 at 09:43):

If you can equip your type T with an eqType structure (ie a boolean function e : T -> T -> bool and a proof that forall t t', reflect (t = t') (e t t'), you can always go back and forth between the two notions using the eqP view. Here is a very simple example:

From mathcomp Require Import all_ssreflect.

Hypothesis (T : eqType).

Goal forall (P : T -> Type) (t t' : T), t == t' -> P t -> P t'.
Proof.
  move => ? ? ? /eqP -> HP.
  by apply: HP.
Qed.

Now, as to whether you should use one or the other I would say depends on how you want to use the lemma: typically, if you want to rewrite with it, then stating it with = is wise, because you cannot do rewrite lem if lem ends with t == t'. Conversely, if you usually want small-step computation steps with it (especially in hypothesis), then maybe using the computational version is smarter. But in the end the whole point of mathcomp is to make it easy to go back and forth between both representations, so making one choice or the other should not be too crucial :)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 15:41):

@walker the rule of thumb for me when I'm faced predicates that are "reflectable" is as follows:


Last updated: Feb 01 2023 at 13:03 UTC