Stream: Coq users

Topic: Inductive types and Fixpoint


view this post on Zulip Adrián García (Jun 06 2022 at 02:24):

I know that is possible to create mutually defined inductive types like tree and forest:

Parameters A B : Set.

Inductive tree : Set := node : A -> forest -> tree

with forest : Set :=
| leaf : B -> forest
| cons : tree -> forest -> forest.

is it possible to do something like that but using a fixpoint? For example:

Inductive Foo: Type :=
 | cons1 : Foo
 | cons2 : forall A B, fxpnt A B -> Foo

with fxpnt A B : Prop :=
 ...

I need to try that because the fxpnt definition depends on the inductive and the other way around.

view this post on Zulip Li-yao (Jun 06 2022 at 02:31):

That sounds like induction-recursion, which is not supported in Coq.

view this post on Zulip Meven Lennon-Bertrand (Jun 07 2022 at 08:05):

One way to cheat your way out of this is to replace the fixpoint by an indexed inductive definition (basically, its graph). You lose computation, but this you can do in Coq.

Inductive Foo: Type :=
 | cons1 : Foo
 | cons2 : forall A B T, fxpnt A B T -> Foo

with fxpnt A B : Type -> Prop :=
 ...

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 09:13):

that depends on how the fixpoint dependes on Foo
for instance if A or B is in Foo you need induction-induction


Last updated: Jan 28 2023 at 06:30 UTC