Как определить индуктивный тип, взаимно рекурсивный с функцией?

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, но, если я не ошибаюсь, поддерживается в программе проверки теорем Агды.