The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

The problem with using an open_constr instead of a uconstr is that all 
of the implict args immediately become shelved existential goals.  Just 
try doing "Show Existentials" after the head_pose_proof call.

My purpose to trying to get to the explicitized version of the function 
name is just so I have more control over those shelved existential goals 
- as in not shelving them.  I know I can do a refine (let H:=foo in _) - 
so that the implicit args become unshelved subgoals, but in this case I 
want to deal with one arg at a time, and foo might have multiple 
implicit args.

-- Jonathan

On 11/12/2015 02:48 PM, Jason Gross wrote:
> Does this do what you want?
>
> Tactic Notation "with_open" open_constr(v) tactic3(tac) := tac v.
>
> Tactic Notation "foo'" uconstr(v) tactic3(foo2) :=
>    first [ let v' := constr:v in tryif has_evar v' then fail else pose proof
> v
>          | with_open v foo2 ].
>
> Ltac foo2 v :=
>      idtac;
>      match v with
>        | ?f _ => foo' f foo2
>        | _ => fail 1
>      end.
>
> Tactic Notation "head_pose_proof" uconstr(v) := foo' v foo2.
>
> Goal True -> True.
>    intro H.
>    head_pose_proof eq_refl.
>
> Or, if you want something simpler:
>
> Ltac head x :=
>    match x with
>      | ?f _ => head f
>      | _ => constr:x
>    end.
>
> Tactic Notation "head_pose_proof" open_constr(v) := let v' := head v in
> pose proof v'.
>
> which may or may not have the behavior you want on things with explicit
> arguments already passed.
>
>
>
> On Thu, Nov 12, 2015 at 11:35 AM, Jonathan Leivent 
> <jonikelee AT gmail.com>
> wrote:
>
> > Given the name of a function with implicit args, say "foo", the name
> > "@foo" names the same function with all args made explict.  However, the
> > "@" does not seem to be an operator that one can apply to a name
> > tactically.  For example - the following doesn't work:
> >
> > Tactic Notation "Explicitly" uconstr(L) := pose proof @L.
> >
> > as it appears to ignore the "@", with the result that pose proof fails due
> > to uninferrable implicits.
> >
> > Is there any way to take a name of a function and tactically change it to
> > its explicit version?
> >
> > -- Jonathan