The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I've seen some recent work in Lean along these lines, I believe, but I, for one, am glad not to see that kind of feature complicating the trusted core of Coq!  To start with, taken literally, your proposal sounds logically inconsistent, since there could be two definitionally equal values that trigger different behavior for the "eq" operation.

Also, if you really want good performance, why not verify a program in some deeply embedded language?  I've found performance predictability to be quite treacherous within normalization of Gallina terms.  I'd much rather generate a C program with a proof that it computes the answer I want.  Many potential target languages allow your proposed optimization to be proved from first principles.

On 1/20/21 2:18 PM, jonikelee AT gmail.com wrote:

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