Mercurial > hg > Members > Moririn
changeset 728:0786c97b4919
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Apr 2023 19:15:34 +0900 |
| parents | fd63d70310c3 |
| children | 5599bd559f3e |
| files | hoareRedBlackTree.agda redBlackTreeTest.agda |
| diffstat | 2 files changed, 0 insertions(+), 1130 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareRedBlackTree.agda Mon Apr 10 19:12:50 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,644 +0,0 @@ - -module hoareRedBlackTree where - - -open import Level renaming (zero to Z ; suc to succ) - -open import Data.Nat hiding (compare) -open import Data.Nat.Properties as NatProp -open import Data.Maybe --- open import Data.Maybe.Properties -open import Data.Empty -open import Data.List -open import Data.Product - -open import Function as F hiding (const) - -open import Relation.Binary -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary -open import logic - - - -record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where - field - putImpl : treeImpl → a → (treeImpl → t) → t - getImpl : treeImpl → (treeImpl → Maybe a → t) → t -open TreeMethods - -record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where - field - tree : treeImpl - treeMethods : TreeMethods {n} {m} {a} {t} treeImpl - putTree : a → (Tree treeImpl → t) → t - putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} )) - getTree : (Tree treeImpl → Maybe a → t) → t - getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d ) - -open Tree - -SingleLinkedStack = List - -emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data -emptySingleLinkedStack = [] - -clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t -clearSingleLinkedStack [] cg = cg [] -clearSingleLinkedStack (x ∷ as) cg = cg [] - -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t -pushSingleLinkedStack stack datum next = next ( datum ∷ stack ) - -popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t -popSingleLinkedStack [] cs = cs [] nothing -popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1) - -data Color {n : Level } : Set n where - Red : Color - Black : Color - -record Node {n : Level } (a : Set n) : Set n where - inductive - field - key : ℕ - value : a - right : Maybe (Node a ) - left : Maybe (Node a ) - color : Color {n} -open Node - -record RedBlackTree {n : Level } (a : Set n) : Set n where - field - root : Maybe (Node a ) - nodeStack : SingleLinkedStack (Node a ) - - -open RedBlackTree - --- record datum {n : Level} (a : Set n) : Set n where --- field --- key : ℕ --- val : a - --- leaf nodes key is 0. --- --- data BTree {n : Level} (a : Set n) (lk nk rk : ℕ) : Set n where --- leaf : (l<n : lk < nk) → BTree a lk nk rk --- node : (left : BTree a lk nk rk) --- → (datum : ℕ) → (right : BTree a lk nk rk) --- → BTree a lk nk rk - - -{-- tree に サイズ比較をつけたい(持ち運びたい)が leaf をどう扱うか問題(0にするとright についたときにおわる) -終わってほしくないので node のときだけにしたいがそれだと根本的に厳しい（BTree a の再帰構造なので） - - ---} - --- data BTree {n : Level} (a : Set n) : Set n where --- leaf : BTree a --- node : (left : BTree a ) --- → (datum : ℕ) --- → (right : BTree a ) --- → BTree a - --- {a b c : ℕ} {a≤b : a ≤ b } {b≤c : b ≤ c} → --- trans≤ : {n : Level} {a : Set n} → Trans {_} {_} {_} {_} {_} {_} {ℕ} {ℕ} {ℕ} (λ x y → x < y) (λ y z → y < z) (λ x z → (x < z)) -- a≤b b≤c --- trans≤ {n} {a} {i} {j} {k} i<j j<k = ≤-trans i<j {!!} --- with i <? k --- trans≤ {n} {a} {i} {j} {k} i<j j<k | yes p = p --- trans≤ {n} {a} {i} {j} {k} i<j j<k | no ¬p = {!!} - - --- data BTree {n : Level} {a : Set n} (p q : ℕ) : ℕ → Set n where --- leaf : (p<q : p ≤ q ) → BTree p q 0 --- node : ∀ {hl hr h : ℕ} --- → (key : ℕ) --- → (left : BTree {n} {a} p key hl ) --- → (right : BTree {n} {a} key q hr ) --- → BTree p q (suc h) - --- leaf-inj : {n : Level} {a : Set n} {p q : ℕ} {pp qq : p ≤ q} --- → (leaf {n} {a} pp) ≡ (leaf qq) → pp ≡ qq --- leaf-inj refl = refl - - - --- node-inj : {n : Level} {a : Set n} --- {k1 k2 h : ℕ} {l1 r1 : BTree {n} {a} h} {l2 r2 : BTree {n} {a} h} --- → ((node {n} {a} {h} l1 k1 r1)) ≡ (node l2 k2 r2) → k1 ≡ k2 --- node-inj refl = refl - --- node-inj1 : {n : Level} {a : Set n} --- {k1 k2 h hl1 hl2 hr1 hr2 p q : ℕ } --- {l1 : BTree {n} {a} p k1 hl1 } {l2 : BTree {n} {a} p k2 hl2} {l1 : BTree {n} {a} k1 q hr1} {r2 : BTree {n} {a} k2 q hr2} --- → (node {n} {a} {h} {?} {?} {?} {!!} {!!} ) ≡ (node {!!} {!!} {!!} ) → k1 ≡ k2 --- node-inj1 as = {!!} - - - ---- add relation find functions --- fTree is start codeGear. findT2 is loop codeGear. --- findT2 : {n m : Level } {a : Set n} {b lk rk kk1 kk2 : ℕ} {t : Set m} --- → (k1<k2 : kk1 ≤ kk2) → BTree {n} {a} b lk rk → (key : ℕ) --- → SingleLinkedStack (BTree {n} {a} b lk rk) --- → ( (lk ≤ rk) → BTree {n} {a} b lk rk → SingleLinkedStack (BTree {n} {a} b lk rk) → t) → t --- findT2 k1<k2 (leaf p<q) key stack cg = cg {!!} (leaf p<q) stack --- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg with <-cmp key1 key --- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri≈ ¬a b ¬c = {!!} --- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri< a ¬b ¬c = {!!} --- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri> ¬a ¬b c = {!!} - --- cg k1<k2 (leaf p<q) stack --- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 lt) key stack cg with <-cmp key1 key --- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 tree@(node rt key1 lt) key stack cg | tri≈ ¬lt eq ¬gt = cg {!!} tree stack --- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri< lt ¬eq ¬gt = {!!} --- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri> ¬lt ¬eq gt = {!!} - - --- fTree : {n m : Level } {a : Set n} {b k1 k2 : ℕ} {t : Set m} --- → BTree {n} {a} b → (key : ℕ) --- → SingleLinkedStack (BTree {n} {a} b) → ( k1 < k2 → BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t --- fTree {n} {m} {a} {b} tree key stack cg = clearSingleLinkedStack stack (λ cstack → findT2 {n} {m} {a} {b} {0} {key} z≤n tree key cstack λ x x₁ x₂ → {!!}) - -{-- -そもそも Tree は 高さを受け取るのではなく 関係だけを持つ -leaf は関係を受け取って tran で (0 < n < m)をつくる ---} - - -{-- 思いつき - Max Hight を持ち運んで必ず規定回数で止まるようにするのはあり…ｎきがする - Tree を作ったあとに 左右の最大 hight を比較して Max にするのは良い - 操作時はMaxが減る。 途中で終わった場合や、値が見つかった場合は - 受け取って Max を減らすだけの関数で既定回数数を減らすだけ - - 関数に持たせる?データに持たせる? - とりあえず関数(Data だと 再帰的な構造上定義が難しい) - ---} - -data BTree {n : Level} {a : Set n} : (hight : ℕ) → Set n where - leaf : {p q h : ℕ } → (p<q : p ≤ q ) → BTree (suc h) - node : { h : ℕ } - → (left : BTree {n} {a} (suc h) ) - → (key : ℕ) - → (right : BTree {n} {a} (suc h) ) - → BTree h - -maxHight : {n m : Level} {a : Set n} {t : Set m} {h : ℕ} → (searchHight : ℕ) → (BTree {n} {a} h) → ℕ -maxHight {n} {m} {a} {t} zero (leaf p<q) = 0 -- root is leaf -maxHight {n} {m} {a} {t} (suc hi) (leaf p<q) = (suc hi) -- max -maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) with (maxHight {n} {m} {a} {t} hi tree₁) | (maxHight {n} {m} {a} {t} hi tree₂) -... | lh | rh with <-cmp lh rh -maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri< a₁ ¬b ¬c = rh -maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri≈ ¬a b ¬c = lh -maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri> ¬a ¬b c = lh --- maxHight {n} {m} {a} {t} hi (rnode tree₁ key₁ tree₂) = {!!} - - -LastNodeIsLeaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool -LastNodeIsLeaf h (leaf p<q) P = true -LastNodeIsLeaf h (node rt k1 lt) P = (P rt k1 lt) /\ LastNodeIsLeaf (suc h) lt (λ _ z _ → P lt z lt) /\ LastNodeIsLeaf (suc h) rt λ _ z _ → P lt z lt - --- allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool --- allnodes leafEx p = true --- allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p - --- MaxHightStop? : {n : Level} {a : Set n} → {h : ℕ} → (hight : ℕ) → (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool --- MaxHightStop? {n} {a} {.(suc _)} zero (leaf p<q) P = true --- MaxHightStop? {n} {a} {.(suc _)} (suc allh) (leaf p<q) P = false --- MaxHightStop? {n} {a} {h} zero (node lt k rt) P = false --- MaxHightStop? {n} {a} {h} (suc allh) (node lt k rt) P = (P lt k lt) /\ (MaxHightStop? allh lt λ _ z _ → ) /\ (MaxHightStop? allh rt λ _ z _ → P rt z rt) - - -SearchLeaf : {n : Level} {a : Set n} → (h : ℕ) → (t : BTree {n} {a} h) → Bool -SearchLeaf h tree = LastNodeIsLeaf h tree (λ l k r → LastNodeIsLeaf (suc h) l (λ _ j _ → j <B? k) /\ LastNodeIsLeaf (suc h) r (λ _ n _ → k <B? n)) - - -{-- whats leaf relation...? -i think keys relation... -"leaf relation" maybe 0<"parent node key" ??? ---} -test : {n : Level} {a : Set n} {h : ℕ} → BTree {n} {a} h -test {n} {a} {h} = (node (leaf {n} {a} {0} {2} z≤n) 2 (node (leaf {n} {a} {0} {3} z≤n) 3 (leaf {n} {a} {0} {3} z≤n))) - -c : {n : Level} {a : Set n} → Bool -c {n} {a} = SearchLeaf {n} {a} 3 test - -cm : {n : Level} {a : Set n} → ℕ -cm {n} {a} = maxHight {n} {n} {a} {a} {zero} {!!} test - -lemma-all-leaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → SearchLeaf h tree ≡ true -lemma-all-leaf .(suc _) (leaf p<q) = refl -lemma-all-leaf h tt@(node pltree k1 rtree) = {!!} -- lemma-all-leaf h tt --- lemma-all-leaf .0 tt@(rnode ltree k1 rtree) = lemma-all-leaf zero tt - -findT : {n m : Level } {a : Set n} {b left current : ℕ} {t : Set m} - → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ) - → SingleLinkedStack (BTree {n} {a} b) - → (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t -findT = {!!} - --- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st --- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1 --- findT l<c (node tree₁ key1 tree₂) key st cg | tri< a ¬b ¬c = {!!} --- findT l<c (node tree₁ key1 tree₂) key st cg | tri≈ ¬a b ¬c = {!!} --- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬a ¬b c = {!!} --- -- findT l<c tree@(node ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st --- findT {n} {m} {a} {b} {l} {cu} {?} l<c tree@(node {b} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = ? --- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {l} {cu} {!!} ({!!}) key st2 cg) --- findT の {!!} の部分は trans したやつが入ってほしい(型が合わない) - - ---- nomal find --- findT : {n m : Level } {a : Set n} {b left current : ℕ} {t : Set m} --- → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ) --- → SingleLinkedStack (BTree {n} {a} b) --- → (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t - --- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st --- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1 --- findT l<c tree@(node ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st - --- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node (leaf p<q) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → {!!}) -- findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} (leaf {n} {a} ⦃ !! ⦄ {cu} {!!}) key st2 cg) - --- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltt@(node ltree key₁ ltree₁) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} {!!} key st2 cg) - --- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {key} {key1} {!!} (rtree) key st2 cg) - - --- findT l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st - --- findT {n} {m} {a} {b} {l} l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = {!!} -- pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {lh} {rh} {h} {!!} ({!!}) key {!!} λ x x₁ → {!!}) --- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬lt ¬eq gt = {!!} --- findT (leaf p<q) key st cg = cg (leaf p<q ) st --- findT (node tree₁ key₁ tree₂) key st cg with <-cmp key key₁ --- findT tree@(node tree₁ key₁ tree₂) key st cg | tri≈ ¬a b ¬c = cg tree st --- findT tree@(node tree₁ key₁ tree₂) key st cg | tri< a ¬b ¬c = {!!} --- findT tree@(node tree₁ key₁ tree₂) key st cg | tri> ¬a ¬b c = {!!} - - -data BTreeEx {n : Level} {a : Set n} : Set n where - leafEx : BTreeEx - nodeEx :(left : BTreeEx {n} {a} ) - → (key : ℕ) - → (right : BTreeEx {n} {a} ) - → BTreeEx - - -cmpMax : ℕ → ℕ → ℕ -cmpMax lh rh with <-cmp lh rh -cmpMax lh rh | tri< a ¬b ¬c = rh -cmpMax lh rh | tri≈ ¬a b ¬c = lh -cmpMax lh rh | tri> ¬a ¬b c₁ = lh - - -max1 : {n m : Level} {a : Set n} {t : Set m} → ℕ → (BTreeEx {n} {a}) → (ℕ → t) → t -max1 {n} {m} {a} {t} hi leafEx cg = cg hi -max1 {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg = (max1 {n} {m} {a} {t} (suc hi) tree₁ - (λ lh → (max1 {n} {m} {a} {t} (suc hi) tree₂ (λ rh → cg (cmpMax lh rh))) )) - - -max : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → (ℕ → t) → t -max {n} {m} {a} {t} tree = max1 zero tree - - -maxI : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ℕ -maxI {n} {m} {a} {t} tree = max tree (λ x → x) - --- bad proof --- isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max 0 tr (λ n → n ≡ n)) --- isStopMax? leafEx = refl --- isStopMax? (nodeEx tree₁ key₁ tree₂) = {!!} - -isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max tr (λ eq → eq ≡ eq)) -isStopMax? leafEx = refl -isStopMax? (nodeEx tree₁ key₁ tree₂) = max (nodeEx tree₁ key₁ tree₂) (λ n₁ → {!!}) - -ltreeSearchLeaf : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ((BTreeEx {n} {a}) → t) → t -ltreeSearchLeaf leafEx cg = cg leafEx -ltreeSearchLeaf (nodeEx tree₁ key₁ tree₂) cg = ltreeSearchLeaf tree₁ cg - -ltreeStop? : {n m : Level} {a : Set n} {t : Set m} → (tree : BTreeEx {n} {a}) → ltreeSearchLeaf tree (λ tt → tt ≡ tt) -ltreeStop? leafEx = refl -ltreeStop? {n} {m} {a} {t} (nodeEx tree₁ key₁ tree₂) = ltreeStop? {n} {m} {a} {t} tree₁ - -ltreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t -ltreeSearchNode key leafEx cg = cg leafEx -ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁ -ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = ltreeSearchNode key tree₁ cg -ltreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt -ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = cg tree₂ - - - - --- 何らかの集合のサイズが減っていれば良い…？ -ltreeStoplem : {n m : Level} {a : Set n} {t : Set m} - → (key : ℕ) → (lt : BTreeEx {n} {a}) → (key1 : ℕ) → (rt : BTreeEx {n} {a}) → (p<q : key < key1 ) - → (ℕ → BTreeEx {n} {a} → t ) → t - -ltreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → ltreeSearchNode key tree (λ tt → tt ≡ tt) -ltreeNodeStop? key leafEx = refl -ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁ -ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = {!!} - --- ltreeNodeStop? {!!} {!!} -{-- -Failed to solve the following constraints: -[720] ltreeSearchNode ?4 ?5 (λ tt → tt ≡ tt) -=< ltreeSearchNode key tree₁ (λ tt → tt ≡ tt) -: Set n ---} -ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl -ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = refl - - - --- rtreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t --- rtreeSearchNode key leafEx cg = cg leafEx --- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁ --- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = cg tree₂ --- rtreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt --- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = rtreeSearchNode key tree₁ cg - - --- rtreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → rtreeSearchNode key tree (λ tt → tt ≡ tt) --- rtreeNodeStop? key leafEx = refl --- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁ --- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = refl --- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl --- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = rtreeNodeStop? key {!!} - - -ltreeStoplem key lt key1 rt p<q cg = cg key (nodeEx lt key1 rt) - - - - --- with (max {n} {m} {a} {t} (suc hi) tree₁ cg) | (max {n} {m} {a} {t} (suc hi) tree₂ cg) --- ... | lh | rh = {!!} - --- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri< a₁ ¬b ¬c = cg rh --- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri≈ ¬a b ¬c = cg lh --- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri> ¬a ¬b c = cg lh - - --- findStop : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t --- findStop = {!!} - -findTEx : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t -findTEx leafEx sd st next = next leafEx st -findTEx (nodeEx ltree datum rtree) sd st next with <-cmp sd datum -findTEx tree@(nodeEx ltree datum rtree) sd st next | tri≈ ¬a b ¬c = next tree st -findTEx tree@(nodeEx ltree datum rtree) sd st next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findTEx ltree sd st2 next) -findTEx tree@(nodeEx ltree datum rtree) sd st next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findTEx rtree sd st2 next) - -findL : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t -findL leafEx key stack cg = cg leafEx stack -findL (nodeEx tree₁ key1 tree₂) key stack cg with (key1 ≤? key) -findL (nodeEx tree₁ key1 tree₂) key stack cg | yes p with key1 ≟ key -findL tree@(nodeEx tree₁ key1 tree₂) key stack cg | yes p | yes p₁ = cg tree stack -findL tree@(nodeEx ltree key1 tree₂) key stack cg | yes p | no ¬p = pushSingleLinkedStack stack tree (λ stack1 → findL ltree key stack1 cg) -findL (nodeEx tree₁ key1 tree₂) key stack cg | no ¬p = cg leafEx stack - - - -allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool -allnodes leafEx p = true -allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p - -find-leaf : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → Bool -find-leaf tree = allnodes tree (λ l k r → allnodes l (λ _ j _ → j <B? k) /\ allnodes r (λ _ n _ → k <B? n)) - -testTree : {n : Level} {a : Set n} → BTreeEx {n} {a} -testTree {n} {a} = (nodeEx (nodeEx leafEx 1 leafEx) 2 (nodeEx leafEx 3 (nodeEx (nodeEx leafEx 4 leafEx) 5 (nodeEx leafEx 6 leafEx)))) - -badTree : {n : Level} {a : Set n} → BTreeEx {n} {a} -badTree {n} {a} = (nodeEx (nodeEx leafEx 3 leafEx) 2 leafEx) - - - -lemm : {n : Level} {a : Set n} → find-leaf {n} {a} testTree ≡ true -lemm = refl - - -bool-⊥ : true ≡ false → ⊥ -bool-⊥ () - -{-- badTree --} --- lemm1 : {n : level} {a : set n} → find-leaf {n} {a} badtree ≡ true --- lemm1 {n} {a} with badtree --- lemm1 {n} {a} | leafex = {!!} --- lemm1 {n} {a} | nodeex gda key₁ gda₁ = {!!} - --- lemm-all : {n : Level} {a : Set n} (any-tree : BTreeEx {n} {a}) → find-leaf {n} {a} any-tree ≡ true --- lemm-all leafEx = refl --- lemm-all t@(nodeEx ltree k rtree) with (find-leaf t) ≟B true --- lemm-all (nodeEx ltree k rtree) | yes p = p --- lemm-all (nodeEx ltree k rtree) | no ¬p = {!!} - --- findT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} {a} → (key : ℕ) → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t --- findT = ? - --- {-- --- 一旦の方針は hight を使って書く, 大小関係 (片方だけ) を持って証明しながら降りてく --- --} - - --- hoge = findTEx testTree 44 [] (λ t s → s) - --- {-- --- Tree に対して l < x < r の条件を足すときに気になるのは l or r が leaf の場合 --- leaf のときだけ例外的な証明を書く必要ありそう --- --} - - --- {-- AVL Tree メモ --- - $AGDA-HOME/Data/AVL.agda 関連を眺めた Tips --- AVL は特徴として すべての枝の長さの差が1以内に収まっている木。バランスもできる。 - --- AVL Tree には key , value , left right の他にkeyの 上限、下限、高さを持ってるらしい --- (後ろに付いてるのは高さ+- 1 の関係をもってる) - --- cast operation は木のサイズの log になる --- (cast operation は… わすれた) - --- insert では 同じ key の値があったら Node を置き換え - - --- --} - --- -- findT testTreeType 44 [] (λ t st → t) --- -- leaf - --- -- findT testTree 44 [] (λ t st → st) --- -- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ [] - - --- -- findT testTreeType 3 [] (λ t st → t) --- -- node leaf 3 leaf - --- -- findT testTreeType 3 [] (λ t st → st) --- -- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ [] - - --- replaceT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t --- replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf) --- replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree - --- replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next - - --- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum --- replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c = replaceT tree n0 rstack next --- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next --- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c = replaceT (node x datum (node leaf n0 leaf)) n0 rstack next - - - --- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next - --- -- bad some code --- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum --- replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next --- | tri≈ ¬a b ¬c = replaceT tree n0 rstack next --- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next --- | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next --- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next --- | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next - --- insertT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t --- insertT tree n0 st next = findT tree n0 st ( λ new st2 → replaceT new n0 st2 next ) - - --- c1 : {n : Level} {a : Set n} → BTree {n} a --- c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t)))) - --- c2 : {n : Level} {a : Set n} → BTree {n} a --- c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t)))) - --- -- -- 末 --- -- findDownEnd : {n m : Level} {a : Set n} {t : Set m} → (find : ℕ) → (any : BTree a) → findT any find [] (λ tt stack → {!!}) --- -- findDownEnd d tree = {!!} - --- find-insert : {n m : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (key ≡ {!!}))) --- find-insert leaf key with <-cmp key key --- find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a ) --- find-insert leaf key | tri≈ ¬a b ¬c = {!!} --- find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c ) --- find-insert tr@(node any₁ datum any₂) key with <-cmp key datum --- find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!} --- find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!} --- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum --- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!} --- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!} --- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!} - --- -- where --- find-lemma : {n m : Level} {a : Set n} {t : Set m} → BTree a → ℕ → SingleLinkedStack (BTree a) → (BTree a → SingleLinkedStack (BTree a) → t) → t --- find-lemma leaf ke st nt = nt leaf st --- find-lemma (node tr datum tr₁) ke st nt with <-cmp ke datum --- find-lemma tt@(node tr datum tr₁) ke st nt | tri< a ¬b ¬c = find-lemma tr ke (tt ∷ st) nt --- find-lemma tt@(node tr datum tr₁) ke st nt | tri≈ ¬a b ¬c = nt tt st --- find-lemma tt@(node tr datum tr₁) ke st nt | tri> ¬a ¬b c = find-lemma tr₁ ke (tt ∷ st) nt - ----- --- find node potition to insert or to delete, the path will be in the stack --- - -{-# TERMINATING #-} -findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t -findNode {n} {m} {a} {t} tree n0 next with root tree -findNode {n} {m} {a} {t} tree n0 next | nothing = next tree -findNode {n} {m} {a} {t} tree n0 next | just x with <-cmp (key x) (key n0) -findNode {n} {m} {a} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree -findNode {n} {m} {a} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next) -findNode {n} {m} {a} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next) - - - -findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t -findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) - module FindNode where - findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t - findNode2 nothing st = next record { root = nothing ; nodeStack = st } - findNode2 (just x) st with <-cmp (key n0) (key x) - ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) - ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1) - ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1) - -node001 : Node ℕ -node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black } -node002 : Node ℕ -node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black } -node003 : Node ℕ -node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black } - -tes0t01 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } ) - node001 ( λ tree → tree ) -test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } ) - node001 ( λ tree → tree ) -test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } ) - node001 ( λ tree → tree ) -test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } ) - node001 ( λ tree → tree ) - -replaceNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t -replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } ) - module FindNodeR where - replaceNode1 : (Maybe (Node a )) → Node a - replaceNode1 nothing = record n0 { left = nothing ; right = nothing } - replaceNode1 (just x) = record n0 { left = left x ; right = right x } - replaceNode2 : SingleLinkedStack (Node a ) → (Node a → t) → t - replaceNode2 [] next = next ( replaceNode1 (root tree) ) - replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0) - replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) ) - replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) ) - replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) ) - -insertNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t -insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next ) - -createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ) - → RedBlackTree {n} a -createEmptyRedBlackTreeℕ a b = record { - root = nothing - ; nodeStack = emptySingleLinkedStack - } - -findNodeLeft : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n -findNodeLeft x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing ) -findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h)) -- stack の top と比較するのはたぶん replace ...? - -findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n -findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing ) -findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h)) - -data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (node : Maybe (Node a) ) → Set n where - fni-stackEmpty : (now : Maybe (Node a) ) → FindNodeInvariant [] now - fni-treeEmpty : (st : SingleLinkedStack (Node a)) → FindNodeInvariant st nothing - fni-Left : (x : Node a) (st : SingleLinkedStack (Node a)) (node : Maybe (Node a )) - → FindNodeInvariant ( x ∷ st ) node → findNodeLeft x st → FindNodeInvariant st node - fni-Right : (x : Node a) (st : SingleLinkedStack (Node a)) (node : Maybe (Node a )) - → FindNodeInvariant ( x ∷ st ) node → findNodeRight x st → FindNodeInvariant st node -findNodeLoop : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n -findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st)) - -findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) - → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) (root new ) → t ) - → ( FindNodeInvariant (nodeStack tree) (root tree) ) → t -findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev - module FindNodeH where - findNode2h : (new : Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s new → t - findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } prev - findNode2h (just x) st prev with <-cmp (key n0) (key x) - ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) prev - ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 {!!} {!!} {!!}) ) - ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 {!!} {!!} {!!}) ) - - --- replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t --- replaceNodeH = {!!}
--- a/redBlackTreeTest.agda Mon Apr 10 19:12:50 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,486 +0,0 @@ -module redBlackTreeTest where - -open import Level hiding (zero) renaming ( suc to succ ) - -open import Data.Empty -open import Data.List -open import Data.Maybe -open import Data.Bool -open import Data.Nat -open import Data.Nat.Properties as NatProp - -open import Relation.Nullary -open import Relation.Binary - -open import Algebra - -open import RedBlackTree -open import stack - -open Tree -open Node -open RedBlackTree.RedBlackTree -open Stack - --- tests - -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 import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Function - - --- check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool --- check1 nothing _ = false --- check1 (just n) x with Data.Nat.compare (value n) x --- ... | equal _ = true --- ... | _ = false - -check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool -check2 nothing _ = false -check2 (just n) x with compare2 (value n) x -... | EQ = true -... | _ = false - -test1 : {m : Level} {A B C : Set} → putTree1 {Level.zero} {succ Level.zero} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ {!!} {!!} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true )) -test1 = {!!} - --- test2 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( --- λ t → putTree1 t 2 2 ( --- λ t → getRedBlackTree t 1 ( --- λ t x → check2 {m} x 1 ≡ true ))) --- test2 = refl - --- open ≡-Reasoning --- test3 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 --- $ λ t → putTree1 t 2 2 --- $ λ t → putTree1 t 3 3 --- $ λ t → putTree1 t 4 4 --- $ λ t → getRedBlackTree t 1 --- $ λ t x → check2 {m} x 1 ≡ true --- test3 {m} = begin --- check2 {m} (just (record {key = 1 ; value = 1 ; color = Black ; left = nothing ; right = just (leafNode 2 2)})) 1 --- ≡⟨ refl ⟩ --- true --- ∎ - --- test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 --- $ λ t → putTree1 t 2 2 --- $ λ t → putTree1 t 3 3 --- $ λ t → putTree1 t 4 4 --- $ λ t → getRedBlackTree t 4 --- $ λ t x → x - --- -- test5 : Maybe (Node ℕ ℕ) --- test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 --- $ λ t → putTree1 t 6 6 --- $ λ t0 → clearSingleLinkedStack (nodeStack t0) --- $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) --- $ λ t1 s n1 → replaceNode t1 s n1 --- $ λ t → getRedBlackTree t 3 --- -- $ λ t x → SingleLinkedStack.top (stack s) --- -- $ λ t x → n1 --- $ λ t x → root t --- where --- findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t --- findNode1 t s n1 nothing next = next t s n1 --- findNode1 t s n1 ( just n2 ) next = findNode t s n1 n2 next - --- -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → --- -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ just (record { key = 1; value = 1; left = just (record { key = 2 ; value = 2 } ); right = nothing} ) --- -- test51 = refl - --- test6 : Maybe (Node ℕ ℕ) --- test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) - - --- test7 : Maybe (Node ℕ ℕ) --- test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) --- where --- tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} --- k1 = 1 --- n2 = leafNode 0 0 --- value1 = 1 - --- test8 : Maybe (Node ℕ ℕ) --- test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 --- $ λ t → putTree1 t 2 2 (λ t → root t) - - --- test9 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true )) --- test9 = refl - --- test10 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( --- λ t → putRedBlackTree t 2 2 ( --- λ t → getRedBlackTree t 1 ( --- λ t x → check2 {m} x 1 ≡ true ))) --- test10 = refl - --- test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 --- $ λ t → putRedBlackTree t 2 2 --- $ λ t → putRedBlackTree t 3 3 --- $ λ t → getRedBlackTree t 2 --- $ λ t x → root t - - -compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y ) -compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) - where open import Relation.Binary - -checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool -checkT nothing _ = false -checkT (just n) x with compTri (value n) x -... | tri≈ _ _ _ = true -... | _ = false - -checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (just n) x ≡ true -checkEQ x n refl with compTri (value n) x -... | tri≈ _ refl _ = refl -... | tri> _ neq gt = ⊥-elim (neq refl) -... | tri< lt neq _ = ⊥-elim (neq refl) - --- checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq --- checkEQ' x y refl with x ≟ y --- ... | yes refl = refl --- ... | no neq = ⊥-elim ( neq refl ) - ---- search -> checkEQ ---- findNode -> search - -redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} {A B C : Set Level.zero } → RedBlackTree {Level.zero} {m} {t} {A} {B} {C} a ℕ -redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; nodeComp = λ x x₁ → {!!} } -- record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compTri } - - -open stack.SingleLinkedStack -open stack.Element - - -insertP : { a : Set } { t : Set } {P : Set } → ( f : ( a → t ) → t ) ( g : a → t ) ( g' : P → a → t ) - → ( p : P ) - → ( g ≡ g' p ) - → f ( λ x → g' p x ) ≡ f ( λ x → g x ) -insertP f g g' p refl = refl - - -{-# TERMINATING #-} -inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool -inStack {l} n s with ( top s ) -... | nothing = true -... | just n1 with compTri (key n) (key (datum n1)) -... | tri> _ neq _ = inStack {l} n ( record { top = next n1 } ) -... | tri< _ neq _ = inStack {l} n ( record { top = next n1 } ) -... | tri≈ _ refl _ = false - -record StackTreeInvariant ( n : Node ℕ ℕ ) -<<<<<<< working copy - ( s : SingleLinkedStack (Node ℕ ℕ) ) : Set where -||||||| base - ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where -======= - ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where ->>>>>>> destination - field -<<<<<<< working copy - -- sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True) - notInStack : inStack n s ≡ True → ⊥ -||||||| base - sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True) - notInStack : inStack n s ≡ True → ⊥ -======= - sti : {m : Level} → replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT {m} x1 (value n) ≡ true) - notInStack : {m : Level} → inStack {m} n s ≡ true → ⊥ ->>>>>>> destination - -open StackTreeInvariant - -<<<<<<< working copy -putTest1 : (n : Maybe (Node ℕ ℕ)) - → (k : ℕ) (x : ℕ) - → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) -putTest1 n k x with n -... | Just n1 = lemma0 - where - tree0 : (n1 : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ - tree0 n1 s = record { root = Just n1 ; nodeStack = s ; compare = compareT } - lemma2 : (n1 : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s - → findNode (tree0 n1 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))) - lemma2 n1 s STI with compTri k (key n1) - ... | tri> le eq gt with (right n1) - ... | Just rightNode = {!!} -- ( lemma2 rightNode ( record { top = Just ( cons n1 (top s) ) } ) (record {notInStack = {!!} } ) ) - ... | Nothing with compTri k k - ... | tri≈ _ refl _ = {!!} - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - lemma2 n1 s STI | tri< le eq gt = {!!} - lemma2 n1 s STI | tri≈ le refl gt = lemma5 s ( tree0 n1 s ) n1 - where - lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } ) - ( \ s1 _ -> (replaceNode (tree0 n1 s1) s1 (record n1 { key = k ; value = x } ) (λ t → - GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) ) - lemma5 s t n with (top s) - ... | Just n2 with compTri k k - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - ... | tri≈ _ refl _ = ⊥-elim ( (notInStack STI) {!!} ) - lemma5 s t n | Nothing with compTri k k - ... | tri≈ _ refl _ = checkEQ x _ refl - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 n1 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))) - lemma0 = lemma2 n1 (record {top = Nothing}) ( record { notInStack = {!!} } ) -... | 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 → compareT x₁ y } ) k - ( λ t x1 → checkT x1 x ≡ True) - lemma1 with compTri k k - ... | tri≈ _ refl _ = checkEQ x _ refl - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) -||||||| base -putTest1 : (n : Maybe (Node ℕ ℕ)) - → (k : ℕ) (x : ℕ) - → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) -putTest1 n k x with n -... | Just n1 = lemma0 - where - tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ - tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT } - lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s) - → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))) - lemma2 s STI with compTri k (key n1) - ... | tri≈ le refl gt = lemma5 s ( tree0 s ) n1 - where - lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } ) - ( \ s1 _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → - GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) ) - lemma5 s t n with (top s) - ... | Just n2 with compTri k k - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - ... | tri≈ _ refl _ = ⊥-elim ( (notInStack STI) {!!} ) - lemma5 s t n | Nothing with compTri k k - ... | tri≈ _ refl _ = checkEQ x _ refl - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) - ... | tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!} } ) - ... | tri< le eq gt = {!!} - lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 - (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))) - lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!} ; notInStack = {!!} } ) -... | 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 → compareT x₁ y } ) k - ( λ t x1 → checkT x1 x ≡ True) - lemma1 with compTri k k - ... | tri≈ _ refl _ = checkEQ x _ refl - ... | tri< _ neq _ = ⊥-elim (neq refl) - ... | tri> _ neq _ = ⊥-elim (neq refl) -======= - --- testn : {!!} --- testn = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 --- $ λ t → putTree1 t 1 1 --- $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta }) - - --- List と Node で書こうとしたがなんだかんだListに直したほうが楽そうだった - -nullNode = (record {key = 0 ; value = 0 ; right = nothing ; left = nothing ; color = Red}) - --- treeTotal : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → (List ℕ → t) → t --- treeTotal {m} {t} s tr next with (left tr) | (right tr) --- treeTotal {m} {t} s tr next | nothing | nothing = next ((key tr) ∷ []) --- treeTotal {m} {t} s tr next | nothing | just x = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li)) --- treeTotal {m} {t} s tr next | just x | nothing = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li)) --- treeTotal {m} {t} s tr next | just x | just x₁ = treeTotal {m} {t} s x (λ li1 → treeTotal {m} {t} s x₁ (λ li2 → next (s ++ li1 ++ li2))) -treeTotal : { n m : Level } {a : Set n} {t : Set m} → ( s : List a ) → ( tr : (Node a a) ) → List a -treeTotal {n} {m} {a} {t} s tr with (left tr) | (right tr) -treeTotal {n} {m} {a} {t} s tr | nothing | nothing = (key tr) ∷ [] -treeTotal {n} {m} {a} {t} s tr | nothing | just x = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x) -treeTotal {n} {m} {a} {t} s tr | just x | nothing = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x) -treeTotal {n} {m} {a} {t} s tr | just x | just x₁ = s ++ ((key tr) ∷ (treeTotal {n} {m} {a} {t} s x) ++ (treeTotal {n} {m} {a} {t} s x₁)) - - --- treeTotalA : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → List ℕ - --- (treeTotal {_} {ℕ} ([]) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} testn 5 5 {!!})))) - --- exput : (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ ℕ))) (λ total → {!!})) ≡ {!!} --- exput = {!!} - - --- aaa = (treeTotal {_} {_} {ℕ} {_} (5 ∷ []) ((record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }))) - - --- fuga = putTree1 {_} {_} {ℕ} {ℕ} (record {root = just (record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }) ; nodeStack = ( record {top = nothing}) ; compare = (λ x x₁ → EQ) }) 5 5 (λ aaa → aaa ) - --- nontree ++ 2 :: [] - --- piyo = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 ( λ t1 → findNode t1 (record {top = nothing}) (leafNode 2 2) (Data.Maybe.fromMaybe nullNode (root t1)) (λ tree stack node → {!!})) - - --- exn2l : {!!} ≡ (treeTotal {_} {ℕ} ([]) (putTree1 {_} {_} {ℕ} {ℕ} {!!} 5 5 (λ t → {!!}))) -- (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root testn))) --- exn2l = refl - - - - - --- record FS {n m : Level } {a : Set n} {t : Set m} (oldTotal : List a) ( s : List a ) ( tr : (Node a a) ) : Set where --- field --- total : treeTotal {n} {m} {a} {t} s tr ≡ oldTotal --- -- usage = FS.total -- relation - --- data P { n m : Level } { t : Set m } : Set where --- P₀ : (old : List ℕ) ( s : List ℕ ) → (tr : (Node ℕ ℕ) ) → FS {m} {t} old s tr → P - - - --- ttt = putTree1 {_} {_} {ℕ} {ℕ} - --- record TreeInterface {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set n where --- field --- tree : treeImpl --- list : List ℕ --- node : Node ℕ ℕ --- putTreeHoare : (FS {_} {ℕ} list list node) → putTree1 {!!} {!!} {!!} {!!} - -stack2list : {n m : Level} {t : Set m} {a : Set n} → (s : SingleLinkedStack a) → List a -stack2list stack with top stack -stack2list stack | just x = (datum x) ∷ (elm2list {_} {_} {ℕ} x) - where - elm2list : {n m : Level} {t : Set m} {a : Set n} → (elm : (Element a)) → List a - elm2list el with next el - elm2list el | just x = (datum el) ∷ (elm2list {_} {_} {ℕ} x) - elm2list el | nothing = (datum el) ∷ [] -stack2list stack | nothing = [] - - --- list2element : {n m : Level} {t : Set m} {a : Set n} → (l : List a) → Maybe (Element a) --- list2element [] = nothing --- list2element (x ∷ l) = just (cons x (list2element {_} {_} {ℕ} l)) - --- ltest = list2element (1 ∷ 2 ∷ 3 ∷ []) - -list2stack : {n m : Level} {t : Set m} {a : Set n} {st : SingleLinkedStack a} → (l : List a) → SingleLinkedStack a -list2stack {n} {m} {t} {a} {s} (x ∷ l) = pushSingleLinkedStack s x (λ s1 → list2stack {n} {m} {t} {a} {s1} l ) -list2stack {n} {m} {t} {a} {s} [] = s - - - --- stest = list2stack (1 ∷ 2 ∷ 3 ∷ []) - -open Node - -exfind : { m : Level } { t : Set m} → (dt : ℕ) → (node : (Node ℕ ℕ)) → (st : List ℕ) → findNode {_} {_} {ℕ} {ℕ} (redBlackInSomeState ℕ (just node)) (emptySingleLinkedStack) (leafNode dt dt) (node) (λ t1 st1 n1 → (( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ≡ ( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) )) -exfind dt node st with left node | right node -exfind dt node st | just x | just x₁ = {!!} -exfind dt node st | just x | nothing = {!!} -exfind dt node st | nothing | just x = {!!} -exfind dt node st | nothing | nothing with (compTri dt (key node)) -exfind dt node st | nothing | nothing | tri< a ¬b ¬c = {!!} -exfind dt node st | nothing | nothing | tri≈ ¬a b ¬c = {!!} -exfind dt node st | nothing | nothing | tri> ¬a ¬b c = {!!} - --- exput : (ni : ℕ) → (tn : Node ℕ ℕ) → (ts : List ℕ) → (treeTotal {_} {ℕ} (ni ∷ ts) tn) --- ≡ (treeTotal {_} {ℕ} (ts) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} (record { root = just tn } ) ni ni (λ tt → tt))))) --- exput datum node [] with (right node) | (left node) --- exput datum node [] | nothing | nothing = {!!} --- exput datum node [] | just x | just x₁ = {!!} --- exput datum node [] | just x | nothing = {!!} --- exput datum node [] | nothing | just x = {!!} --- exput datum node (x ∷ stack₁) = {!!} - - --- proofTree : {n m : Level} {t : Set m} {a : Set n} (old stackl : List ℕ) → (node : Node ℕ ℕ) → (FS {_} {ℕ} old stackl node) → (tree : RedBlackTree ℕ ℕ) → (key : ℕ) → findNode {{!!}} {{!!}} {{!!}} {{!!}} tree (list2stack {!!} (record {top = nothing})) (leafNode key key) node (λ tree1 stack1 datum → {!!}) --- -- -- -- putTree1 tree key key (λ t → (FS {_} {ℕ} old stackl (Data.Maybe.fromMaybe nullNode (root tree))) ) --- proofTree old stack node fs t k = {!!} - --- FS は 証明そのものになると思ってたけど実は違いそう --- oldTotal と 現在の node, stack の組み合わせを比較する --- oldTotal はどうやって作る? >< --- treeTotal は list と node を受け取って それの total を出すのでそれで作る(list に put するデータなどを入れることで適当に作れる) - --- p : {n m : Level} {t : Set m} {a : Set n} → ( s : SingleLinkedStack ℕ ) ( tr : (Node ℕ ℕ) ) ( tree : RedBlackTree ℕ ℕ ) (k : ℕ) → (FS (treeTotal (k ∷ (stack2list s)) tr) (stack2list s) tr) → putTree1 tree k k (λ atree → FS (treeTotal (stack2list s) (Data.Maybe.fromMaybe (tr) (root atree))) {!!} {!!}) --- p stack node tree key = {!!} - --- tt = (FS {_} {ℕ} [] [] (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ {_} ℕ {ℕ})))) - --- ttt : (a : P) → P --- ttt a = P₀ {!!} {!!} (record { key = {!!} ; value = {!!} ; right = {!!} ; left = {!!} ; color = {!!} }) (record { total = {!!} }) - - --- FS では stack tree をあわせた整合性を示したい --- そのためには...? --- stack は前の node (というか一段上)が入ってる --- tree は現在の node がある - - - -- tr(Node ℕ ℕ) s (List (Node)) - -- 3 [] - -- / \ - -- 2 5 - -- / / \ - -- 1 4 6 - - -- search 6 (6 > 3) - -- tr(Node ℕ ℕ) s (List (Node)) - -- 5 just (node (1 2 nothing) 3 (4 5 6) - -- / \ [] - -- 4 6 - --- search 6 (6 > 5) --- tr(Node ℕ ℕ) s (List (Node)) --- 6 just (node (4 5 6)) --- just (node (1 2 nothing) 3 (4 5 6) --- [] - --- just 6 → true みたいな感じ - --- stack に node ごと入れるのは間違い…？ --- 一応非破壊な感じがする(新しく作り直してる) --- どう釣り合いをとるか - --- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t --- stack+tree {n} stack mid org = st stack mid org where --- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ) --- st [] _ _ = nothing --- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org) --- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org --- st (x ∷ []) n n1 | _ | _ = nothing --- st (x ∷ a) n n1 with st a n n1 --- st (x ∷ a) n n1 | just x₁ = {!!} --- st (x ∷ a) n n1 | nothing = nothing - - --- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t --- stack+tree {n} stack mid org cg = st stack mid org --- where --- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ) --- st [] _ _ = nothing --- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org) --- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org --- st (x ∷ []) n n1 | _ | _ = nothing --- st (x ∷ a) n n1 with st a n n1 --- st (x ∷ a) n n1 | just x₁ = {!!} --- st (x ∷ a) n n1 | nothing = nothing - --- findNodePush : {n : Level} → (stack : List (Node ℕ ℕ)) → (mid : Node ℕ ℕ) → (org : Node ℕ ℕ) → stack+tree stack mid org ≡ just ? --- → ? {return (? ∷ stack),mid'} → stack+tree (? ∷ stack) (mid') org ≡ just ? --- findNodePush - --- stack+tree が just だって言えたらよい --- {}2 は orig の どっちかのNode - ->>>>>>> destination