Stream: Coq users

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

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.

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.

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.

Julien Puydt (Oct 19 2022 at 07:59):

If it's computable, boolean is preferable afaik.

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.

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 :)

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:

• when P is in the hypothesis, I like it to be in propositional form, in your case A = B, as propositions are _easy_ to consume.
• when P is in the goals, I like it to be in _computable_ form, as propositions are usually _hard_ to consume, but computations are _easy_ to check.

Last updated: Oct 13 2024 at 01:02 UTC