I was trying to implement a `ConstrMap`

(which we currently have a custom implementation of) using the `FSet`

/`FMap`

interface but I noticed that I do not have access to the evarmap anywhere so I cannot safely go from Ltac2's `constr`

, which is `EConstr.t`

, to `Constr.t`

. I think `Constr.t`

is the correct choice for a map but maybe that is not correct? Would it make sense to offer an extended version of the interface for maps that need access to the evarmap (or the goal's environment)?

Unfortunately this is a hard problem.

I've been pondering about this for a while, and I don't know of a reasonable notion of ConstrMap for terms that may contain evars

You need to have access to a comparison function for binary trees, but this function is inherently impure in presence of evars, so you wreak havoc in the invariants of the map.

The only safe alternative is to store terms in a list, but this is inefficient.

You could also have a partial indexing à la discrimination net, but this is lossy

(I was hoping that experts in separation logic could chime in and say something along the lines of "oh yes this is a well-known issue with a straightforward solution")

We've been using maps on `Constr.t`

with no issues whatsoever. We actually rely crucially on evars being considered "different" after they are instantiated. I suppose our use case is not the one you had in mind.

An EConstr doesn't make sense without an evar map, this is really a datastructure full of pointers (the evars) into a heap (the evarmap)

anything that distinguishes structurally equivalent terms is breaking the invariants of the representation

so as long as 1. you don't touch the evarmap after storing terms in the ConstrMap and 2. you only observe evars in a monotone way you should be fine

@Pierre-Marie Pédrot : I must say I wouldn't mind if the map equality would be such that evars are unique terms different from any other evar and different from any other term. In other words, an evar is only map-equal to itself. Sure this would have the effect that in the map equality is not equivalent to structural equality in Coq, but structural equality is anyway different from Coq's main concept of equality (Leibnitz). I expect that in most applications it simply doesn't matter. Worst case you treat two structurally equal terms separately, but you will anyway treat all Leibnitz equal but not structurally equal terms separately.

Just to be very specific: we only ever store `Constr.t`

and I think those are valid without an evarmap, aren't they?

@Michael Soegtrop the problem is that this is literally unsound w.r.t. all of the proof engine

@Janno if you don't have evars in your terms you're fine

I think evars have a globally valid identity (they are just taken from a global counter, right?) so I don't understand what the problem is with having them in the map. Again, it might really be down to our use case that this setup works for us but I would like to understand the limitations.

Undefined evars have indeed a unique id, so they're fine. What wreaks havoc is the fact that you can instantiate an evar, which morally invalidates any term stored in the map that mentions such an evar.

You have to take this into account when fetching a term. A way to make things sound is to ignore such terms in the map, and normalize input terms before checking they are in the map (but this is inefficient).

Ignoring the term must be performed cautiously, because it might be the case that you rely on the fact that some term is *not* there for the soundness of your algorithm (hence the monotonicity property I was mentioning above)

so the spec of the resulting data structure is not really a set anymore

(and you also have to store somewhere in the map the set of undefined evars at the time each term was stored)

otherwise you cannot recognize that a term has been invalidated

We actually want a miss when we lookup terms with evars that have been instantiated between the insertion and the lookup

then you have to be extremely careful

@Pierre-Marie Pédrot : I don't understand why this would be unsound. Why can't I assign arbitrary hash numbers to terms and put the terms into a table by these numbers? Why would Coq care if equal terms get different numbers in a table of terms?

I mean I can put arbitrary terms into a Ltac2 list in arbitrary order. I can also put terms into a list in random order (using some pseudo RNG). Why can't I use instead of random numbers some numbers which depend in some arbitrary way on the term?

Because all of EConstr primitives are stable by evar expansion, and thus Ltac2 also is

there are unsafe primitives to break this invariant, but they are unsafe indeed

I see, good point, thanks!

And making Ltac2 not stable wrt. Evar expansion would make Ltac2 unsound?

I wonder how Elpi does this ...

I haven't experimented that much with it as yet, but afaik one can index a predicate in an Elpi database by arbitrary Coq terms.

@Enrico Tassi : can you shed some light on this question?

It's not directly related to Ltac2, nor elpi, nor actually any proof language. It's a fundamental invariant of the proof API.

Pierre-Marie Pédrot said:

Janno if you don't have evars in your terms you're fine

universes?

maybe we could have a map which stores `evar_map * econstr`

and equality is the progress equality (Evarutil.eq_constr_univs_test)

Pierre-Marie Pédrot said:

It's not directly related to Ltac2, nor elpi, nor actually any proof language. It's a fundamental invariant of the proof API.

I see, makes sense. Thanks for the explanation - I always wondered what the problem with hashing terms is.

In elpi there is no magic, the maps work well on ground terms, not on open terms.

In ATP they have order relations which are stable by instantiation, but are not trivial to compute. Iirc you make a polynomial on the unif variables and their occurrences, and measure the " potential size"... But these are not total I'm afraid, so I don't know if the resulting search tree is well balanced

@Enrico Tassi : so what does happen if I add a predicate with an open term as argument to a database? Is this prevented in some way? PMP wrote above (if I got him right) that the proof API has to be stable over evar instantiation to be consistent (I guess in the sense that one can construct proofs which then don't type check - not in the sense that one can construct a proof of False which would type check).

There are two possibilities, for example:

- you add
`my-pred (app[const "plus",X,Y])`

via`=>`

- you add
`my-pred (app[const "plus",X,Y])`

via`coq.elpi.accumulate`

In the first case, there is no problem, if X or Y are assigned, everything works, but the rule dies with the program. Evar instantiation is part of the runtime of elpi, there is no way to forget one by mistake.

The problem with the order relation is that the relation may not be stable by instantiation, eg if `a < b`

is `Y < b`

? if `Y`

gets `a`

fine, but what if it gets `b`

? Typically you can only say that `Y`

and `b`

are not comparable, but you could say that `Y < Y + Y`

(using the term size as a measure). Maps/sets need a total order relation, at least the ones we usually think about.

In the second case accumulate complains, you have to accumulate `pi X\ pi Y\ my-pred (app[const "plus",X,Y])`

instead that means that the rule works for any `X`

and `Y`

.

About universes I don't recall exactly which kind of universes, but the idea is that if you accumulate `my-pred (sort (typ "univ33"))`

elpi automatically accumulates `pi U\ my-pred (sort (typ U))`

, the alternative would be to pre-process the rule into something like `pi U\ my-pred (sort (typ U)) :- relate-somehow U "univ33".`

but in that case it is the user that has to do the job, since the relation can be anything.

About consistency, yes, one could generate a silly term. The kernel is not affected by any mess done in the upper layers.

@Enrico Tassi : thanks for the detailed explanation, especially the hint that one can add temporary db entries which do contain evars using `=>`

and that this is properly handled - quite useful.

@Pierre-Marie Pédrot what about having a map of tuple-of-undefined-evars -> constr -> value, which can be configured at creation time to either drop terms whose evars become instantiated or to merge them in O(n) (or O(n log n))? Every lookup operation should check if any evar tuples have been defined in the meantime, and, if so, should normalize the map and warn the user that they should have normalized the map themselves to avoid bad asymptotics.

Last updated: Oct 12 2024 at 13:01 UTC