Mercurial > hg > Papers > 2018 > ryokka-thesis
view final_main/src/AgdaTreeProof.agda @ 4:12204a2c2eda
add .pdf and some section.
author | ryokka |
---|---|
date | Sun, 18 Feb 2018 21:43:41 +0900 |
parents | 2155c6ff589f |
children | eafc166804f3 |
line wrap: on
line source
module AgdaTreeProof where open import RedBlackTree open import stack open import Level hiding (zero) open import Data.Nat open Tree open Node open RedBlackTree.RedBlackTree open Stack open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import Function check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} check1 Nothing _ = False check1 (Just n) x with Data.Nat.compare (value n) x ... | equal _ = True ... | _ = False check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} check2 Nothing _ = False check2 (Just n) x with compare2 (value n) x ... | EQ = True ... | _ = False putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next)) open ≡-Reasoning redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ putTest1Lemma2 zero = refl putTest1Lemma2 (suc k) = putTest1Lemma2 k putTest1Lemma1 : (x y : ℕ) -> compareℕ x y ≡ compare2 x y putTest1Lemma1 zero zero = refl putTest1Lemma1 (suc m) zero = refl putTest1Lemma1 zero (suc n) = refl putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m where lemma1 : (m : ℕ) -> LT ≡ compare2 m (ℕ.suc (m + k)) lemma1 zero = refl lemma1 (suc y) = lemma1 y putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m where lemma1 : (m : ℕ) -> EQ ≡ compare2 m m lemma1 zero = refl lemma1 (suc y) = lemma1 y putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m where lemma1 : (m : ℕ) -> GT ≡ compare2 (ℕ.suc (m + k)) m lemma1 zero = refl lemma1 (suc y) = lemma1 y putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) compareLemma1 : {x y : ℕ} -> compare2 x y ≡ EQ -> x ≡ y compareLemma1 {zero} {zero} refl = refl compareLemma1 {zero} {suc _} () compareLemma1 {suc _} {zero} () compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) ) where lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y lemma2 = refl putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) -> (k : ℕ) (x : ℕ) -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True)) putTest1 n k x with n ... | Just n1 = lemma2 ( record { top = Nothing } ) where lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) lemma2 s with compare2 k (key n1) ... | EQ = lemma3 {!!} where lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) lemma3 eq with compare2 x x | putTest1Lemma2 x ... | EQ | refl with compare2 k (key n1) | eq ... | EQ | refl with compare2 x x | putTest1Lemma2 x ... | EQ | refl = refl ... | GT = {!!} ... | LT = {!!} ... | Nothing = lemma1 where lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) lemma1 with compare2 k k | putTest1Lemma2 k ... | EQ | refl with compare2 x x | putTest1Lemma2 x ... | EQ | refl = refl