Ltac that goes under binders to return a non constr value?

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 https://github.com/coq/coq/issues/7210, 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