The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On Wed, Jan 20, 2021 at 10:18 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

It occurs to me that I don't really need "eq x y = true -> x = y", but
instead can get by with "eq x y = false -> x <> y"

This is just as inconsistent.  If x and y are (structurally) equal but physically unequal, you get false = false -> ~True.

"eq" cannot be a Coq function because it does not map equals to equals.

One possibility is to use the function "lambda x y a b. if eq x y then a else b" with a type that forces "a" and "b" to be equal if "x" and "y" are equal (and thus both "then" and "else" branches could be taken).  Something like:

Parameter eq: forall {T U: Type} (x y: T) (a b: U), (x = y -> a = b) -> U.

Axiom eq_same: forall {T U: Type} (x: T) (a b: U) P, eq x x a b P = a.
Axiom eq_different: forall {T U: Type} (x y: T) (a b: U) P, x <> y -> eq x y a b P = b.

- Xavier Leroy

 

(another good reason
not to be classical!), because the vast majority of the comparisons I'd
be doing will end up being false.  And I can get that with UIDs, or even
just mostly-unqiue IDs.  I would then embed such a UID in each
structure I need to compare quickly.

That should be somewhat attainable once Ltac2 has a more complete set
of mutable structure capabilities - so that an Ltac2 function can create
such an almost-UID.  That would at least allow me to generate UIDs at
type checking time, which again might be sufficient for my purposes,
although barely.

Of course, it would be even better if Gallina had an opaque type to use
for these UIDs that implemented a very fast equality check - but
integers would work for now.  And even better still if Gallina could
generate such UIDs itself without violating the logic.

On Wed, 20 Jan 2021 21:22:38 +0100
Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

> On 20/01/2021 21:17, jonikelee AT gmail.com wrote:
> > I am working on some Coq reflection procedures and trying to stay
> > within Gallina as much as possible. 
>
> Why don't you implement your own heap inside Coq then, using some form
> of state monad? It's going to be overly cumbersome but at least you'd
> get pointer equality from first principles.
>
> PMP
>