Stream: Ltac2

Topic: Creating a fresh ident

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?

Pierre-Marie Pédrot (Feb 03 2022 at 16:47):

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

Pierre-Marie Pédrot (Feb 03 2022 at 16:47):

Like @myfavouritebasenameident

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)

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.

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

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.

Pierre-Marie Pédrot (Feb 03 2022 at 17:10):

do you have some tests?

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.

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)

Gaëtan Gilbert (Feb 03 2022 at 17:22):

why not directly match on the kind instead of lazy_match?

Pierre-Marie Pédrot (Feb 03 2022 at 17:24):

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

Pierre-Marie Pédrot (Feb 03 2022 at 17:24):

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

Gaëtan Gilbert (Feb 03 2022 at 17:25):

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

Pierre-Marie Pédrot (Feb 03 2022 at 17:26):

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

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)

Pierre-Marie Pédrot (Feb 03 2022 at 17:26):

instead, one should use higher-level functions

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.

Pierre-Marie Pédrot (Feb 03 2022 at 17:27):

yeah, value-returning CPS is the bane of Ltac1

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

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

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

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.

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

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.

Pierre-Marie Pédrot (Feb 03 2022 at 17:35):

it's the same basic primitive as Ltac1

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

Guillaume Melquiond (Feb 03 2022 at 17:37):

Oh! I had completely missed Notations.v.

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: Nov 29 2023 at 21:01 UTC