Mercurial > hg > Gears > GearsAgda

changeset 805:28323f2e6dc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
write depth
author mori
date Mon, 18 Dec 2023 18:58:21 +0900
parents a03d00eba6b7
children a11ebb914b7c
files hoareBinaryTree1.agda
diffstat 1 files changed, 9 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Dec 11 19:51:04 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Dec 18 18:58:21 2023 +0900
@@ -203,7 +203,7 @@
 ... | tri< a ¬b ¬c = left
 ... | tri≈ ¬a b ¬c = node key₁ value left right
 ... | tri> ¬a ¬b c = right
-
+{-
 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
    field
      tree0 : bt A
@@ -526,7 +526,7 @@
 -- other element is preserved?
 
 -- deletion?
-
+-}
 data Color  : Set where
     Red : Color
     Black : Color
@@ -626,7 +626,9 @@
    → 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
 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
  →  (tleft tright : bt (Color ∧ A))
  → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
@@ -977,11 +979,13 @@
                ... | 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 (¬a {!!})
                ... | 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 {!!} {!!} {!!} {!!}) (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = 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 = {!!}
                ... | 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 | t = {!!} 
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ ? ? ? ? ? ) ? , ? ⟫
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ?
                ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!}　-- red-red
                ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} 
                --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