Hey, I stumbled upon https://github.com/coq/coq/issues/9462 after figuring out that indeed,
repeat is not multigoal as I expected. Question: can a multigoal repeat be implemented using Ltac2?
Look at the definition of
repeat in Ltac2.
Hmm, I suspect that I need to replace the call to Control.enter to something that distributes the tactic on all goals?
That's the role of
If you simply remove it your tactic will be multigoal.
I assumed that Control.enter focused on the first goal, is that what you mean?
(sorry, I'm very much a ltac2 noob at this point...)
Control.enter f evaluates
f on every goal under focus, one by one, in order.
thanks. then I think I have all I need to code this multigoal repeat, just need to think it through :-)
hmm, so, now I have a
grepeat : (unit -> unit) -> unit defined in Ltac2. Is there a way of exposing it as a Ltac1 tactic(al)?
You can try your luck with the FFI
It is possible to pass an Ltac1 closure to Ltac2 as an untyped blob, and run that thing inside the argument of
I tried to do
Ltac grepeat t := ltac2:(t |- grepeat)., but then
grepeat foo says it doesn't find foo. (where foo is a ltac tactic)
(as you can probably notice, I don't really understand how the |- syntax is supposed to be working)
You have to pass it as an argument.
ltac2:(x |- t) builds a Ltac1 function that takes one argument.
The x variable is bound inside the body with a Ltac1 generic type, and you can use it in there.
so, something along the lines of
Ltac grepeat t := let f := ltac2:(tac |- grepeat (fun _ => Ltac1.run tac)) in f t.
(I don't remember why but I started let-binding all my
ltac2:(s. I think it produced better error messages when one forgets to apply it? In any case it doesn't hurt.)
(The trivial let-cut is to allow Ltac1 parsing, since you can only apply identifiers in Ltac1...)
ah, thanks! I was almost there...
it fails with a parsing error if one does not let-bind the ltac2:()
hmm, it still says that it can't find my ltac1 tactic
@Kenji Maillard not my fault, have you ever tried to write higher-order / value returning Ltac1?
@Armaël Guéneau which
grepeat are you talking about?
the Ltac1 one or the Ltac2 one ?
the ltac1 one
It's probably parsed as a constr.
You need to wrap it into ltac:(...)
ah, good point
(Another wonder of Ltac1 "semantics".)
For easiness (and more fun trying to understand wtf went wrong) just export a Ltac1 Tactic Notation.
ok it runs now, but it seems I need to debug my ltac2 grepeat
Copy-pasting the one from Notations and removing Control.enter was not enough?
Ltac2 rec grepeat (t: unit -> unit) := ifcatch (fun _ => Control.progress (fun _ => Control.enter t)) (fun _ => Control.check_interrupt (); grepeat t) (fun _ => ()).
here's what I have, but it doesn't seem to be doing anything right now
t is single goal, so I think I need to have a Control.enter somewhere still?
Ltac1 does fancy stuff w.r.t. focussing.
The progress is probably on the wrong side?
it's progressing if there is at least one goal that progressed, is it the desired behaviour?
I am not sure of what the enter in your code is supposed to do.
I think it's effectively ruining the multigoal behaviour of the repeat (assuming you properly defined the expected semantics of grepeat)
hmm well I want to call t on each goal, and continue if it succeeded on at least one goal
(t is instantiating evars, so making progress on one goal may allow making progress on another goal later)
You don't need the enter for that, Ltac1 focusses dynamically when needed
But yeah, you're expecting t to be a single-goal tactic right?
In that case enter should be a noop
if I remove the enter, won't it apply only to the first goal (if I rely on Ltac1 autofocusing), where I want it to apply on all the goals?
Ltac1 does implicit enters "sometimes" and two enter are the same as one.
But it might be the case here that something is wrong with the dynamic enter.
Let me try on my side.
right now it looks like as if enter is only executing t on the first goal
gtg, will keep you informed later
So I guess that the problem comes from the tactic failing in one of the entered goals.
Here is an example with a self-contained code.
Require Import Ltac2.Ltac2. Ltac2 rec grepeat (t : unit -> unit) := ifcatch (fun _ => Control.progress t) (fun _ => Control.check_interrupt (); repeat0 t) (fun _ => ()). Ltac grepeat t := let f := ltac2:(tac |- grepeat (fun _ => Ltac1.run tac)) in f t. Set Default Proof Mode "Classic". Ltac foo := match goal with | [ |- ?P ] => idtac P; constructor end. Goal exists n : nat, match n with 0 => True | S n => False end. Proof. unshelve eexists. all: cycle 1. all: grepeat ltac:(foo).
The last invocation fails because foo will fail if it does not manage to apply to one goal.
the semantics of
constructor over several goals is to apply in parallel, and succeed if all succeed.
Assuming you are in a similar situation, you need to wrap the Ltac1 you want to apply inside a try block.
You also have to be careful that the tactic you're evaluating is really a thunk (i.e. you have to write it as
So, something along those lines:
Require Import Ltac2.Ltac2. Ltac2 rec grepeat (t : unit -> unit) := ifcatch (fun _ => Control.progress t) (fun _ => Control.check_interrupt (); repeat0 t) (fun _ => ()). Ltac grepeat t := let t := try t in let f := ltac2:(tac |- grepeat (fun _ => Ltac1.run tac)) in f t. Set Default Proof Mode "Classic". Ltac foo := match goal with | [ |- ?P ] => constructor end. Goal exists n : nat, match n with 0 => True | S n => False end. Proof. unshelve eexists. all: cycle 1. all: grepeat ltac:(idtac; foo).
awesome! that works indeed. thanks a lot!
uh, I have a scenario where, in Ltac2,
foo; bar (). succeeds, but
foo; bar constr:("H":string). fails with the exception
bar has type
'a -> unit).
Yes, constr quotations need to be focussed.
(in the real example I need the type annotation to insert a coercion)
constr:(...) is an impure expression that fails when there is more than one goal under focus
uhm, ok… but does it need to lookup the current goal?
For variables and what not.
A term is always a term in a context.
So if you have several contexts...
right. so how do I focus (whatever goal) in the constr? here it's important that bar stays multigoal
or alternatively, is there a better way to indicate that I want "H" to be typed as type baz (possibly inserting a coercion)?
(possibly wrapping up
bar in a notation)
mmh, I figured out that I could do
let h := Control.focus 1 1 (fun _ => '("H":stringlike)) in bar h, but now I don't know how to wrap that in a notation, because there doesn't seem to be something similar to
(assuming a coercion
string -> stringlike)
Last updated: Oct 01 2023 at 17:01 UTC