Mercurial > hg > Gears > GearsAgda

changeset 800:418ab1fa2aca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rb07
author Moririn
date Mon, 20 Nov 2023 10:31:44 +0900
parents 794f6d8ddac2
children 772a6bb0b614
files hoareBinaryTree1.agda
diffstat 1 files changed, 33 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat Oct 28 19:11:12 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Nov 20 10:31:44 2023 +0900
@@ -1,3 +1,4 @@
+
 module hoareBinaryTree1 where
 
 open import Level hiding (suc ; zero ; _⊔_ )
@@ -544,6 +545,28 @@
 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₁ )
 
+pro1 : { m : ℕ } → zero ≡ suc m → ⊥
+pro1 ()
+pro2 : {m : ℕ } → suc m ≡ zero → ⊥ 
+pro2 ()
+{-# TERMINATING #-}
+DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n
+DepthCal zero zero zero  = refl 
+DepthCal zero zero (suc n)  = ⊥-elim (pro1 (DepthCal zero zero (suc n)))
+DepthCal zero (suc m) zero  = ⊥-elim (pro1 (DepthCal zero (suc m) zero))
+DepthCal zero (suc m) (suc n)  = ⊥-elim (pro1 (DepthCal zero (suc m) (suc n)))
+DepthCal (suc l) zero zero  = ⊥-elim (pro2 (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)
@@ -748,7 +771,12 @@
 ... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi
 ... | tri≈ ¬a b ¬c = rbi
 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
-
+{-
+ReplRBI : {n : Level} {A : Set n } {key : ℕ} {value : A } (c : Color ) → { tree1 : bt (Color ∧ A)} → (repl tree : bt (Color ∧ A)) → RBtreeInvariant tree → RBtreeInvariant tree1 → RBtreeInvariant repl
+ → RBtreeInvariant (node key ⟪ c , value ⟫ tree tree1 ) → RBtreeInvariant (node key ⟪ c , value  ⟫ tree repl)
+ReplRBI Red leaf leaf rbt rbt1 rbrepl rbtt1 = {!!} --⊥-elim ( ¬(Red ≡ Black))
+ReplRBI Black (node key ⟪ c , value ⟫ t t1) (node key1 value1 l r) rbt rbt1 rbrepl rbtt1 = {!!}
+-}
 -- 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
@@ -933,9 +961,9 @@
              } 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 = {!!}
-               ... | tri≈ ¬a b ¬c = {!!}
-               ... | tri> ¬a ¬b c = {!!}
+               ... | 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)
                -- rb05 should more general
                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)
@@ -947,7 +975,7 @@
                ... | 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-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 = {!!}
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)