codepad
[
create a new paste
]
login
|
about
Language:
C
C++
D
Haskell
Lua
OCaml
PHP
Perl
Plain Text
Python
Ruby
Scheme
Tcl
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)
Private
[
?
]
Run code
Submit