Agda

module ind$1$ where

open import lib

open import ntree

thm$1$ : $($n : $)->$ list$-$any iszero $($repeat n $1)$ ff

thm$1=\{!!\}$

treeMapId : $($t : Tree$)->$ treeMap $(\backslash$lambda x $->$ x$)$ t $$ t

treeMapId $=\{!!\}$

$--$ mirroring a tree twice gives you back the original tree

mirror$-$mirror : $($t : Tree$)->$ mirror $($mirror t$)$ t

mirror$-$mirror $=\{!!\}$

$--$ The number of leaves in a perfect tree of height n is $2$ to the n$.$

$--$

$--$ I found I needed the $+0$ theorem from nat$-$thms$.$agda

perfect$-$numLeaves : $($n : $)->$ numLeaves $($perfect n$)2$ pow n

perfect$-$numLeaves $=\{!!\}$

$--$ the size of a perfect binary tree of depth n is $(2$ to the $($n$+1))$ minus $1$

$--$

$--$ I needed $+0,+$suc

perfect$-$size : $($n : $)->$ suc $($size $($perfect n$))2$ pow $($suc n$)$

perfect$-$size $=\{!!\}$

$--$ simple Tree type storing natural numbers

data Tree : Set where

Node : $->$ Tree $->$ Tree $->$ Tree

Leaf : Tree

$--$ a few functions on trees, used in problems in some of the ind$*$agda files

$--$ flip left and right subtrees throughout a tree

mirror : Tree $->$ Tree

mirror $($Node x t$1$ t$2)=$ Node x $($mirror t$2)($mirror t$1)$

mirror Leaf $=$ Leaf

$--$ construct the perfect binary tree whose depth is the input number

perfect : $->$ Tree

perfect zero $=$ Leaf

perfect $($suc n$)=$ Node $1($perfect n$)($perfect n$)$

$--$ count the number of leaves in a tree

numLeaves : Tree $->$

numLeaves $($Node x t t$\text{'})=$ numLeaves t $+$ numLeaves t$\text{'}$

numLeaves Leaf $=1$

$--$ count the number of constructors $($either Leaf or Node$)$ in a Tree

size : Tree $->$

size $($Node x t t$\text{'})=1+$ size t $+$ size t$\text{'}$

size Leaf $=1$

$--$ apply a function to every number stored in a tree, returning the resulting tree

treeMap : $(->)->$ Tree $->$ Tree

treeMap f Leaf $=$ Leaf

treeMap f $($Node x t t$\text{'})=$ Node $($f x$)($treeMap f t$)($treeMap f t$\text{'})$