The Coq mailing list

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

On Wed, 20 Jan 2021 14:45:40 -0500
Adam Chlipala <adamc AT csail.mit.edu> wrote:

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

I am working on some Coq reflection procedures and trying to stay
within Gallina as much as possible.

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