Если у меня есть следующее:
H : some complicated expression = some other complicated expression
и я хочу схватить
u := some other complicated expression
без жесткого кодирования в моем доказательстве (т. е. с использованием pose)
Есть ли чистый способ сделать это в LTac?
Я уверен, что есть другие способы сделать это с помощью ltac, в моем случае я предпочитаю использовать для этого контекстный язык шаблонов SSReflect. (Вам нужно будет установить плагин или использовать Coq >= 8.7, который включает SSReflect):
(* ce_i = complicated expression i *)
Lemma example T (ce_1 ce_2 : T) (H : ce_1 = ce_2) : False.
set u := (X in _ = X) in H.
результирующая цель:
T : Type
ce_1, ce_2 : T
u := ce_2 : T
H : ce_1 = u
============================
False
Обычно вы можете улучшать шаблон все больше и больше, пока не получите довольно стабильное совпадение.
Обратите внимание, что это первый пример раздела 8.3 «Контекстные шаблоны» в руководстве SSReflect.
Вот еще одна версия, в которой используется Ltac и его способность сопоставлять шаблоны по типам терминов:
Tactic Notation "assign" "rhs" "of" ident(H) "to" ident(u) "in" ident(H') :=
match type of H with _ = ?rhs => set (u := rhs) in H' end.
Tactic Notation "assign" "rhs" "of" ident(H) "to" ident(u) "in" "*" :=
match type of H with _ = ?rhs => set (u := rhs) in * end.
Мы можем создать больше вариантов вышеперечисленного (см., например, здесь). Вот как это использовать:
Lemma example {T} (ce1 ce2 ce3 : T) (H1 : ce1 = ce2) (H2 : ce2 = ce3) : ce1 = ce3.
Proof.
assign rhs of H1 to u in *.
Состояние доказательства:
u := ce2 : T
H1 : ce1 = u
H2 : u = ce3
============================
ce1 = ce3
Еще раз:
Undo.
assign rhs of H1 to u in H1.
Состояние доказательства:
u := ce2 : T
H1 : ce1 = u
H2 : ce2 = ce3
============================
ce1 = ce3
