The Coq mailing list

[Mario Carneiro <di.gama AT gmail.com>]

The lean implementation uses quotient types. The version in the paper has the form

forall A B, subsingleton B -> forall x y : A, (option (x = y) -> B) -> B

or equivalently

forall x y, trunc (option (x = y))

where trunc is the quotient by the always-true relation. The "reference implementation" of the function, available to the logic, evaluates the inner function on none, while the actual implementation calls the function with "some <>" if x and y are pointer-equal. The restriction to subsingletons (in the CPS version) or using the propositional truncation ensures that there is no difference between the "none" and "some <>" cases in the logic itself - the two cases can take more or less time but must compute the same answer.

This does not respect definitional equality, in the sense that the computation is not following the same path as the definitional reduction. In most cases these constants have in fact been defined as constants, which block any definitional reduction (but must still be proven to exist via the "reference implementation" to ensure soundness).

Mario Carneiro

On Wed, Jan 20, 2021 at 3:20 PM Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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