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
Binder.name return an option. Where I should look for a function that actually creates an ident?
This ident is the base name, so you can pick whatever you want.
(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)
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.
please publish the code to see whether there is a shorter / more idiomatic way to do that
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.
do you have some tests?
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.
(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)
why not directly match on the kind instead of lazy_match?
yeah also, although you shouldn't use the unsafe functions in basic situations
(i.e. we should provide a set of destructors returning options)
they're not anymore unsafe than mixing ltac2 let and constr binders
Unsafe is there to signal that this is compiler-level detail
we don't make any promise that this API is going to be stable (it can change if we change the kernel AST)
instead, one should use higher-level functions
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.
yeah, value-returning CPS is the bane of Ltac1
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.)
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
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
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.
fair enough, I was just innocently mentioning scaling issues that are hard to overcome in Ltac1
By the way, where does
intro $x come from? I did not find it in the documentation.
it's the same basic primitive as Ltac1
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
Oh! I had completely missed
(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