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.

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

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.

If it's computable, boolean is preferable afaik.

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.

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

@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: Jun 18 2024 at 09:02 UTC