Stream: Coq users

Topic: Inductive types and Fixpoint

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.

Li-yao (Jun 06 2022 at 02:31):

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

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 :=
 ...

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: Oct 13 2024 at 01:02 UTC