В Lta c шаблон контекста может использоваться для построения функции Lta c -уровня , которая принимает термин Галлина и создает термин Галлина, заполняя отверстие. Я хотел бы усовершенствовать эту функцию и использовать ее на уровне Галлина, а не Lta c.
Например, следующий код работает с использованием мета-переменных, а не шаблонов контекста.
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.
Но следующий код не работает, потому что я не могу перенести переменную x в область действия перед заполнением шаблона:
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. *)
Также не работает следующее, потому что я не могу использовать Lta c в Галлина:
Goal (P a).
match goal with
| |- context C[a] => let y := exact (H (fun x => context C[x]))
end.
(* Syntax error... *)
Но следующий код показывает, что мой шаблон контекста работает так, как я думаю:
Goal (P a).
match goal with
| |- context C[a] => let y := context C[a] in idtac y
end.
(* (P a) *)
Хотя этот пример тривиален, поскольку целью является одно приложение, в В общем, я хочу использовать контекстные шаблоны, чтобы соответствовать значительно более сложным целям, а затем использовать эти шаблоны для построения функций Галлины. Можно ли это сделать?