Defining sigma-labelled ranked trees and unranked trees

tree.v

Module FiniteRankedTree.
Inductive Forest {A : Set} {sigma : A -> nat} : nat -> Set :=
  | leaf : Forest O
  | sibl : RankedTree -> forall n, Forest n -> Forest (S n)
with
RankedTree {A : Set} {sigma : A -> nat} : Set := node : forall a, Forest (sigma a) -> RankedTree.
End FiniteRankedTree.

Module RankedTree.
Require Import List.
CoInductive Forest {A : Set} {sigma : A -> nat} : nat -> Set :=
  | leaf : Forest O
  | sibl : RankedTree -> forall n, Forest n -> Forest (S n)
with
RankedTree {A : Set} {sigma : A -> nat} : Set := node : forall a, Forest (sigma a) -> RankedTree.

Fail Fixpoint to_list {A : Set} {s : A -> nat} {n : nat} (f : Forest (sigma:=s) n) : list (RankedTree (sigma:=s)) :=
  match f with
  | leaf => nil
  | sibl t _ f' => t :: to_list f'
  end.

Fail Fixpoint child {A : Set} {sigma : A -> nat} (t : RankedTree (sigma:=sigma)) (i: nat) :=
match t with
| node a f => (fix child' j g :=
  match g with
  | leaf => None
  | sibl t _ h =>
    match j with
    | 0 => Some t
    | S k => child' k h
    end
  end) i f
end.

End RankedTree.

Check RankedTree.node.

Module Tree.
Set Implicit Arguments.
Set Contextual Implicit.
(*Set Reversible Pattern Implicit.*)
Inductive Forest (T : Set): nat -> Set :=
  | leaf : Forest T O
  | sibl (_ : T) {n : nat} : Forest T n -> Forest T (S n).
(*
Arguments leaf {T}.
About leaf.
Arguments sibl {T} _ {n} _.
About sibl.
*)
CoInductive RankedTree {A : Set} (sigma : A -> nat) : Set := node : forall a, Forest (RankedTree sigma) (sigma a) -> RankedTree sigma.
(*
Arguments node {A sigma} a _.
About node.
*)
CoInductive UnrankedTree {A : Set} (sigma : A -> nat) : Set := unode :  A -> list (UnrankedTree sigma) -> UnrankedTree sigma.
About UnrankedTree.
About unode.
Require Import List.
About RankedTree.
Definition children {A : Set} {sigma : A -> nat} (t : RankedTree sigma) : list (RankedTree sigma) :=
match t with
| node a f => (fix to_list {n : nat} (g : Forest (RankedTree sigma) n) := match g with
  | leaf => nil
  | sibl t _ h => t :: to_list h
  end) _ f
end.
End Tree.

Section Test1.
Import Tree.
Let id_nat := fun x:nat => x.
Check (sibl (node (sigma:=id_nat) 0 leaf) leaf).
Check (sibl (node 0 leaf) (sibl (node (sigma:=id_nat) 0 leaf) leaf)).
Let t1 := node (sigma:=id_nat) 1 (sibl (node 0 leaf) leaf).
Let t2 := node (sigma:=id_nat) 2 (sibl (node 0 leaf) (sibl (node (sigma:=id_nat) 0 leaf) leaf)).
Eval compute in (children t2).

Check (node 0 leaf : RankedTree id_nat).

CoFixpoint x : RankedTree id_nat := (node 1 (sibl x leaf)).
Fail CoFixpoint x : RankedTree id_nat := (node 2 (sibl x leaf)).

End Test1.

Section Test2.
Import RankedTree.
Let id_nat := fun x:nat => x.
Let t1 := node (sigma:=id_nat) 1 (sibl (node 0 leaf) 0 leaf).
Check t1.

End Test2.