时间戳

首页 > 解决方案 > 在 Coq 的归纳类型中，没有 `match` 的 `with` 关键字有什么作用？

coq - 在 Coq 的归纳类型中，没有 `match` 的 `with` 关键字有什么作用？

问题描述

在 Coq 的归纳类型中没有 do的with关键字是什么？，例如：match

Inductive Block : Type :=
  | EmptyBlk : Block
  | Blk : Statement -> Block
with Statement : Type :=
  | Assignment : string -> AExp -> Statement
  | Seq : Statement -> Statement -> Statement
  | IfElse : BExp -> Block -> Block -> Statement
  | While : BExp -> Block -> Statement.

我尝试检查的类型，Statement它似乎不是类型块或其他东西......那么在另一个归纳类型中定义它而不是单独定义它有什么意义。至少检查 Statement 的类型给 Set 与 Block 相同...

标签： coq

解决方案

它用于指定相互递归的定义。例如，考虑以下两个函数：

Fixpoint even (n : nat) : bool :=
  match n with
  | O => true
  | S n => odd n
  end
with odd (n : nat) : bool :=
  match n with
  | O => false
  | S n => even n
  end.

在这里，您不能even先定义，因为它需要odd定义。您也不能odd先定义，因为它需要even. 您需要能够同时定义两者-您可以通过使用with关键字来做到这一点。

您的示例类似，但在其定义和用途中定义了归纳数据类型而不是递归函数 -Statement使用。因此，同时定义它们。BlockBlockStatementwith

请注意，这是与表达式with完全不同的关键字。事实上，它们属于两种不同的语言：前者是Vernacular的一部分，而后者是Gallina的一部分。withmatch

推荐阅读