Mercurial > hg > Gears > GearsAgda
view work.agda @ 842:ee2dd920e414
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 21 Mar 2024 15:25:37 +0900 |
parents | 858655384dea |
children |
line wrap: on
line source
module work where open import Level hiding (suc ; zero ; _⊔_ ) 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 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 node-key : {n : Level}{A : Set n} → bt A → Maybe ℕ node-key leaf = nothing node-key (node key value tree tree₁) = just key node-value : {n : Level} {A : Set n} → bt A → Maybe A node-value leaf = nothing node-value (node key value tree tree₁) = just value bt-depth : {n : Level} {A : Set n} → (tree : bt A) → ℕ bt-depth leaf = 0 bt-depth (node key value tree tree₁) = suc (bt-depth tree ⊔ bt-depth tree₁) --一番下のleaf =0から戻るたびにsucをしていく treeTest1 : bt ℕ treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)) -- 0 0 -- / \ -- leaf 3 1 -- / \ -- 2 5 2 -- / \ -- 1 leaf 3 -- / \ -- leaf leaf 4 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 ( _≟_ ; _≤?_ ; _≤_) data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where t-leaf : treeInvariant leaf t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf) t-left : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1 → treeInvariant (node key value t1 t2) → treeInvariant (node key1 value1 (node key value t1 t2) leaf) t-right : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1 → treeInvariant (node key1 value1 t1 t2) → treeInvariant (node key value leaf (node key1 value1 t1 t2)) t-node : {key key1 key2 : ℕ}→ {value value1 value2 : A} → {t1 t2 t3 t4 : bt A} → key1 < key → key < key2 → treeInvariant (node key1 value1 t1 t2) → 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 ∷ [] ) s-right : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)} → key1 < key → stackInvariant key (node key1 value t1 t2) tree0 st → stackInvariant key t2 tree0 (t2 ∷ st) s-left : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)} → key < key1 → stackInvariant key (node key1 value t1 t2) tree0 st → stackInvariant key t1 tree0 (t1 ∷ st) data replacedTree {n : Level } {A : Set n} (key : ℕ) (value : A) : (before after : bt A) → Set n where r-leaf : replacedTree key value leaf (node key value leaf leaf) r-node : {value₁ : A} → {left right : bt A} → replacedTree key value (node key value₁ left right) (node key value left right) -- key is the repl's key , so need comp key and key1 r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1 → replacedTree key value left repl → replacedTree key value (node key1 value1 left right) (node key1 value1 repl right) r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl) depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j ) depth-1< {i} {j} = s≤s (m≤m⊔n _ j) depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) depth-2< {i} {j} = s≤s (m≤n⊔m j i) depth-3< : {i : ℕ } → suc i ≤ suc (suc i) depth-3< {zero} = s≤s ( z≤n ) depth-3< {suc i} = s≤s (depth-3< {i} ) treeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A) → treeInvariant (node key value tleft tright) → treeInvariant tleft treeLeftDown leaf leaf (t-single key value) = t-leaf treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A) → treeInvariant (node key value tleft tright) → treeInvariant tright treeRightDown leaf leaf (t-single key value) = t-leaf treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2 findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A)) → (treeInvariant top) → stackInvariant tkey top orig st → (next : (newtop : bt A) → (stack : List (bt A)) → (treeInvariant newtop) → (stackInvariant tkey newtop orig stack) → bt-depth newtop < bt-depth top → t) → (exit : (newtop : bt A) → (stack : List (bt A)) → (treeInvariant newtop) → (stackInvariant tkey newtop orig stack) --need new stack ? → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t) → t findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl) findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl) findP tkey (node key value tl tr) orig st ti si next exit | tri< a ¬b ¬c = next tl (tl ∷ st) (treeLeftDown tl tr ti) (s-left a si) (s≤s (m≤m⊔n (bt-depth tl) (bt-depth tr))) findP tkey (node key value tl tr) orig st ti si next exit | tri> ¬a ¬b c = next tr (tr ∷ st) (treeRightDown tl tr ti) (s-right c si) (s≤s (m≤n⊔m (bt-depth tl) (bt-depth tr))) --RBT data Color : Set where Red : Color Black : Color RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A 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 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ black-depth leaf = 0 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 : {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₁) → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} → 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 → 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)} → {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 (node key ⟪ Black , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ 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 (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ 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-node : {t : bt A } → rotatedTree t t -- a b -- b c d a -- d e e c -- rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A} --kd < kb < ke < ka< kc → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} → kd < kb → kb < ke → ke < ka → ka < kc → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1) → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1) → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A} --kd < kb < ke < ka< kc → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child → kd < kb → kb < ke → ke < ka → ka < kc → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1) → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1) → 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)) RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) → RBtreeInvariant tleft RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf 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 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)) → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) → RBtreeInvariant tright RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti 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 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))) → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) → (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 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 child-replaced key (node key₁ value left right) with <-cmp key key₁ ... | tri< a ¬b ¬c = left ... | tri≈ ¬a b ¬c = node key₁ value left right ... | 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)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁) 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) 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 } → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand 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 pg : ParentGrand self parent uncle grand rest : List (bt A) stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where field od d rd : ℕ tree rot : bt (Color ∧ A) origti : treeInvariant orig origrb : RBtreeInvariant orig treerb : RBtreeInvariant tree replrb : RBtreeInvariant repl d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red)) si : stackInvariant key tree orig stack rotated : rotatedTree tree rot ri : replacedRBTree key value (child-replaced key rot ) repl rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) → RBtreeInvariant parent → RBtreeInvariant repl → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (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 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 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) ) → RBtreeInvariant parent → RBtreeInvariant repl → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right → RBtreeInvariant left → RBtreeInvariant right → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) ) 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 = {!!} -} -}