IteratedTrees.v

Require Import List.
Import ListNotations.

Set Implicit Arguments.
Set Maximal Implicit Insertion.

Module tree.
  Section tree.
    Variable A : Type.

    Local Unset Elimination Schemes.

    Inductive t :=
    | atom : A -> t
    | node : list t -> t
    .

    Section t_rect.
      Variable P : t -> Type.
      Variable P_list : list t -> Type.
      Hypothesis P_atom : forall a, P (atom a).
      Hypothesis P_node : forall l, P_list l -> P (node l).
      Hypothesis P_list_nil : P_list [].
      Hypothesis P_list_cons : forall a l, P a -> P_list l -> P_list (a :: l).

      Fixpoint t_rect (x : t) : P x :=
        let fix go_list (l : list t) : P_list l :=
            match l with
            | [] => P_list_nil
            | x :: l => P_list_cons (t_rect x) (go_list l)
            end
        in
        match x with
        | atom a => P_atom a
        | node l => P_node (go_list l)
        end.
    End t_rect.

    Definition app (x y : t) : t := node [x; y].

  End tree.

  Definition nil {A} : t A := node [].

  Section map.
    Variable A B : Type.
    Variable f : A -> B.

    (* In order to be able to use this function during further recursive definitions,
       (eg, treetree.map below), it is essential that the fixpoint happen *after* the
       function variable has been introduced. We accomplish this by moving `f` into a
       section variable. An alternative would have been to use a `Definition` with a
       local `fix` expression.

       Notice that we can use List.map here without trouble because it is similarly
       carefully defined so that the fix happens after the function variable:

           Print List.map.

           List.map =
           fun (A B : Type) (f : A -> B) =>
           fix map (l : list A) : list B := match l with
                                            | [] => []
                                            | a :: t => f a :: map t
                                            end
                : forall A B : Type, (A -> B) -> list A -> list B
     *)
    Fixpoint map (x : t A) : t B :=
      match x with
      | atom a => atom (f a)
      | node l => node (List.map map l)
      end.
  End map.
  Print tree.map. (* notice the fix happens late: *)
  (*
    tree.map =
    fun (A B : Type) (f : A -> B) =>
    fix map (x : t A) : t B :=
      match x with
      | atom a => atom (f a)
      | node l => node (List.map map l)
      end
         : forall A B : Type, (A -> B) -> t A -> t B
   *)

  Lemma map_app : forall A B (f : A -> B) x y,
      map f (app x y) = app (map f x) (map f y).
  Proof. reflexivity. Qed.
End tree.

Module treetree.
  Section treetree.
    Variable A : Type.

    Local Unset Elimination Schemes.

    Inductive t : Type :=
    | atom : A -> t
    | node : tree.t t -> t
    .

    Section t_rect.
      Variable P : t -> Type.
      Variable P_tree : tree.t t -> Type.
      Variable P_list : list (tree.t t) -> Type.
      Hypothesis P_atom : forall a, P (atom a).
      Hypothesis P_node : forall t, P_tree t -> P (node t).
      Hypothesis P_tree_atom : forall t, P t -> P_tree (tree.atom t).
      Hypothesis P_tree_node : forall l, P_list l -> P_tree (tree.node l).
      Hypothesis P_list_nil : P_list [].
      Hypothesis P_list_cons : forall t l, P_tree t -> P_list l -> P_list (t :: l).

      Fixpoint t_rect (x : t) : P x :=
        let fix go_tree (x : tree.t t) : P_tree x :=
            let fix go_list (l : list (tree.t t)) : P_list l :=
                match l with
                | [] => P_list_nil
                | x :: l => P_list_cons (go_tree x) (go_list l)
                end
            in
            match x with
            | tree.atom t => P_tree_atom (t_rect t)
            | tree.node l => P_tree_node (go_list l)
            end
        in
        match x with
        | atom a => P_atom a
        | node t => P_node (go_tree t)
        end.
    End t_rect.
  End treetree.

  Definition nil {A} : t A := node tree.nil.

  Section map.
    Variable A B : Type.
    Variable f : A -> B.

    Fixpoint map (x : t A) : t B :=
      match x with
      | atom a => atom (f a)
      | node t => node (tree.map map t)
      end.
  End map.
End treetree.