Что делает ключевое слово `with` без` match` внутри индуктивного типа в Coq?

Question

Что делает ключевое слово with без match внутри индуктивного типа в 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 и, похоже, его неттип блока или что-то ... Так какой смысл определять его внутри другого индуктивного типа, а не сам по себе.По крайней мере, проверка типа Statement дает Set такой же, как для Block ...

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 является совершенно другим ключевым словом, чем with из выражений match.На самом деле они принадлежат двум разным языкам: первый является частью народного , тогда как последний является частью Gallina .