The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Wed, 20 Jan 2021 20:45:21 +0100
Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr> wrote:

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

Of course.  I appologize for not realizing that myself.  I guess such
a function is then only possible without any associated lemmas, which
would probably make it far less useful.

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

Oh - bright shiny link to useful paper! ;-)

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