The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/01/2016 01:22 AM, Gregory Malecha wrote:
> Hello --
>
> I'm wondering if anyone has a trick to get tactics-in-terms to fire later?
> Here's a somewhat contrived example:
>
> Definition foo (ls : list nat) : nat := 0.
>
> Ltac try_something :=
>    lazymatch goal with
>    | |- nat => exact 0
>    | |- bool => exact true
>    end.
>
> Notation "'it'" := ltac:(try_something) (at level 0).
>
> Definition bar : nat := foo (it :: nil).
>
> In the last line, we know that the type of 'it' should be [nat] since [foo]
> takes an argument of type [list nat]. However, when the Ltac actually
> fires, the goal is a unification variable and therefore neither of branches
> of the [lazymatch] matches.
>
> Any hackish tricks to get this to work? Possibly something involving
> 'Program' or canonical structures?

About tactic-in-term: one can force it to see an instantiated conclusion 
only by (that I know of) a cast.  In other words, if you can do 
"ltac:(tac):T", then tac will see T instead of an evar as the 
conclusion.  However, I don't see how to use that fact to help you here.

-- Jonathan