Paolo Giarrusso (Jul 22 2022 at 12:01): Paolo Giarrusso (Jul 22 2022 at 12:01):Does vm_compute not work correctly under coq.ltac.call? The result mostly works, but the output proof terms contains a normal cast rather than a vm_compute cast... relevant snippet:
std.assert-ok! (coq.elaborate-skeleton TyFinite _ ETyFinite) "[mk-finite] [TyFinite]",
std.assert-ok! (coq.typecheck {{ lp:BoFinite : lp:ETyFinite }} _) "typechecking [Finite] failed",
coq.ltac.collect-goals BoFinite [SealedGoal] [],
coq.ltac.open (coq.ltac.call "solve_finite" [trm ECtorList]) SealedGoal [],
Ah, it seems that src/coq_elpi_HOAS.ml ignores the cast_kind inside constr2lp?
Paolo Giarrusso (Jul 22 2022 at 12:52):so one cannot output a vm_cast through coq-elpi, and if the ltac output goes through coq-elpi's term representation, it makes sense you can't do it through ltac either.
Paolo Giarrusso (Jul 22 2022 at 13:01):https://github.com/LPCIC/coq-elpi/blob/640b3cf38d7f84c6f107f6482c8a52f7f9ddda72/src/coq_elpi_HOAS.ml#L1237 ignores the cast_kind and turns casts into applications, while https://github.com/LPCIC/coq-elpi/blob/640b3cf38d7f84c6f107f6482c8a52f7f9ddda72/src/coq_elpi_HOAS.ml#L1734 uses Constr.DEFAULTcast unconditionally.
Paolo Giarrusso (Jul 22 2022 at 13:01):I can live with it, but users of native_cast probably can't.
Paolo Giarrusso (Jul 22 2022 at 20:08):Filed as https://github.com/LPCIC/coq-elpi/issues/375.
Enrico Tassi (Jul 22 2022 at 20:14):thanks, I knew the limitation, but never had a use case since typically ltac1 is used to kill a goal, while you seem to look at how the goal was killed to do something withthat term.
Paolo Giarrusso (Jul 22 2022 at 20:18):Not really: I just want the vm_cast to end up in the actual proof
Paolo Giarrusso (Jul 22 2022 at 20:22):All I do after the above with BoFinite is this:
coq.env.add-const InstanceName BoFinite ETyFinite @transparent! C,
am I doing this wrong?
Paolo Giarrusso (Jul 22 2022 at 20:28):I should say I _don't_ know what I'm doing, and I'm sorry about that — I started from Gordon's code, and only skimmed your docs lazily (as in call-by-need, not necessarily as in the character flaw).
This pattern doesn't appear in https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html.
But I'm working on a top-level command, and https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html suggests coq.env.add-const, and that takes a term.
Paolo Giarrusso (Jul 22 2022 at 20:50):Also, it _seems_ Ltac shouldn't really be essential — ultimately, I only invoke apply: bool_decide_eq_true_1; vm_compute; reflexivity. with Lemma bool_decide_eq_true_1 P {!Decision P}: bool_decide P = true → P., so there might be no need to go through Ltac (and it might be faster to skip that step, not sure, but at least one doesn't depend on the legacy Ltac1)? The following proof script also works, and one hopes that would translate to elpi — except for the vm_compute` cast:
refine (bool_decide_eq_true_1 _ _).
match goal with
|- ?G =>
refine (@eq_refl _ true <: G)
end.
(and yes, this is more complex than seems needed, but inlining the two refines tries to run vm_compute _before_ TC inference finds the actual Decision instance to run).
Enrico Tassi (Jul 23 2022 at 05:41):Yes, I was not clear. what you do makes sense, the fix is not hard, one has to do something like encoding in the name of the degenerate let in the kind of cast, eg
let `<:` ty t x\x
or something along these lines.
Enrico Tassi (Jul 23 2022 at 05:41):casts in elpi don't have a dedicated term constructor
Enrico Tassi (Jul 23 2022 at 05:43):In coq
let name : ty := t in name
Coq had historically many hiccups becase of the special term constructor which has to be ignored by most, but not discarded either ... so I went the let way.
Enrico Tassi (Jul 23 2022 at 05:47):now, given the name is irrelvant, even more in elpi, you can put anything in there
Paolo Giarrusso (Jul 23 2022 at 10:21):So alpha-renaming would change typechecking performance? I feel like I should ask: should anything ignore a vm cast? I agree on normal casts but not here.
Paolo Giarrusso (Jul 23 2022 at 10:22):Thankfully name hints are available in elpi's HOAS, so the basics work, but it doesn't seem like a long-term solution.
Enrico Tassi (Jul 23 2022 at 15:25):well, another option is to use a known, named and global, identity function:
Definition vmcast T (x:T) := x.
and have the HOAS recognise it.
But note that elpi never touches these pphints, and they are converted to casts, so coq s pp would not rename either. I don't think there is much risk.
Paolo Giarrusso (Jul 23 2022 at 16:24):I agree there isn't a _concrete_ bug with pp hints. My (weakly held) opinion is that it seems to violate the principle of least surprise, and I speculate some people writing transformers will need to account for this specifically, and that they will be surprised. "Weakly held" = feel free to stop listening, but I'd be interested in alternatives :-)
Paolo Giarrusso (Jul 23 2022 at 16:26):For the vmcast function, calls to it would only exist in the elpi term representation, but not in Coq's term representation? That sounds less surprising and is closer to adding a separate term constructor.
Paolo Giarrusso (Jul 23 2022 at 17:58):In any case, both solutions are enough for the short/medium term; my concerns above are only about the long term.
Janno (Mar 07 2024 at 11:00):Has anything changed regarding the situation with casts since this discussion? I am trying to use volatile casts :> in terms that go through coq-elpi and the fact that they are turned into normal casts ends up undoing the advantages of using them in the first place. I could maybe use lazy beta to reduce them but I am not confident that there couldn't be other terms that are disturbed by that.
How difficult would it be to add casts to coq-elpi's AST? I feel not having them is an interoperability headache.
Enrico Tassi (Mar 07 2024 at 13:13):The two places were we lose information from coq to elpi are:
https://github.com/LPCIC/coq-elpi/blob/363f4dc74819402e0d958c52f6bb63f889b9e459/src/coq_elpi_HOAS.ml#L1316-L1321
https://github.com/LPCIC/coq-elpi/blob/363f4dc74819402e0d958c52f6bb63f889b9e459/src/coq_elpi_glob_quotation.ml#L245-L249
The place where we reconstruct a regular cast is:
https://github.com/LPCIC/coq-elpi/blob/363f4dc74819402e0d958c52f6bb63f889b9e459/src/coq_elpi_HOAS.ml#L1854-L1861
If the extra info is hacked into the name, it seems rather quick. We can refine later maybe..
Janno (Mar 07 2024 at 13:27):I understand that we could work around it by encoding the cast type in the binder name. I am just not a huge fan of those kinds of workarounds. I suppose it seems inherently odd to me to pretend that one AST constructor of Coq simply doesn't exist in a metaprogramming language for Coq. Would it really be that bad to treat it like any other AST constructor?
Enrico Tassi (Mar 07 2024 at 14:19):We could, but I'm not very happy about it since all functions that inspect terms would need to be adapted, and let-in aleady has the type of the term in it. In particular it caused a lot of confusion, since it is not a term constructor you want to see in most of the cases (it is really meta). I mean, should lazy/whd get rid of it or no? The encoding with a degenerate let-in has the good property that code not handling let-in is broken anyway, so the bug does not come from the "cast". Don't get me wrong, it is not perfect either...
if you want to go the other way suggested above, then the encoding I suggest would be Cast(t,kind,ty) goes to let x : ty := tag t in x (in elpi) where tag would be a known identity constant. Here an example on how to get it:
https://github.com/LPCIC/coq-elpi/blob/363f4dc74819402e0d958c52f6bb63f889b9e459/src/coq_elpi_HOAS.ml#L636
and there should be one per kind of cast I guess.
The code paths to be changed are the same, this is why I think starting with the hack is not that bad after all, since it would allow you to test/play with it almost immediately.
Last updated: Oct 13 2024 at 01:02 UTC