The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Actually, thinks are not so simple.

If there is a function eq: T -> T -> bool for a given type T such that
  eq x y = true   and    x = y

then, forall z such that z=x, we have eq x z = true.

Thus, such an "eq" cannot only accept pointers equals to "x", but it 
must also accept any "z" structurally equals to "x".

In other words, the pointer equality needs to be modelled as a kind of 
"non-deterministic" function, because it is more discriminating than Coq 
equality.

A way to encode such a "non-deterministic" function is to use a monad...

See Section 4.4 of this paper:
  https://hal.archives-ouvertes.fr/hal-02185883/document

Sorry, for unsolicited advertising ;-)

Regards,

S.

Le 20/01/2021 à 20:18, jonikelee AT gmail.com a écrit :
> Is there any fast "eq" predicate in Gallina?
>
> By fast, I mean that it tests references only - returning true iff the
> two arguments refer to the same reference.  Hence it is analogous to
> the Lisp "eq" predicate, whereas the standard equality in Gallina is
> analogous to Lisp "equal".
>
> One would also need the associated lemmas, such as
> eq x y = true -> x = y.
>
> Also, one would need to know about when two references might be eq.
> For instance, it is possible to create a highly wasteful functional
> language without any reference sharing (such that eq would be false in
> all non-reflexive cases), but hopefully Gallina is not that, and that
> the ways in which Gallina is not that can be described in a useful way.