\import Data.List
\import Equiv
\import Paths
\import Paths.Meta

\data Tree : \Set
  | leaf (n : Nat)
  | node (t : List Tree) \with {
    | nil => leaf 0
    | leaf n :: nil => leaf (suc n)
  }

\func tsuc (a : Tree) => node (a :: nil)

\func add (a b : Tree): Tree \elim b
  | leaf 0 => a
  | leaf (suc n) => tsuc (add a (leaf n))
  | node (n :: nil) => tsuc (add a n)
  | node (n :: n' :: ns) => node (add_list a (n :: n' :: ns))
  \where {
    \func add_list (a : Tree) (b : List Tree) : List Tree \elim b
      | nil => nil
      | b :: bs => add a b :: add_list a bs
  }

\func add-assoc {a b c : Tree} : add a (add b c) = add (add a b) c \elim c
  | leaf 0 => idp
  | leaf (suc n) => pmap tsuc add-assoc
  | node (n :: nil) => pmap tsuc add-assoc
  | node (n :: n' :: ns) => rewrite (add-assoc, add-assoc, add_list-assoc) idp
  \where {
    \func add_list-assoc {a b : Tree} {cs : List Tree}
      : add.add_list a (add.add_list b cs) = add.add_list (add a b) cs \elim cs
      | nil => idp
      | c :: cs => pmap2 (::) add-assoc add_list-assoc
  }


\data Tree'
  | node' (List Tree')

\func zro' : Tree' => node' nil

\func suc' (n : Tree') : Tree' => node' (n :: nil)

\func add' (a b : Tree') : Tree' \elim b
  | node' nil => a
  | node' bs => node' (add_list' a bs)
  \where {
    \func add_list' (a : Tree') (b : List Tree') : List Tree' \elim b
      | nil => nil
      | b :: bs => add' a b :: add_list' a bs
  }

\func Tree_to_Tree' (t : Tree) : Tree' \elim t
  | leaf 0 => zro'
  | leaf (suc n) => suc' (Tree_to_Tree' (leaf n))
  | node (t :: nil) => suc' (Tree_to_Tree' t)
  | node (t :: t' :: ts) => node' (mut_list (t :: t' :: ts))
  \where {
    \func mut_list (ts : List Tree) : List Tree' \elim ts
      | nil => nil
      | t :: ts => Tree_to_Tree' t :: mut_list ts

    \func eq (t : Tree) : Tree'_to_Tree (Tree_to_Tree' t) = t \elim t
      | leaf 0 => idp
      | leaf (suc n) => rewrite eq idp
      | node (t :: nil) => rewrite eq idp
      | node (t :: t' :: ts) => rewrite (eq, eq, mut_list-eq) idp

    \func mut_list-eq (ts : List Tree) : Tree'_to_Tree.mut_list (mut_list ts) = ts \elim ts
      | nil => idp
      | _ :: _ => rewrite (eq, mut_list-eq) idp
  }

\func Tree'_to_Tree (t : Tree') : Tree \elim t
  | node' ts => node (mut_list ts)
  \where {
    \func mut_list (ts : List Tree') : List Tree \elim ts
      | nil => nil
      | t :: ts => Tree'_to_Tree t :: mut_list ts

    \func eq (t : Tree') : Tree_to_Tree' (Tree'_to_Tree t) = t \elim t
      | node' nil => idp
      | node' (t :: nil) => rewrite eq idp
      | node' (t :: t' :: ns) => rewrite (eq, eq, mut_list-eq) idp

    \func mut_list-eq (ts : List Tree') : Tree_to_Tree'.mut_list (mut_list ts) = ts \elim ts
      | nil => idp
      | _ :: _ => rewrite (eq, mut_list-eq) idp
  }

\func Tree-eq : QEquiv {Tree} {Tree'} \cowith
  | f => Tree_to_Tree'
  | ret => Tree'_to_Tree
  | ret_f => Tree_to_Tree'.eq
  | f_sec => Tree'_to_Tree.eq


\func add-preserved (a b : Tree) : add' (Tree_to_Tree' a) (Tree_to_Tree' b) = Tree_to_Tree' (add a b) \elim b
  | leaf 0 => idp
  | leaf (suc n) => rewrite add-preserved idp
  | node (b :: nil) => rewrite add-preserved idp
  | node (b :: b' :: bs) => rewrite (add-preserved, add-preserved, add_list-preserved) idp
  \where {
    \func add_list-preserved (a : Tree) (bs : List Tree)
      : add'.add_list' (Tree_to_Tree' a) (Tree_to_Tree'.mut_list bs) = Tree_to_Tree'.mut_list (add.add_list a bs) \elim bs
      | nil => idp
      | b :: bs => rewrite (add-preserved, add_list-preserved) idp
  }

\func add'-assoc {a b c : Tree'} : add' a (add' b c) = add' (add' a b) c \elim c
  | node' nil => idp
  | node' (c :: cs) => rewrite (add'-assoc, add_list'-assoc) idp
  \where {
    \func add_list'-assoc (a b : Tree') (cs : List Tree') : add'.add_list' a (add'.add_list' b cs) = add'.add_list' (add' a b) cs \elim cs
      | nil => idp
      | c :: cs => rewrite (add'-assoc, add_list'-assoc) idp
  }

\func add-assoc' {a b c : Tree} : add a (add b c) = add (add a b) c
  => rewriteI (Tree-eq.ret_f, add-preserved, add-preserved) (rewrite (add'-assoc, add-preserved, add-preserved, Tree-eq.ret_f) idp)