Stream: Coq users

Topic: multi-goal repeat


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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:59):

Answer: yes.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:59):

Look at the definition of repeat in Ltac2.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:01):

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:04):

That's the role of Control.enter.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:05):

If you simply remove it your tactic will be multigoal.

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:06):

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:07):

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:27):

You can try your luck with the FFI

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:30):

You have to pass it as an argument.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:30):

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

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

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

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

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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:34):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:34):

the Ltac1 one or the Ltac2 one ?

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:34):

the ltac1 one

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:35):

It's probably parsed as a constr.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:35):

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:35):

ah, good point

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:35):

(Another wonder of Ltac1 "semantics".)

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:36):

yeah

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:36):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:37):

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:37):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:38):

The progress is probably on the wrong side?

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:38):

yeah

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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:41):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:41):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:41):

In that case enter should be a noop

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:41):

yeah

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:42):

Nope.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:42):

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

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:43):

Let me try on my side.

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:43):

thx

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:45):

gtg, will keep you informed later

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 16:45):

alright!

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 17:26):

Here is an example with a self-contained code.

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

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

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

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

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

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 17:53):

awesome! that works indeed. thanks a lot!

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:26):

Yes, constr quotations need to be focussed.

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 19:26):

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

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 19:28):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

Yes.

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 19:28):

why?

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

For variables and what not.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

A term is always a term in a context.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:28):

So if you have several contexts...

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

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 19:30):

(possibly wrapping up bar in a notation)

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

view this post on Zulip Armaël Guéneau (Nov 20 2020 at 20:21):

(assuming a coercion string -> stringlike)


Last updated: Feb 08 2023 at 22:03 UTC