Stream: Ltac2

Topic: Manipulation under a binder

Meven Lennon-Bertrand (Mar 15 2024 at 11:34):

Rather than keeping on asking XY questions like the previous one, let me ask the real one. I am trying to turn Ltac code looking more or less like the following (admittedly quite ugly) into something sensible, ideally an Ltac2 function from constr to constr:

Ltac bundle Hyp :=
    lazymatch Hyp with
      | F1 ?A ?B => constr:(F1' A B)
      | F2 ?A ?B => constr:(exists T, F2' A B T)
      | ?Hyp' => constr:(Hyp')
    end.

Ltac weak_concl concl :=
    lazymatch concl with
    | ?Hyp -> ?T => let T' := weak_concl T in let Hyp' := bundle Hyp in constr:(Hyp' -> T')
    | forall x : ?Hyp, @?T x => constr:(forall x : Hyp, ltac:(
      let T' := ltac:(eval hnf in (T x)) in let T'' := weak_concl T' in exact T''))
    | ?T => constr:(T)
    end.

Where F1, F1', F2 and F2' are definition names. The idea is that concl is some forall x1 : T1, …, xn : Tn, H1 -> … Hn -> C (a method of a induction principle), and I want to
1) traverse under all dependent binders
2) apply a transformation to all non-dependent hypotheses Hi, to turn them into Hi' with the same free variables, but potentially more bound variables (see F2')
My main issue is part 1, which is where the Ltac code really is terrible. How can I do this "do something under binders then close after yourself" in a reasonable way? Is this even possible without resorting to low-level unsafe primitives? I am not afraid of de Bruijn variables, but would also prefer avoiding them if possible.

Jason Gross (Mar 21 2024 at 18:00):

You are looking for Constr.in_context which let's you extend the context and recuse under binders. It's not performant, though, and Ltac2 is lacking the primitives for performant recursion under binders.

Meven Lennon-Bertrand (Mar 21 2024 at 18:23):

It goes in the right direction, although I'm not sure how to use it in my case, where what I want to do "under the binder" is term manipulation (that, is, use a constr -> constr) rather than unit -> unit…

Jason Gross (Mar 22 2024 at 03:36):

Constr.in_context gives you a new goal, so you want to do Constr.in_context ... (fun () => ... ; Control.refine (fun () => <the new constr>))

Jason Gross (Mar 22 2024 at 03:37):

This is what makes it so much of a performance kill, that it's effectively a slightly nicer version of constr:(ltac2:(...))

Last updated: Oct 12 2024 at 12:01 UTC