Mercurial > hg > Gears > GearsAgda

changeset 810:194b5ae1a7a0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jan 2024 10:22:56 +0900
parents 243faca58e90
children f655afa1b8ea
files hoareBinaryTree1.agda
diffstat 1 files changed, 13 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun Jan 21 12:49:28 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jan 22 10:22:56 2024 +0900
@@ -549,22 +549,7 @@
 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
@@ -684,19 +669,6 @@
  = 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 : ℕ)
@@ -751,7 +723,6 @@
     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
@@ -982,14 +953,19 @@
              } where
                rb07 :  black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl
                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)
-          
+               ... | tri< a ¬b ¬c = rb08 where
+                   rb08 : black-depth left ≡ black-depth left ⊔ black-depth repl
+                   rb08 = ?
+               ... | tri≈ ¬a b ¬c = ? where
+                   rb08 : suc (black-depth left ⊔ black-depth (RBI.rot r)) ≡ black-depth left ⊔ black-depth repl
+                   rb08 = ?
+               ... | tri> ¬a ¬b c = ? where
+                   rb08 : black-depth (RBI.rot r) ≡ black-depth left ⊔ black-depth repl
+                   rb08 = ?
                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
+               rb09 (rb-right-red x x0 x2) = x
                -- rb05 should more general
                tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
                tkey (node key value t t2) = key
@@ -1005,11 +981,11 @@
                ... | 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 = ⟪ rb-right-red a ? (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 = ⟪ rb-right-red a ? (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
@@ -1027,6 +1003,5 @@
            --     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)
 
--}