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)
lemma1 : ∀ {a b c} → a ≡ suc b → suc b ≡ c → a ⊔ b ≡ a ⊔ c
lemma1 .{_} {b} refl refl = suc⊔self b
lemma2 : ∀ {a b c} → a ≡ b → a ⊔ c ≡ b ⊔ c
lemma2 refl = refl
lemma3 : ∀ {a b c} → b ≡ c → a ⊔ b ≡ a ⊔ c
lemma3 refl = refl
insertTree-height : {A : Set} (a : A) (t : Tree A) → Balanced t → maybe (λ t′ → height t ≡ height t′) ⊤ (insertTree a t)
insertTree-height a .leaf leaf = _
insertTree-height a .(branch left a' t₁ t₂) (branchˡ a' t₁ t₂ y y' y0)
with insertTree a t₁ | insertTree-height a t₁ y | insertFullTree-height a t₂ y'
... | nothing | _ | t₂′-height = cong suc (lemma1 y0 t₂′-height)
... | just t₁′ | t₁′-height | _ = cong suc (lemma2 t₁′-height)
insertTree-height a .(branch right a' t₁ t₂) (branchʳ a' t₁ t₂ y y' y0)
with insertTree a t₂ | insertTree-height a t₂ y'
... | nothing | _ = _
... | just t₂′ | t₂′-height = cong suc (lemma3 {height t₁} t₂′-height)