如何定义与函数相互递归的归纳类型？答案

【问题标题】：How to define an inductive type mutually recursive with a function?如何定义与函数相互递归的归纳类型？
【发布时间】：2020-08-11 02:44:21
【问题描述】：

我想定义一个归纳类型Foo，构造函数接受一些属性作为参数。我希望这些属性依赖于我当前定义的类型的归纳参数。我希望能够使用一些递归函数bar 在这些属性中从它们那里收集一些数据，该函数将采用Foo 类型的对象。但是，我不知道如何声明这两个以便 Coq 接受它们的定义。我希望能够写出这样的东西：

Inductive Foo : Set (* or Type *) :=
| Foo1 : forall f : Foo, bar f = 1 -> Foo
| Foo2 : forall f : Foo,  bar f = 2 -> Foo
| Foon : nat -> Foo
with bar (f : Foo) : nat := 
  match f with
  | Foo1 _ _ => 1
  | Foo2 _ _ => 2
  | Foon n => S n
  end.

通常，with 是处理相互递归的方式，但是我看到的所有示例都是它与两个定义一起使用，要么以 Inductive 开头，要么以 Fixpoint 开头。这样的相互递归甚至可能吗？

【问题讨论】：

最坏的情况是最坏的情况，我认为你总是可以“重铸”像bar 这样的函数的用法，用Inductive 表示它的图形。不过，为了这个目的，这种翻译可能有点矫枉过正。

标签： coq induction mutual-recursion

【解决方案1】：

这种类型的定义称为“归纳递归”。不幸的是，它在 Coq 中不受支持，但如果我没记错的话，它在 Agda 定理证明器中得到支持。

【讨论】：