Stream: Ltac2

Topic: Creating a fresh ident


view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 16:42):

So, I am now trying to create a fresh ident. And I have no idea on how to do that. Indeed, Fresh.in_goal has type ident -> ident. But how do I get the initial ident? Both Ident.of_string and Binder.name return an option. Where I should look for a function that actually creates an ident?

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 16:47):

This ident is the base name, so you can pick whatever you want.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 16:47):

Like @myfavouritebasenameident

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 16:48):

(the fact Ident.of_string returns an option is distinct from the binder one, in the first case it's because not all strings are valid identifiers, while in the second it's that not all binders are named)

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 16:52):

I understand why they return an option. But my 5-line Ltac1 tactic has now grown to a 30-line Ltac2 tactic, and I am still not sure I have reached feature parity.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 16:59):

please publish the code to see whether there is a shorter / more idiomatic way to do that

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:03):

This is Ltac1 code. I will not show the Ltac2 code yet, so as to not influence you.

Ltac unquantify_prop H cont :=
  lazymatch type of H with
  | forall x : ?T, _ =>
    let x' := fresh x in refine (fun x' : T => _) ;
    unquantify_prop constr:(H x') cont
  | _ => cont H
  end.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:10):

do you have some tests?

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:18):

what about this? it follows pretty much the Ltac1 code

Require Import Ltac2.Ltac2.

Ltac2 get_name c :=
match Constr.Unsafe.kind c with
| Constr.Unsafe.Prod b _ => Ltac2.Option.default @x (Constr.Binder.name b)
| _ => Control.throw Not_found
end.

Ltac2 rec unquantify_prop h :=
let t := Constr.type h in
lazy_match! t with
| forall x : _, _ =>
  let x := Fresh.in_goal (get_name t) in intro $x;
  let x := Control.hyp x in
  unquantify_prop '($h $x)
| _ => h
end.

Require Import Ltac2.Printf.

Goal (forall m n : nat, m = n) -> forall m n : nat, True.
Proof.
intros H.
let t := unquantify_prop &H in printf "%t" t.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:21):

(you can probably make this even more idiomatic by returning an option in get_name and matching on that instead of relying on lazy_match)

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 17:22):

why not directly match on the kind instead of lazy_match?

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:24):

yeah also, although you shouldn't use the unsafe functions in basic situations

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:24):

(i.e. we should provide a set of destructors returning options)

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 17:25):

why not?
they're not anymore unsafe than mixing ltac2 let and constr binders

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:26):

Unsafe is there to signal that this is compiler-level detail

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:26):

we don't make any promise that this API is going to be stable (it can change if we change the kernel AST)

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:26):

instead, one should use higher-level functions

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:27):

Unfortunately, I am not yet able to run all the tests because there is still a lot of Ltac1 around and it is hard to travel between Ltac1 and Ltac2. But after putting unquantify_prop back into CPS, the few tests I already have go through. But since your version does not seem to need Control.focus, I might be able to get rid of CPS, which should be a net boon. Thanks for the translation.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:27):

yeah, value-returning CPS is the bane of Ltac1

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:28):

Sure, but I needed it for Ltac2 too, because the continuation has to run on a specific subgoal. (But since your version does not create any subgoal, it should be fine to get rid of it now.)

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:28):

note that this implem is naive because you have to recompute the type of the application at each step, so you'd likely get a quadratic blowup

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:29):

in theory you should be able to do that more efficiently (although in a more involved way) using the low-level unsafe interfaces of Ltac2

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:30):

Yes, but it will not be worse than Ltac1, and in practice I do not expect the user to ever have more than three binders in a row.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:30):

fair enough, I was just innocently mentioning scaling issues that are hard to overcome in Ltac1

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:34):

By the way, where does intro $x come from? I did not find it in the documentation.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:35):

it's the same basic primitive as Ltac1

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:36):

I don't know whether it's in the doc, but you can read Std.v and Notations.v to have a list of basic notations / tactics exported by default

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:37):

Oh! I had completely missed Notations.v.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 17:37):

(there is no built-in magical tactics in Ltac2, at worst some notation scopes are pretty specific, but you can basically redefine the whole stuff from scratch if you wanted to)


Last updated: Jan 31 2023 at 09:01 UTC