Stream: Coq users

Topic: multi-goal repeat

Armaël Guéneau (Nov 20 2020 at 15:59):

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?

Pierre-Marie Pédrot (Nov 20 2020 at 15:59):

Answer: yes.

Pierre-Marie Pédrot (Nov 20 2020 at 15:59):

Look at the definition of repeat in Ltac2.

Pierre-Marie Pédrot (Nov 20 2020 at 16:01):

(In user-contrib/Ltac2/Notations.v)

Armaël Guéneau (Nov 20 2020 at 16:04):

thanks!
Hmm, I suspect that I need to replace the call to Control.enter to something that distributes the tactic on all goals?

Pierre-Marie Pédrot (Nov 20 2020 at 16:04):

That's the role of Control.enter.

Pierre-Marie Pédrot (Nov 20 2020 at 16:05):

If you simply remove it your tactic will be multigoal.

Armaël Guéneau (Nov 20 2020 at 16:05):

I assumed that Control.enter focused on the first goal, is that what you mean?

Armaël Guéneau (Nov 20 2020 at 16:06):

(sorry, I'm very much a ltac2 noob at this point...)

Pierre-Marie Pédrot (Nov 20 2020 at 16:06):

Control.enter f evaluates f on every goal under focus, one by one, in order.

Pierre-Marie Pédrot (Nov 20 2020 at 16:07):

https://coq.inria.fr/refman/proof-engine/ltac2.html#goals

Armaël Guéneau (Nov 20 2020 at 16:09):

thanks. then I think I have all I need to code this multigoal repeat, just need to think it through :-)

Armaël Guéneau (Nov 20 2020 at 16:27):

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)?

Pierre-Marie Pédrot (Nov 20 2020 at 16:27):

You can try your luck with the FFI

Pierre-Marie Pédrot (Nov 20 2020 at 16:29):

It is possible to pass an Ltac1 closure to Ltac2 as an untyped blob, and run that thing inside the argument of grepeat

Armaël Guéneau (Nov 20 2020 at 16:29):

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)

Armaël Guéneau (Nov 20 2020 at 16:30):

(as you can probably notice, I don't really understand how the |- syntax is supposed to be working)

Pierre-Marie Pédrot (Nov 20 2020 at 16:30):

You have to pass it as an argument.

Pierre-Marie Pédrot (Nov 20 2020 at 16:30):

ltac2:(x |- t) builds a Ltac1 function that takes one argument.

Pierre-Marie Pédrot (Nov 20 2020 at 16:31):

The x variable is bound inside the body with a Ltac1 generic type, and you can use it in there.

Pierre-Marie Pédrot (Nov 20 2020 at 16:32):

so, something along the lines of

Ltac grepeat t :=
  let f := ltac2:(tac |- grepeat (fun _ => Ltac1.run tac)) in
  f t.

Janno (Nov 20 2020 at 16:32):

(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.)

Pierre-Marie Pédrot (Nov 20 2020 at 16:32):

(The trivial let-cut is to allow Ltac1 parsing, since you can only apply identifiers in Ltac1...)

Armaël Guéneau (Nov 20 2020 at 16:32):

ah, thanks! I was almost there...
it fails with a parsing error if one does not let-bind the ltac2:()

Armaël Guéneau (Nov 20 2020 at 16:34):

hmm, it still says that it can't find my ltac1 tactic foo in grepeat foo..

Pierre-Marie Pédrot (Nov 20 2020 at 16:34):

@Kenji Maillard not my fault, have you ever tried to write higher-order / value returning Ltac1?

Pierre-Marie Pédrot (Nov 20 2020 at 16:34):

@Armaël Guéneau which grepeat are you talking about?

Pierre-Marie Pédrot (Nov 20 2020 at 16:34):

the Ltac1 one or the Ltac2 one ?

Armaël Guéneau (Nov 20 2020 at 16:34):

the ltac1 one

Pierre-Marie Pédrot (Nov 20 2020 at 16:35):

It's probably parsed as a constr.

Pierre-Marie Pédrot (Nov 20 2020 at 16:35):

You need to wrap it into ltac:(...)

Armaël Guéneau (Nov 20 2020 at 16:35):

ah, good point

Pierre-Marie Pédrot (Nov 20 2020 at 16:35):

(Another wonder of Ltac1 "semantics".)

Pierre-Marie Pédrot (Nov 20 2020 at 16:36):

For easiness (and more fun trying to understand wtf went wrong) just export a Ltac1 Tactic Notation.

Armaël Guéneau (Nov 20 2020 at 16:36):

yeah

Armaël Guéneau (Nov 20 2020 at 16:36):

ok it runs now, but it seems I need to debug my ltac2 grepeat

Pierre-Marie Pédrot (Nov 20 2020 at 16:37):

Copy-pasting the one from Notations and removing Control.enter was not enough?

Armaël Guéneau (Nov 20 2020 at 16:37):

    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

Armaël Guéneau (Nov 20 2020 at 16:37):

t is single goal, so I think I need to have a Control.enter somewhere still?

Pierre-Marie Pédrot (Nov 20 2020 at 16:37):

Ltac1 does fancy stuff w.r.t. focussing.

Pierre-Marie Pédrot (Nov 20 2020 at 16:38):

The progress is probably on the wrong side?

Pierre-Marie Pédrot (Nov 20 2020 at 16:38):

it's progressing if there is at least one goal that progressed, is it the desired behaviour?

Armaël Guéneau (Nov 20 2020 at 16:38):

yeah

Pierre-Marie Pédrot (Nov 20 2020 at 16:39):

I am not sure of what the enter in your code is supposed to do.

Pierre-Marie Pédrot (Nov 20 2020 at 16:40):

I think it's effectively ruining the multigoal behaviour of the repeat (assuming you properly defined the expected semantics of grepeat)

Armaël Guéneau (Nov 20 2020 at 16:40):

hmm well I want to call t on each goal, and continue if it succeeded on at least one goal

Armaël Guéneau (Nov 20 2020 at 16:40):

(t is instantiating evars, so making progress on one goal may allow making progress on another goal later)

Pierre-Marie Pédrot (Nov 20 2020 at 16:41):

You don't need the enter for that, Ltac1 focusses dynamically when needed

Pierre-Marie Pédrot (Nov 20 2020 at 16:41):

But yeah, you're expecting t to be a single-goal tactic right?

Pierre-Marie Pédrot (Nov 20 2020 at 16:41):

In that case enter should be a noop

Armaël Guéneau (Nov 20 2020 at 16:41):

yeah

Armaël Guéneau (Nov 20 2020 at 16:42):

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?

Pierre-Marie Pédrot (Nov 20 2020 at 16:42):

Nope.

Pierre-Marie Pédrot (Nov 20 2020 at 16:42):

Ltac1 does implicit enters "sometimes" and two enter are the same as one.

Pierre-Marie Pédrot (Nov 20 2020 at 16:43):

But it might be the case here that something is wrong with the dynamic enter.

Pierre-Marie Pédrot (Nov 20 2020 at 16:43):

Let me try on my side.

Armaël Guéneau (Nov 20 2020 at 16:43):

right now it looks like as if enter is only executing t on the first goal

Armaël Guéneau (Nov 20 2020 at 16:43):

thx

Pierre-Marie Pédrot (Nov 20 2020 at 16:45):

gtg, will keep you informed later

Armaël Guéneau (Nov 20 2020 at 16:45):

alright!

Pierre-Marie Pédrot (Nov 20 2020 at 17:25):

So I guess that the problem comes from the tactic failing in one of the entered goals.

Pierre-Marie Pédrot (Nov 20 2020 at 17:26):

Here is an example with a self-contained code.

Pierre-Marie Pédrot (Nov 20 2020 at 17:26):

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).

