Hi,

I know how to write a tactic that goes under binders of a term, using the `constr:(fun x => )`

trick. But I could not use this trick to return something else than a constr. Is it possible?

For the record I am trying to make my library LiHypsNaming able to find good names for hypothesis of the form `forall x, ...`

by looking at its conclusion recursively.

No, it is not possible, but if you say what kind of thing you want to return, there might be a way to encode that thing as a constr and then pull out out later. (For example, if you want to return a name, you can instead return a Î» whose argument has the given name.)

Thanks Jason I did exactly that. And a match context to extract it later.

Le sam. 6 avr. 2019 Ă 06:34, Jason Gross via Coq coq@discoursemail.com a Ă©crit :

Can anybody show an example of whatâ€™s possible? I donâ€™t think I ever heard this trickâ€¦

EDIT: googling led me to issue Ltac's tactics in terms pick up the wrong variable when names are repeated Â· Issue #7210 Â· coq/coq Â· GitHub, and I see e.g. `constr:(fun n n' : nat => ltac:(exact n))`

. But itâ€™s not clear how that lets me descend under existing binders, or what I can or cannot do. Surely, if this trick is well-known, thereâ€™s some explanation around?

I can try to explain.

Suppose I have a hypothesis of the form:

```
H: forall x y..., H1 -> H2 -> H3 -> ... -> (P ...).
```

My particular use case is the following: I would like to extract the name of P in order to use it to rename H into something like say `h_P`

. I need to open binders recursively to reach the application at the bottom of products and call the renaming tactic from there. But I canâ€™t because tactics cannot manipulate terms with free variables. The only way I can go into the type recursively is to build a term with a similar structure using the `lconstr:(forall x, ltac:())`

trick. the tactic inside the constr is is called in a proof environment where the enclosing binders have been â€śintroducedâ€ť.

The rest is ugly adhoc hack for my use case: I can build a term mimicking the structure of the type of H but with a special term at the bottom of the products such that I can then perform a `match .. with context [...]`

to extract it from the outside.

The goal of the tactic below is to build a term with the same products than in the type of H (th) but with a special recognizable pattern at the bottom of the products (so that a simple match x with context[â€¦] can catch it). It is a slighlty (untested) simplified version of this.

Hope it was clear.

```
Definition DUMMY:= fun x:Prop => x.
(* Extract the head of an application *)
Ltac head_application th :=
match th with
| ?f _ _ _ _ _ _ _ _ _ _ _ => f
| ?f _ _ _ _ _ _ _ _ _ _ => f
| ?f _ _ _ _ _ _ _ _ _ => f
| ?f _ _ _ _ _ _ _ _ => f
| ?f _ _ _ _ _ _ _ => f
| ?f _ _ _ _ _ _ => f
| ?f _ _ _ _ _ => f
| ?f _ _ _ _ => f
| ?f _ _ _ => f
| ?f _ _ => f
| ?f _ => f
end.
(* go under binder and rebuild a term with a good name inside,
catchable by a match context. *)
Ltac build_dummy_quantified h th :=
lazymatch th with
| forall z:?A , ?B =>
let x :=
constr:(
forall z:A,
let h' := (h z) in
ltac:(
let th' := type of h' in
let res := build_dummy_quantified h' th' in
exact res)) in
(* remove the let *)
eval lazy zeta in x
| _ =>
(* let nme := fallback_rename_hyp h th in *)
let hd := head_application th in
let frshnme := fresh hd in
(* Build something catchable with mathc context *)
constr:(forall frshnme:Prop, DUMMY frshnme)
end.
Lemma xxx:
(forall x y z:nat, x <y -> y< z -> x < z) -> True.
Proof.
intros h.
let typ := type of h in
let x := build_dummy_quantified h typ in
idtac x; (* Se the type built by the tactic *)
(* use it to rename h: *)
match x with
| context [forall X, DUMMY X] => let nme := fresh "h_" X in rename h into nme
end.
Qed.
```

1 Like