The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> I ran into something similar to this yesterday and came up with the
> following solution:
> 
> (** This is my 'Var' constructor **)
> Var_ctx
>      : forall (a : otype) (n : nat) (ls : list otype),
>        List.nth_error ls n = Some a -> InCtx ls a
> 
> (** This tactic exposes the spine of a list **)
> Ltac make_cons T n :=
>   let rec go n :=
>       lazymatch n with
>       | 0 => uconstr:(@cons T _ _)
>       | S ?Z =>
>         let p := go Z in
>         uconstr:(@cons T _ p)
>       end
>   in
>   let z := go n in
>   refine z.
> 
> (** Here is the notation that uses tactics-in-terms to call [make_cons] **)
> Notation "# n" := (@Var_ctx _ n%nat ltac:(make_cons otype n) eq_refl)
> (at level 0) : ctx_scope.
> 
> Here, the [make_cons] tactic makes a list that exposes the spine, e.g.
> [make_cons nat 2] will produce (_ :: _ :: _ :: _). When Coq sees this,
> it can reduce the fixpoint to [Some _ = Some _] which [eq_refl] solves.
> Then, later is unifies (_ :: _ :: _ :: _) with this list.

Thanks for this example, it is a nice illustration for tactics-in-terms
-- in particular this pattern of not actually constructing the full
term, but preparing the structure such that unification can do the rest,
sounds useful.

The Notation you defined, is this useful for printing at all? I doubt
the pretty printer can figure out if the actual proof term it sees, when
it prints some @Var_ctx, was actually generated using the given tactic,
so it could either ignore the ltac:(...) when printing, or it could just
never use this notation for printing.

Kind regards,
Ralf