文章/答案/技术大牛

发布

社区首页 >问答首页 >我怎么写那些表现得像“毁灭.一样”的战术？

问我怎么写那些表现得像“毁灭.一样”的战术？
EN

Stack Overflow用户

提问于 2015-05-09 00:38:11

回答 1查看 973关注 0票数 8

在coq中，destruct策略有一个变体，它接受一种“连接分离引入模式”，允许用户为引入的变量指定名称，即使在解压复杂的归纳类型时也是如此。

coq中的Ltac语言允许用户编写自定义策略。我想写(事实上，保持)一种在将控制权交给destruct之前做一些事情的策略。

我希望我的自定义策略允许(或要求，无论哪个更容易)用户提供一个介绍模式，我的策略可以交给destruct。

Ltac语法实现了这一点吗？

coq

ltac

回答 1

Stack Overflow用户

回答已采纳

发布于 2015-05-11 02:55:40

您可以使用在参考手册中描述的战术符号。例如,

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).

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')

票数 7

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/30134754

复制

相似问题

问我怎么写那些表现得像“毁灭.一样”的战术？
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问我怎么写那些表现得像“毁灭.一样”的战术？EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问我怎么写那些表现得像“毁灭.一样”的战术？
EN