如何定义一个与函数互为递归的归纳类型？

Question

我想定义一个归纳类型 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. 这样的相互递归是否可能？

Answer 1

这种类型的定义被称为 "归纳-递归"。不幸的是，Coq中不支持它，但如果我没有记错的话，Agda定理prover中是支持的。