[ create a new paste ] login | about

Link: http://codepad.org/xKPqBWN2    [ raw code | fork ]

Haskell, pasted on Feb 11:
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)

sucself :  b  suc b  b  suc b  suc b
sucself zero = refl
sucself (suc n) = cong suc (sucself n)

lemma1 :  {a b c}  a  suc b  suc b  c  a  b  a  c
lemma1 .{_} {b} refl refl = sucself 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)


Create a new paste based on this one


Comments: