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

Using Coq
1

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.

2

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.)

3

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 :

4

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?

5

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