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.
That sounds like induction-recursion, which is not supported in Coq.
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 := ...
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 01 2023 at 18:01 UTC