open import Data.Sum
open import Data.Nat
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- plain (unindexed) trees
data Tree (α : Set) : Set where
  Empty  : Tree α
  Branch : Tree α → α → Tree α → Tree α

max : ℕ → ℕ → ℕ
max zero r = r
max r zero = r
max (suc l) (suc r) = suc (max l r)

depth : ∀ {α} → Tree α → ℕ
depth Empty = zero
depth (Branch t x t₁) = suc (max (depth t) (depth t₁))

-- depth-indexed trees
data DTree (α : Set) : ℕ → Set where
  Empty : DTree α zero
  Branch : ∀ {x y : ℕ} → DTree α x → α → DTree α y →
           DTree α (suc (max x y))

-- convert an unindexed tree to an indexed tree
-- (unlike the GADT version we don't need existential wrapping)
dify : ∀{α} → (t : Tree α) → DTree α (depth t)
dify Empty = Empty
dify (Branch t x t₁) = Branch (dify t) x (dify t₁)


-- perfectly-balanced trees as a depth-indexed inductive type
data GTree (α : Set) : ℕ → Set where
  Empty : GTree α zero
  TreeG : ∀ {n} → GTree α n → α → GTree α n → GTree α (suc n)

-- perfectly-balanced trees defined recursively
gtree : Set → ℕ → Set
gtree α zero = ⊤
gtree α (suc n) = gtree α n × α × gtree α n

-- swivel on inductively-defined trees
Swivel : ∀ {α n} → GTree α n → GTree α n
Swivel Empty = Empty
Swivel (TreeG t x t₁) = TreeG (Swivel t₁) x (Swivel t)

-- swivel on recursively-defined trees, matching on the index (depth)
swivel : ∀ {α n} → gtree α n → gtree α n
swivel {α} {zero} t = tt
swivel {α} {suc n} (l , x , r) = swivel r , (x , swivel l)

-- swivel on unindexed trees
swivel' : ∀ {α} → Tree α → Tree α
swivel' Empty = Empty
swivel' (Branch t x t₁) = Branch (swivel' t₁) x (swivel' t)


{- external verification: unindexed definitions, separate proofs -}

-- max is commutative
max-comm  : ∀ {m n} → (max m n) ≡ (max n m)
max-comm {zero} {zero} = refl
max-comm {zero} {suc n} = refl
max-comm {suc m} {zero} = refl
max-comm {suc m} {suc n}  with max-comm {m} {n }
...                  |    foo = cong suc foo


-- max(m,n) is either m or n
max-either : ∀ {m n o} → (max m n ≡ o) → (o ≡ m) ⊎ (o ≡ n)
max-either {zero} {n} refl = inj₂ refl
max-either {suc m} {zero} refl = inj₁ refl
max-either {suc m} {suc n} refl with max-either {m} {n} refl
max-either {suc m} {suc n} refl | inj₁ x = inj₁ (cong suc x)
max-either {suc m} {suc n} refl | inj₂ y = inj₂ (cong suc y)

-- swivel on unindexed trees is depth-preserving
swiv-depth : ∀ {α} → (t : Tree α) → depth t ≡ depth (swivel' t)
swiv-depth Empty = refl
swiv-depth (Branch t x t₁)
  with swiv-depth t | swiv-depth t₁
...  |     y          |      z =  
     let eq₁ = cong₂ max y z in
     let eq₂ = trans eq₁ (max-comm {depth (swivel' t)} {depth (swivel' t₁)}) in
     cong suc eq₂