In Ltac, a context pattern can be used to build an Ltac-level function which accepts a Gallina term and constructs a Gallina term by filling in a hole. I would like to reify this function and use it at the level of Gallina, rather than Ltac.
E.g., the following code works using meta-variables rather than context patterns.
Variables
(A : Set)
(P : A -> Prop)
(a : A)
(H : forall Q: A -> Prop, Q a).
Goal (P a).
match goal with
| |- ?P a => exact (H P)
end.
Qed.
But the following code does not work because I cannot bring the variable x into scope before filling in the pattern:
Goal (P a).
match goal with
| |- context C[a] => let y := context C[x] in exact (H (fun x => y))
end.
(* The reference x was not found in the current
environment. *)
Nor does the following work because I cannot use Ltac within Gallina:
Goal (P a).
match goal with
| |- context C[a] => let y := exact (H (fun x => context C[x]))
end.
(* Syntax error... *)
But the following code shows that my context pattern works like I think it should:
Goal (P a).
match goal with
| |- context C[a] => let y := context C[a] in idtac y
end.
(* (P a) *)
While this example is trivial because the goal is a single application, in general I want to use context patterns to match significantly more complex goals and then use those patterns to build Gallina functions. Can this be done?
Use ltac:(...)
match goal with
| |- context C[a] => exact (H (fun x => ltac:(let y := context C[x] in exact y)))
end.
ltac:(...) can replace any Gallina term. The expected type of that hole becomes the goal for the contained tactic expression, which is executed to produce a new Gallina term to fill the hole.