Mercurial > hg > Gears > GearsAgda
changeset 809:243faca58e90
merge
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 21 Jan 2024 12:49:28 +0900 |
| parents | bc75f442d646 (current diff) 5d15ec862bcb (diff) |
| children | 194b5ae1a7a0 |
| files | hoareBinaryTree1.agda |
| diffstat | 2 files changed, 301 insertions(+), 125 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon Nov 13 18:55:58 2023 +0900 +++ b/hoareBinaryTree1.agda Sun Jan 21 12:49:28 2024 +0900 @@ -510,7 +510,7 @@ (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1 (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) - $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ + $ λ tree repl P → {!!} --exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ insertTestP1 = insertTreeP leaf 1 1 t-leaf $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0) @@ -527,6 +527,7 @@ -- deletion? + data Color : Set where Red : Color Black : Color @@ -544,9 +545,30 @@ black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁ black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ ) +zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥ +zero≢suc () +suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ +suc≢zero () +{-# TERMINATING #-} +DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n +DepthCal zero zero zero = refl +DepthCal zero zero (suc n) = ⊥-elim (zero≢suc (DepthCal zero zero (suc n))) +DepthCal zero (suc m) zero = ⊥-elim (zero≢suc (DepthCal zero (suc m) zero)) +DepthCal zero (suc m) (suc n) = ⊥-elim (zero≢suc (DepthCal zero (suc m) (suc n))) +DepthCal (suc l) zero zero = ⊥-elim (suc≢zero (DepthCal (suc l) zero zero )) +DepthCal (suc l) zero (suc n) with <-cmp (suc l) (suc n) +... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) )) +... | tri≈ ¬a b ¬c = cong suc (suc-injective b) +... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) )) +DepthCal (suc l) (suc m) zero with <-cmp (suc l) (suc m) +... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero )) +... | tri≈ ¬a b ¬c = cong suc (suc-injective b) +... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero )) +DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n ) + data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where - rb-leaf : RBtreeInvariant leaf - rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) + rb-leaf : RBtreeInvariant leaf + rb-single : {c : Color} → (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) @@ -555,29 +577,26 @@ → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) - rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ + rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key₁ < key → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf ) - rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} + rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color} → key₁ < key → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf) rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ - → black-depth t₁ ≡ black-depth t₂ + → black-depth (node key ⟪ Black , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) - → black-depth t₃ ≡ black-depth t₄ → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) - rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ + rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {c c₁ : Color} - → black-depth t₁ ≡ black-depth t₂ + → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂) - → black-depth t₃ ≡ black-depth t₄ → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) - data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where rtt-unit : {t : bt A} → rotatedTree t t rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → @@ -605,6 +624,13 @@ → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) + +RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) +RightDown leaf = leaf +RightDown (node key ⟪ c , value ⟫ t1 t2) = t2 +LeftDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) +LeftDown leaf = leaf +LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) @@ -617,11 +643,11 @@ RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til tir) = til +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) @@ -634,31 +660,77 @@ RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til tir) = tir +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) - → treeInvariant tree ∧ stackInvariant key tree tree0 stack - → RBtreeInvariant tree + → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) - → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack - → RBtreeInvariant tree1 + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) - → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack - → RBtreeInvariant tree1 + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t -findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl) -findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁ -findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c - = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left _ _ _ a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1< -findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl) -findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c - = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right _ _ _ c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2< +findRBT key leaf tree0 stack rb0 next exit = exit leaf stack rb0 (case1 refl) +findRBT key (node key₁ value left right) tree0 stack rb0 next exit with <-cmp key key₁ +findRBT key (node key₁ value left right) tree0 stack rb0 next exit | tri< a ¬b ¬c + = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 rb0) , s-left _ _ _ a (_∧_.proj2 rb0) ⟫ depth-1< +findRBT key n tree0 stack rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack rb0 (case2 refl) +findRBT key (node key₁ value left right) tree0 stack rb0 next exit | tri> ¬a ¬b c + = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 rb0), s-right _ _ _ c (_∧_.proj2 rb0) ⟫ depth-2< + + +blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A)) + → RBtreeInvariant tree1 + → RBtreeInvariant tree2 + → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2) + → black-depth tree1 ≡ black-depth tree2 +blackdepth≡ leaf leaf ri1 ri2 rip = refl +blackdepth≡ {n} {A} leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0 +blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3)) +blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0 +blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0 +blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0 +blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4)) (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4)) + + +findTest : {n m : Level} {A : Set n } {t : Set m } + → (key : ℕ) + → (tree0 : bt (Color ∧ A)) + → RBtreeInvariant tree0 + → (exit : (tree1 : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t +findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) + {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫ + $ λ p RBP loop → findRBT k (proj1 p) tr0 (proj2 p) RBP (λ t1 s1 P2 lt1 → loop ⟪ t1 , s1 ⟫ P2 lt1 ) + $ λ tr1 st P2 O → exit tr1 st P2 O + + +testRBTree0 : bt (Color ∧ ℕ) +testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf)) + +record result {n : Level} {A : Set n} {key : ℕ} {tree0 : bt (Color ∧ A)} : Set n where + field + tree : bt (Color ∧ A) + stack : List (bt (Color ∧ A)) + ti : RBtreeInvariant tree + si : stackInvariant key tree tree0 stack + +testRBI0 : RBtreeInvariant testRBTree0 +testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) )) + +findRBTreeTest : result +findRBTreeTest = findTest 14 testRBTree0 testRBI0 + $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) + + + data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where @@ -667,16 +739,7 @@ rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t) rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} - → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) - -RBtreeCopy : {n m : Level} {A : Set n} {t : Set m} {key : ℕ} {value : A} {c : Color} → (tree tree0 : bt (Color ∧ A) ) - → (stack : List (bt (Color ∧ A)) ) - → ( treeInvariant tree ∧ stackInvariant key tree tree0 stack) - → ( next : (tree tree0 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) - → ( treeInvariant tree ∧ stackInvariant key tree tree0 stack ) - → replacedRBTree key value tree0 tree → t ) - → ( exit : (repl : bt (Color ∧ A)) → replacedRBTree key value tree0 repl → t ) → t -RBtreeCopy = ? + → key < k → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } @@ -688,7 +751,7 @@ s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand - +{- record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where field parent grand uncle : bt A @@ -758,18 +821,6 @@ ... | tri≈ ¬a b ¬c = rbi ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi --- findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) --- → (stack : List (bt (Color ∧ A))) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack --- → {d : ℕ} → RBtreeInvariant tree0 --- → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) --- → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack --- → {d1 : ℕ} → RBtreeInvariant tree1 --- → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t ---findRBT {_} {_} {A} {t} key tree0 leaf stack ti {d} rb0 exit = {!!} ---findRBT {_} {_} {A} {t} key tree0 (node key₁ value left right) stack ti {d} rb0 exit with <-cmp key key₁ ---... | tri< a ¬b ¬c = {!!} ---... | tri≈ ¬a b ¬c = {!!} ---... | tri> ¬a ¬b c = {!!} rotateLeft : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) @@ -883,17 +934,6 @@ -- tree is right of parent, parent is right of grand -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) - -- replaced done, clear stack and reconstruct tree - -- we can do this in a codeGear, but to accept context switch during reconstruction, we have to call next - -- this means we have to check prime simple case such as replaced not is exactly the same value / color / key. - insertCase11 : ? - insertCase11 = ? - insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t - insertCase10 leaf eq refl = exit repl stack ? r -- no stack, replace top node - insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁ - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = next ? ? ? ? - ... | tri> ¬a ¬b c = ? insertCase1 : t insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit repl stack eq r -- no stack, replace top node @@ -904,10 +944,10 @@ insertCase12 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → stackInvariant key (RBI.tree r) orig stack → t - insertCase12 leaf eq1 si = ? -- can't happen + insertCase12 leaf eq1 si = {!!} -- can't happen insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr - ... | tri< a ¬b ¬c | cr = ? - ... | tri≈ ¬a b ¬c | cr = ? -- can't happen + ... | tri< a ¬b ¬c | cr = {!!} + ... | tri≈ ¬a b ¬c | cr = {!!} -- can't happen ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where -- -- orig B @@ -916,7 +956,7 @@ -- -- B => B B => B -- / \ / \ / \ rotate L / \ - -- L L0 L R3 L R -- bad B B + -- L L1 L R3 L R -- bad B B -- / \ / \ / \ 1 : child-replace --- L L2 L B L L 2: child-replace ( unbalanced ) -- / \ 3: child-replace ( rotated / balanced ) @@ -941,28 +981,52 @@ ; repl-eq = rb07 } where rb07 : black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl - rb07 = ? - -- rb05 should more general + rb07 with <-cmp key key₁ + ... | tri< a ¬b ¬c = DepthCal (black-depth (left)) (black-depth left) (black-depth repl) + ... | tri≈ ¬a b ¬c = DepthCal (black-depth (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (black-depth left) (black-depth repl) + ... | tri> ¬a ¬b c = DepthCal (black-depth (RBI.rot r)) (black-depth left) (black-depth repl) + + rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} + → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) + → key < key1 + rb09 (rb-right-red x x1 x2) = x + -- rb05 should more general + tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ + tkey (node key value t t2) = key + tkey leaf = {!!} -- key is none + rb051 : {n : Level} {A : Set n} {key key1 : ℕ } {value : A} {t t1 t2 : bt (Color ∧ A)} {c : Color} → replacedRBTree key value (node key1 ⟪ c , value ⟫ t1 t2) (node key1 ⟪ c , value ⟫ t1 t) → key1 < key + rb051 = {!!} + rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁ + rb052 = {!!} rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧ replacedRBTree key value (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl) - rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl - ... | rb-single key₂ value₂ | refl | rb-single key value = ? - ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = ? - ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = ? - ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = ? - ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ? - ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = ? - ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ? - ... | rb-right-black x x₁ t | refl | rb = ? - ... | rb-left-black x x₁ t | refl | rb = ? - ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = ? + rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl | <-cmp key₁ (tkey repl) -- si and ri have key's relation + ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri< a ¬b ¬c = {!!} -- need paternmatch with c + ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique ? + ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri> ¬a ¬b c = ⊥-elim (nat-<> {!!} {!!}) --⊥-elim (¬a (rb052 {!!})) + ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb | t = {!!} -- cant happen ? red - red + ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ leaf (RightDown repl) rb-leaf (RBtreeRightDown leaf (RightDown repl) (RBI.replrb r)) (RBI.replrb r)) (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = Red + ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!} --rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} + ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ({!!} ) + ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red + ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ (LeftDown repl) leaf (RBtreeLeftDown (LeftDown repl) leaf (RBI.replrb r)) rb-leaf (RBI.replrb r)) (RBI.replrb r) , {!!} ⟫ + ... | rb-single key₁ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = ⊥-elim (¬c {!!} ) --(rb09 (RBI.origrb r))) + ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = {!!} + ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb rb₁ | t = {!!} -- red-red + ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri< a ¬b ¬c = {!!} + ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri≈ ¬a b ¬c = {!!} + ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri> ¬a ¬b c = ⊥-elim {!!} + --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫ + --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫ + --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!} insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) - ... | Black = exit ? ? ? ? - ... | Red = exit ? ? ? ? + ... | Black = exit {!!} {!!} {!!} {!!} + ... | Red = exit {!!} {!!} {!!} {!!} -- r = orig RBI.tree b -- / \ => / \ -- b b → r RBI.tree r r = orig o (r/b) ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) +-}
--- a/work.agda Mon Nov 13 18:55:58 2023 +0900 +++ b/work.agda Sun Jan 21 12:49:28 2024 +0900 @@ -16,6 +16,28 @@ open import Relation.Nullary open import logic +zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥ +zero≢suc () +suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ +suc≢zero () +{-# TERMINATING #-} +DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n +DepthCal zero zero zero = refl +DepthCal zero zero (suc n) = ⊥-elim (zero≢suc (DepthCal zero zero (suc n))) +DepthCal zero (suc m) zero = ⊥-elim (zero≢suc (DepthCal zero (suc m) zero)) +DepthCal zero (suc m) (suc n) = ⊥-elim (zero≢suc (DepthCal zero (suc m) (suc n))) +DepthCal (suc l) zero zero = ⊥-elim (suc≢zero (DepthCal (suc l) zero zero )) +DepthCal (suc l) zero (suc n) with <-cmp (suc l) (suc n) +... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) )) +... | tri≈ ¬a b ¬c = cong suc (suc-injective b) +... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) )) +DepthCal (suc l) (suc m) zero with <-cmp (suc l) (suc m) +... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero )) +... | tri≈ ¬a b ¬c = cong suc (suc-injective b) +... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero )) +DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n ) + + data bt {n : Level} (A : Set n) : Set n where leaf : bt A node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A @@ -48,10 +70,12 @@ treeTest2 : bt ℕ treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf) + + testdb : ℕ testdb = bt-depth treeTest1 -- 4 -import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) +import Data.Unit --hiding ( _≟_ ; _≤?_ ; _≤_) data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where t-leaf : treeInvariant leaf @@ -71,6 +95,12 @@ → treeInvariant (node key2 value2 t3 t4) → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4)) +{- +treekey : {n : Level} {A : Set n} → {key key1 : ℕ} {value value1 : A} {t1 t2 : bt A} → treeInvariant (node key value (node key1 value1 t1 t2) leaf) → key1 < key +treekey (t-left x x₁) = x -- normal level +--treekey t-single key value = {!!} +-} + data stackInvariant {n : Level} {A : Set n} (key : ℕ ) : (top orig : bt A) → (stack : List (bt A)) → Set n where s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [] ) @@ -153,6 +183,9 @@ RB→bt {n} A leaf = leaf RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1)) +RBTreeTest : bt (Color ∧ ℕ) +RBTreeTest = node 8 ⟪ Black , 200 ⟫ (node 5 ⟪ Red , 100 ⟫ (_) (_)) (node 10 ⟪ Red , 300 ⟫ (_) (_)) + color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color color leaf = Black color (node key ⟪ C , value ⟫ rb rb₁) = C @@ -162,9 +195,11 @@ black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁ black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ ) + + data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where rb-leaf : RBtreeInvariant leaf - rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) + rb-single : {c : Color} → (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) @@ -173,25 +208,23 @@ → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) - rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ + rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key₁ < key → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf ) - rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} + rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color} → key₁ < key → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf) rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ - → black-depth t₁ ≡ black-depth t₂ + → black-depth (node key ⟪ Black , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) - → black-depth t₃ ≡ black-depth t₄ → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {c c₁ : Color} - → black-depth t₁ ≡ black-depth t₂ + → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂) - → black-depth t₃ ≡ black-depth t₄ → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) @@ -233,11 +266,11 @@ RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til --x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til tir) = til +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) @@ -250,31 +283,42 @@ RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir ) = tir --x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde til tir) = tir +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir + + +blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A)) + → RBtreeInvariant tree1 + → RBtreeInvariant tree2 + → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2) + → black-depth tree1 ≡ black-depth tree2 +blackdepth≡ leaf leaf ri1 ri2 rip = refl +blackdepth≡ {n} {A} leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0 +blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3)) +blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0 +blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0 +blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0 +blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4)) (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4)) findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) - → treeInvariant tree ∧ stackInvariant key tree tree0 stack - → RBtreeInvariant tree + → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) - → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack - → RBtreeInvariant tree1 + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) - → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack - → RBtreeInvariant tree1 + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t -findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl) -findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁ -findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c - = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1< -findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl) -findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c - = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2< +findRBT key leaf tree0 stack inv next exit = exit leaf stack inv (case1 refl) +findRBT key (node key₁ value left right) tree0 stack inv next exit with <-cmp key key₁ +findRBT key (node key₁ value left right) tree0 stack inv next exit | tri< a ¬b ¬c + = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 inv) , s-left a (_∧_.proj2 inv) ⟫ depth-1< +findRBT key n tree0 stack inv _ exit | tri≈ ¬a refl ¬c = exit n stack inv (case2 refl) +findRBT key (node key₁ value left right) tree0 stack inv next exit | tri> ¬a ¬b c + = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 inv) , s-right c (_∧_.proj2 inv) ⟫ depth-2< child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A child-replaced key leaf = leaf @@ -284,6 +328,69 @@ ... | tri> ¬a ¬b c = right +lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ +lemma3 refl () +lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ +lemma5 (s≤s z≤n) () +¬x<x : {x : ℕ} → ¬ (x < x) +¬x<x (s≤s lt) = ¬x<x lt +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ +nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x + +TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) + → (r : Index) → (p : Invraiant r) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t +TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) +open _∧_ +--findRBTree : (exit : ) +add< : { i : ℕ } (j : ℕ ) → i < suc i + j +add< {i} j = begin + suc i ≤⟨ m≤m+n (suc i) j ⟩ + suc i + j ∎ where open ≤-Reasoning + +findTest : {n m : Level} {A : Set n } {t : Set m } + → (key : ℕ) + → (tree0 : bt (Color ∧ A)) + → RBtreeInvariant tree0 + → (exit : (tree1 : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t +findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫ + $ λ p P loop → findRBT k (proj1 p) tr0 (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ tr1 st P2 O → exit tr1 st P2 O + +testRBTree0 : bt (Color ∧ ℕ) +testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf)) +testRBTree : bt (Color ∧ ℕ) +testRBTree = node 10 ⟪ Red , 1000 ⟫ _ _ + +record result {n : Level} {A : Set n} {key : ℕ} {tree0 : bt (Color ∧ A)} : Set n where + field + tree : bt (Color ∧ A) + stack : List (bt (Color ∧ A)) + ti : RBtreeInvariant tree + si : stackInvariant key tree tree0 stack + +testRBI0 : RBtreeInvariant testRBTree0 +testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) )) + +findRBTreeTest : result +findRBTreeTest = findTest 14 testRBTree0 testRBI0 + $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) + + +{- data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf) rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} @@ -332,17 +439,22 @@ ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) ) rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫ -blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key : ℕ} {value : A} → (tree1 tree2 : bt (Color ∧ A)) +blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A)) → RBtreeInvariant tree1 → RBtreeInvariant tree2 → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2) → black-depth tree1 ≡ black-depth tree2 - -blackdepth≡ leaf leaf ri1 ri2 rip = refl -blackdepth≡ leaf (node key value t2 t3) ri1 ri2 rip = {!!} --rip kara mitibiki daseru RBinvariant kara toreruka -blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!} -blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!} +blackdepth≡ leaf leaf ri1 ri2 rip = refl +blackdepth≡ {n} {A} leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0 +blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) +blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0 +blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0 +blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0 +blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4)) (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4)) +rb08 : {n : Level } {A : Set n}{key key1 : ℕ} {value value1 : A} {c c1 : Color} {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} + → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key1 ⟪ c1 , value1 ⟫ t₃ t₄) +rb08 = {!!} {- rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) @@ -355,4 +467,4 @@ rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!} -} - +-}