Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Florent,

this "always" rule is in fact always valid for "`<>` vs `!=`": we prefer 
to write `_ != _` and we never use `<>` on an `eqType`. Their are some 
exceptions where we write `(_ == _) = false` as a conclusion, to make 
the pattern more general to rewrite with...

However, for "`=` vs `==`" it is actually more subtle: generally, `==` 
is used only when necessary, e.g. in the body of a boolean predicate 
(e.g. `[pred x | f x == y]` of `[forall x, exists y, f x == y]`). 
Otherwise we prefer `=` to make the lemma ready to rewrite with.

Best,
--
Cyril

On 01/08/2019 10:45, Florent Hivert wrote:
>        Dear all,
>
> Reading the MathComp book I was surprised reading at the bottom of page 125
> the following sentence:
>
>     Whenever we want to state equality between two expressions, if they live
>     in an eqType, always use ==.
>
> It seems to suggest that lemmas such as
>
>     Lemma subSS n m : m.+1 - n.+1 = m - n.
>
> should be written as
>
>     Lemma subSS n m : m.+1 - n.+1 == m - n.
>
> which doesn't look very practical. Is it a mistake or am I missing something ?
>
> Cheers,
>
> Florent