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.

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.

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`

…

`Constr.in_context`

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

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