在coq中，destruct https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic65策略有一个接受“连接析取引入模式”的变体，该模式允许用户为引入的变量分配名称，即使在解包复杂的归纳类型时也是如此。
coq 中的 Ltac 语言允许用户编写自定义策略。我想写（事实上，维护）一种策略，在将控制权交给之前做一些事情destruct.
我希望我的自定义策略允许（或要求，以更容易者为准）用户提供我的策略可以提供的介绍模式destruct.
什么 Ltac 语法可以实现此目的？
您可以使用策略符号，如参考手册 https://coq.inria.fr/distrib/current/refman/Reference-Manual014.html#sec558。例如，
Tactic Notation "foo" simple_intropattern(bar) :=
match goal with
| H : ?A /\ ?B |- _ =>
destruct H as bar
end.
Goal True /\ True /\ True -> True.
intros. foo (HA & HB & HC).
The simple_intropattern指令指示 Coq 进行解释bar作为介绍模式。因此，调用foo结果调用destruct H as (HA & HB & HC).
这是一个更长的示例，显示了更复杂的引入模式。
Tactic Notation "my_destruct" hyp(H) "as" simple_intropattern(pattern) :=
destruct H as pattern.
Inductive wondrous : nat -> Prop :=
| one : wondrous 1
| half : forall n k : nat, n = 2 * k -> wondrous k -> wondrous n
| triple_one : forall n k : nat, 3 * n + 1 = k -> wondrous k -> wondrous n.
Lemma oneness : forall n : nat, n = 0 \/ wondrous n.
Proof.
intro n.
induction n as [ | n IH_n ].
(* n = 0 *)
left. reflexivity.
(* n <> 0 *)
right. my_destruct IH_n as
[ H_n_zero
| [
| n' k H_half H_wondrous_k
| n' k H_triple_one H_wondrous_k ] ].
Admitted.
我们可以检查生成的目标之一以查看名称的使用情况。
oneness < Show 4.
subgoal 4 is:
n : nat
n' : nat
k : nat
H_triple_one : 3 * n' + 1 = k
H_wondrous_k : wondrous k
============================
wondrous (S n')
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
