Janno (Feb 13 2024 at 11:22): Janno (Feb 13 2024 at 11:22):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)?
Pierre-Marie Pédrot (Feb 13 2024 at 13:26):Unfortunately this is a hard problem.
Pierre-Marie Pédrot (Feb 13 2024 at 13:27):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
Pierre-Marie Pédrot (Feb 13 2024 at 13:28):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.
Pierre-Marie Pédrot (Feb 13 2024 at 13:28):The only safe alternative is to store terms in a list, but this is inefficient.
Pierre-Marie Pédrot (Feb 13 2024 at 13:29):You could also have a partial indexing à la discrimination net, but this is lossy
Pierre-Marie Pédrot (Feb 13 2024 at 13:31):(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")
Janno (Feb 13 2024 at 13:40):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.
Pierre-Marie Pédrot (Feb 13 2024 at 13:43):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)
Pierre-Marie Pédrot (Feb 13 2024 at 13:44):anything that distinguishes structurally equivalent terms is breaking the invariants of the representation
Pierre-Marie Pédrot (Feb 13 2024 at 13:45):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
Michael Soegtrop (Feb 13 2024 at 14:29):@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.
Janno (Feb 13 2024 at 14:31):Just to be very specific: we only ever store Constr.t and I think those are valid without an evarmap, aren't they?
Pierre-Marie Pédrot (Feb 13 2024 at 14:36):@Michael Soegtrop the problem is that this is literally unsound w.r.t. all of the proof engine
Pierre-Marie Pédrot (Feb 13 2024 at 14:37):@Janno if you don't have evars in your terms you're fine
Janno (Feb 13 2024 at 14:44):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.
Pierre-Marie Pédrot (Feb 13 2024 at 14:45):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.
Pierre-Marie Pédrot (Feb 13 2024 at 14:47):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).
Pierre-Marie Pédrot (Feb 13 2024 at 14:48):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)
Pierre-Marie Pédrot (Feb 13 2024 at 14:48):so the spec of the resulting data structure is not really a set anymore
Pierre-Marie Pédrot (Feb 13 2024 at 14:51):(and you also have to store somewhere in the map the set of undefined evars at the time each term was stored)
Pierre-Marie Pédrot (Feb 13 2024 at 14:52):otherwise you cannot recognize that a term has been invalidated
Janno (Feb 13 2024 at 14:52):We actually want a miss when we lookup terms with evars that have been instantiated between the insertion and the lookup
Pierre-Marie Pédrot (Feb 13 2024 at 14:54):then you have to be extremely careful
Michael Soegtrop (Feb 13 2024 at 15:06):@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?
Michael Soegtrop (Feb 13 2024 at 15:09):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?
Pierre-Marie Pédrot (Feb 13 2024 at 15:09):Because all of EConstr primitives are stable by evar expansion, and thus Ltac2 also is
Pierre-Marie Pédrot (Feb 13 2024 at 15:10):there are unsafe primitives to break this invariant, but they are unsafe indeed
Michael Soegtrop (Feb 13 2024 at 15:10):I see, good point, thanks!
Michael Soegtrop (Feb 13 2024 at 15:11):And making Ltac2 not stable wrt. Evar expansion would make Ltac2 unsound?
Michael Soegtrop (Feb 13 2024 at 15:13):I wonder how Elpi does this ...
Michael Soegtrop (Feb 13 2024 at 15:14):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.
Michael Soegtrop (Feb 13 2024 at 15:15):@Enrico Tassi : can you shed some light on this question?
Pierre-Marie Pédrot (Feb 13 2024 at 15:20):It's not directly related to Ltac2, nor elpi, nor actually any proof language. It's a fundamental invariant of the proof API.
Gaëtan Gilbert (Feb 13 2024 at 15:24):Pierre-Marie Pédrot said:
Janno if you don't have evars in your terms you're fine
universes?
Gaëtan Gilbert (Feb 13 2024 at 15:27):maybe we could have a map which stores evar_map * econstr and equality is the progress equality (Evarutil.eq_constr_univs_test)
Michael Soegtrop (Feb 13 2024 at 15:27):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.
Enrico Tassi (Feb 13 2024 at 18:38):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
Michael Soegtrop (Feb 14 2024 at 08:48):@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).
Enrico Tassi (Feb 14 2024 at 09:27):There are two possibilities, for example:
my-pred (app[const "plus",X,Y]) via =>my-pred (app[const "plus",X,Y]) via coq.elpi.accumulateIn 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.
Michael Soegtrop (Feb 14 2024 at 10:46):@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.
Jason Gross (Mar 22 2024 at 16:27):@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