Stream: Coq users

Topic: Tactics taking open terms with typeclass arguments


view this post on Zulip Janno (Mar 06 2024 at 15:42):

What's the correct way to write a tactic (notation) that takes a term which may have holes but which also has implicit typeclass arguments that should be resolved right away? I am fine with leaving the TC arguments unresolved if TC search fails but I do need Coq to at least attempt to fill them.

view this post on Zulip Janno (Mar 06 2024 at 15:47):

Possible answer: Start with uconstr and then go through open_constr:(ltac:(refine t))

view this post on Zulip Janno (Mar 06 2024 at 15:52):

No, that seems to be a terrible idea. It leaves all the original holes in t on the shelf, I think.

view this post on Zulip Pierre Courtieu (Mar 06 2024 at 16:16):

Good question. I have no real answer but you can use ˋlet ˋ to force resolution before using the tactic accepting holes.

let t := termtosolve in
refin (f t terwithholes).

view this post on Zulip Janno (Mar 06 2024 at 16:22):

It seems I have to use either uconstr:, open_constr: or constr: for around termtosolve in that let binding. I can't get Coq to accept an arbitrary term there without one of those quotations.

view this post on Zulip Pierre Courtieu (Mar 06 2024 at 16:26):

Yes that is because Ltac expects a tactic value at this point by default.

view this post on Zulip Pierre Courtieu (Mar 06 2024 at 16:27):

Constr = "solve the implicits now".

view this post on Zulip Gaëtan Gilbert (Mar 06 2024 at 16:37):

I don't remember why the open_constr_flags I exposed in ltac2 https://github.com/coq/coq/blob/26fbe83cafff74ed98a8ef1e2f26a853a0ac9812/user-contrib/Ltac2/Constr.v#L150 solves typeclasses when ltac2 open_constr:() does not but that's how it works
so I guess let x := ltac2val:(x |- Ltac1.of_constr (Pretype.pretype open_constr_flags expected_without_type_constraint (Option.get (Ltac1.to_preterm x))) in let x := x termtosolve in ... would work?

view this post on Zulip Janno (Mar 06 2024 at 16:50):

Ltac1.to_preterm is only available on master, isn't it?

view this post on Zulip Janno (Mar 06 2024 at 16:53):

I just tested it on master it seems to do the right thing. Thank you!


Last updated: Jun 18 2024 at 21:01 UTC