Stream: Elpi users & devs

Topic: elpi -> ltac1 -> vm_compute = normal cast


view this post on Zulip 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 [],

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 12:51):

Ah, it seems that src/coq_elpi_HOAS.ml ignores the cast_kind inside constr2lp?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:01):

I can live with it, but users if native_cast can't.

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 20:08):

Filed as https://github.com/LPCIC/coq-elpi/issues/375.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 20:18):

Not really: I just want the vm_cast to end up in the actual proof

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jul 23 2022 at 05:41):

casts in elpi don't have a dedicated term constructor

view this post on Zulip Enrico Tassi (Jul 23 2022 at 05:43):

In coq

let name : ty := t in name

view this post on Zulip Enrico Tassi (Jul 23 2022 at 05:46):

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.

view this post on Zulip Enrico Tassi (Jul 23 2022 at 05:47):

now, given the name is irrelvant, even more in elpi, you can put anything in there

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.


Last updated: Feb 04 2023 at 02:03 UTC