[Ltac] Tactic that "@" a function passed as argument · Coq users

Hello,
I am trying to write a tactic foo that takes as argument the name of a lemma f which may have maximally inserted implicits as first arguments, pattern match on my context to find these implicits, and uses @f ... in the body of the tactic. I am failing to do what I want without having to call explicitly foo @f rather than foo f.

Variable f : nat -> bool -> Prop.
Arguments f {n} b.

Ltac foo g := assert (g 0 true).

Goal False.
  foo @f. (* Works *)
  (* How can I work an alternative to [foo] that will perform the same thing, but works when called on [f] instead of [@f]? *)
Abort.

(* Unsuccessful attempts: I assumed that I have to go through a tactic notation to use a `uconstr` to prevent the argument to fail type-checking at call-time, but I am utterly confused by what happens then *)
Ltac foo1 g := assert (@g 0 true).
Tactic Notation "foo2" uconstr(g) := foo1 g.
Tactic Notation "foo3" uconstr(g) := foo1 @g.
Tactic Notation "foo4" uconstr(g) := assert (@g 0 true).
Goal False.
  Fail foo1 f. (* cannot infer the implicit parameter: expected, f is type-checked when foo' is called *)
  Fail foo2 f. (* The term "0" has type "nat" while it is expected to have type "bool".
                  This I don't quite understand: I would have expected the call to [foo1]
                  to fail is in the first case.
                  However it happily calls [g], so somehow the untyped annotation must
                  propagate in the body of the notation, but then the [@] in the body of [foo1]
                  ends up being ignored?
                *)
  Fail foo3 f. (* Same result, similar confusion *)
  Fail foo4 f. (* And same as well when inlined *)

Any help in both understanding what I am misunderstanding about uconstr and solving the issue would be awesome :)

Gaëtan Gilbert (Apr 10 2022 at 15:33):

AFAIK implicit argument handling is done before uconstr, ie uconstr already have implicit arguments inserted
so in the notations g is bound to a uconstr which is f applied to a hole
in foo2, foo1 is applied to the variable g so it doesn't get re-interpreted, then it does basically assert (@(@f _) 0 true) (this is fake syntax as @ only works with references)
same with foo4 just with less indirection
in foo3 when running foo1 @g it does constr:(@g) ie constr:(@f _) and finds out that there's a hole in g

I don't think you can make uconstr work for this, maybe reference but Tactic Notation "foo5" reference(g) := foo1 g. doesn't work so I don't know

Stream: Coq users

Topic: [Ltac] Tactic that "@" a function passed as argument

Yannick Zakowski (Apr 10 2022 at 15:12):

Gaëtan Gilbert (Apr 10 2022 at 15:33):

Yannick Zakowski (Apr 10 2022 at 15:51):