Pierre-Marie Pédrot (Nov 20 2020 at 17:27):

The last invocation fails because foo will fail if it does not manage to apply to one goal.

Pierre-Marie Pédrot (Nov 20 2020 at 17:27):

the semantics of constructor over several goals is to apply in parallel, and succeed if all succeed.

Pierre-Marie Pédrot (Nov 20 2020 at 17:28):

Assuming you are in a similar situation, you need to wrap the Ltac1 you want to apply inside a try block.

Pierre-Marie Pédrot (Nov 20 2020 at 17:46):

You also have to be careful that the tactic you're evaluating is really a thunk (i.e. you have to write it as idtac; ...)

Pierre-Marie Pédrot (Nov 20 2020 at 17:47):

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).

Armaël Guéneau (Nov 20 2020 at 17:53):

awesome! that works indeed. thanks a lot!

Armaël Guéneau (Nov 20 2020 at 19:25):

uh, I have a scenario where, in Ltac2, foo; bar (). succeeds, but foo; bar constr:("H":string). fails with the exception Not_focussed... (bar has type 'a -> unit).

Pierre-Marie Pédrot (Nov 20 2020 at 19:26):

Yes, constr quotations need to be focussed.

Armaël Guéneau (Nov 20 2020 at 19:26):

(in the real example I need the type annotation to insert a coercion)

Pierre-Marie Pédrot (Nov 20 2020 at 19:27):

constr:(...) is an impure expression that fails when there is more than one goal under focus

Armaël Guéneau (Nov 20 2020 at 19:28):

uhm, ok… but does it need to lookup the current goal?

Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

Yes.

Armaël Guéneau (Nov 20 2020 at 19:28):

why?

Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

For variables and what not.

Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

A term is always a term in a context.

Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

So if you have several contexts...

Armaël Guéneau (Nov 20 2020 at 19:29):

right. so how do I focus (whatever goal) in the constr? here it's important that bar stays multigoal

Armaël Guéneau (Nov 20 2020 at 19:30):

or alternatively, is there a better way to indicate that I want "H" to be typed as type baz (possibly inserting a coercion)?

Armaël Guéneau (Nov 20 2020 at 19:30):

(possibly wrapping up bar in a notation)

Armaël Guéneau (Nov 20 2020 at 20:19):

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 uconstr.

Armaël Guéneau (Nov 20 2020 at 20:21):

(assuming a coercion string -> stringlike)

Last updated: Apr 19 2024 at 14:02 UTC