没有“匹配”的“with”关键字在Coq的归纳类型中有什么作用

Question

没有

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

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的类型，似乎它不是块类型或其他东西......那么在另一种归纳类型中定义它而不是单独定义它有什么意义呢？至少检查语句的类型会给出与块相同的设置...

Answer 1

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

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在其定义中使用Block，Block使用Statement。因此，with同时定义它们。

请注意，此with与match表达式with关键字完全不同。事实上，它们属于两种不同的语言：前者是白话的一部分，而后者是加利纳语的一部分。