module HeightProperties where

open import Tree
open import BalancedProperty
open import Data.Unit
open import Data.Empty

open import Data.Nat
open import Data.Maybe
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

insertFullTree-height : {A : Set} (a : A) (t : Tree A) → Full t → (1 + height t) ≡ height (insertFullTree a t)
insertFullTree-height a leaf _ = refl
insertFullTree-height a ._ (branch _ t₁ t₂ full₁ _ height-≡) with insertFullTree-height a t₁ full₁
... | eq = cong suc (lemma height-≡ eq)
 where
  lemma : ∀ {a b c} → a ≡ b
                    → 1 + a ≡ c
                    → 1 + (a ⊔ b) ≡ c ⊔ b
  lemma {zero}  refl refl = refl
  lemma {suc a} refl refl = cong suc (lemma {a} refl refl)

suc⊔self : ∀ b → suc b ⊔ b ≡ suc b ⊔ suc b
suc⊔self zero = refl
suc⊔self (suc n) = cong suc (suc⊔self n)

insertTree-height : {A : Set} (a : A) {t : Tree A} → Balanced t → maybe (λ t′ → height t ≡ height t′) ⊤ (insertTree a t)
insertTree-height a leaf = _
insertTree-height a (branchˡ a' t₁ t₂ y y' y0)
  with insertTree a t₁ | insertTree-height a y | insertFullTree-height a t₂ y'
...  | nothing         | _                     | t₂′-height  rewrite sym t₂′-height | y0 = cong suc (suc⊔self (height t₂))
...  | just t₁′        | t₁′-height            | _           rewrite t₁′-height          = refl
insertTree-height a (branchʳ a' t₁ t₂ y y' y0)
  with insertTree a t₂ | insertTree-height a y'
... | nothing          | _                             = _
... | just t₂′         | t₂′-height rewrite t₂′-height = refl