The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 20/01/2021 20:45, Adam Chlipala 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.

As long as you only have an under-approximation in the sense that

forall x y, pointereq x y = true -> x = y

you should be safe, if you only care about soundness.

You'd have a very hard time with subject reduction though, and that
would be a big concern to me. I don't know how Lean 4 implements pointer
equality, but they already threw SR with the bathwater, so it is a
non-problem for them.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature