Ssreflect Users Discussion List

[bertot <>]

On 15/4/14 3:30 PM, Marcus Ramos wrote:

Hi,

In library "ssrnat" I find the definition:
Lemma addn_eq0 : forall m n, (m + n == 0) = (m == 0) && (n == 0).

I can´t, however, figure out the difference between "==" and "=", nor find "==" in the Coq documents. Is this something specific to SSReflect?
Is there an equivalent "forall m n: nat, (m + n) = 0 -> (m = 0) /\ (n = 0)" anywhere?
I also couldn´t find a (nat) lemma like "forall n: nat, (n = 0) -> n <= 0". Does it exist anywhere?
Thanks in advance, Marcus.

The notation "==" is defined in eqtype.v ; it corresponds to a boolean equality test function (an algorithm, usually specific to a given type, that can decide whether to ground values are equal), while "=" corresponds to a proposition.

eqtype contains general lemmas about all types where boolean equality test functions exist.  There is a line in ssrnat.v that expresses that the type nat is one of these types.

Canonical nat_eqMixin := EqMixin eqnP.
Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.

I hope this helps.

Yves