Mercurial > hg > Gears > GearsAgda

changeset 896:1d22e0be980e

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 Wed, 29 May 2024 11:22:24 +0900
parents cce6181558ce
children f09d59c856a1
files hoareBinaryTree1.agda
diffstat 1 files changed, 36 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed May 29 04:01:25 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed May 29 11:22:24 2024 +0900
@@ -703,6 +703,21 @@
 RBtreeEQ  (rb-red _ _ x x₁ x₂ rb rb₁) = x₂
 RBtreeEQ  (rb-black _ _ x rb rb₁) = x
 
+RBtreeToBlack : {n : Level} {A : Set n} 
+ → (tree : bt (Color ∧ A))
+ → RBtreeInvariant tree
+ → RBtreeInvariant (to-black tree)
+RBtreeToBlack leaf rb-leaf = rb-leaf
+RBtreeToBlack (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = rb-black key value x₂ rb rb₁
+RBtreeToBlack (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = rb-black key value x rb rb₁
+
+RBtreeToBlackColor : {n : Level} {A : Set n} 
+ → (tree : bt (Color ∧ A))
+ → RBtreeInvariant tree
+ → color (to-black tree) ≡ Black
+RBtreeToBlackColor leaf rb-leaf = refl
+RBtreeToBlackColor (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = refl
+RBtreeToBlackColor (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = refl
 
 --
 --  findRBT exit with replaced node
@@ -1550,39 +1565,6 @@
      sc01 (s-left .parent .orig tree x si2) with si-property1 si2
      ... | refl = si2
 
-PGtoRBinvariantT : {n : Level} {A : Set n} 
-           → (tree orig : bt (Color ∧ A) )
-           → {key : ℕ } 
-           →  RBtreeInvariant orig
-           →  (stack : List (bt (Color ∧ A)))  → stackInvariant key tree orig stack
-           →  Set n 
-PGtoRBinvariantT tree .tree {key} rb .(tree ∷ []) s-nil = RBtreeInvariant tree
-PGtoRBinvariantT tree orig {key} rb (tree ∷ tail) (s-right .tree .orig tree₁ {key₁} {v1} x si) = RBtreeInvariant tree ∧ PGtoRBinvariantT  (node key₁ v1 tree₁ tree) orig rb tail si
-PGtoRBinvariantT tree orig {key} rb (tree ∷ tail) (s-left .tree .orig tree₁ {key₁} {v1} x si) = RBtreeInvariant tree ∧ PGtoRBinvariantT _ orig rb tail si
-
-PGtoRBinvariant : {n : Level} {A : Set n} 
-           → (tree orig : bt (Color ∧ A) )
-           → {key : ℕ } 
-           →  (rb : RBtreeInvariant orig)
-           →  (stack : List (bt (Color ∧ A)))  → (si : stackInvariant key tree orig stack )
-           →  PGtoRBinvariantT tree orig rb stack si
-PGtoRBinvariant tree .tree rb .(tree ∷ []) s-nil = rb
-PGtoRBinvariant tree .(node key₁ ⟪ Red , value ⟫ tree₂ tree) rb2@(rb-red .key₁ value x₁ x₂ x₃ rb rb₁) (tree ∷ .(node key₁ ⟪ Red , value ⟫ tree₂ tree) ∷ .[]) (s-right .tree .(node key₁ ⟪ Red , value ⟫ tree₂ tree) tree₂ {key₁} {.(⟪ Red , value ⟫)} x s-nil) = ⟪ rb₁ , rb2 ⟫
-PGtoRBinvariant tree .(node key₁ ⟪ Black , value ⟫ tree₂ tree) rb2@(rb-black .key₁ value x₁ rb rb₁) (tree ∷ .(node key₁ ⟪ Black , value ⟫ tree₂ tree) ∷ .[]) (s-right .tree .(node key₁ ⟪ Black , value ⟫ tree₂ tree) tree₂ {key₁} {.(⟪ Black , value ⟫)} x s-nil) = ⟪ rb₁ , rb2 ⟫
-PGtoRBinvariant tree orig rb (tree ∷ .(node key₁ v1 tree₂ tree) ∷ tail₁) (s-right .tree .orig tree₂ {key₁} {v1} x si2@(s-right .(node key₁ v1 tree₂ tree) .orig tree₁ x₁ si)) with PGtoRBinvariant _ orig rb _ si2
-... | ⟪ rb-red .key₁ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ = ⟪ proj5 , ⟪ rb-red key₁ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ ⟫
-... | ⟪ rb-black .key₁ value x₂ proj3 proj5 , proj4 ⟫ = ⟪ proj5 , ⟪ rb-black key₁ value x₂ proj3 proj5 , proj4 ⟫ ⟫
-PGtoRBinvariant tree orig rb (tree ∷ .(node key₁ v1 tree₂ tree) ∷ tail₁) (s-right .tree .orig tree₂ {key₁} {v1} x si2@(s-left .(node key₁ v1 tree₂ tree) .orig tree₁ x₁ si)) with PGtoRBinvariant _ orig rb _ si2
-... | ⟪ rb-red .key₁ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ = ⟪ proj5 , ⟪ rb-red key₁ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ ⟫
-... | ⟪ rb-black .key₁ value x₂ proj3 proj5 , proj4 ⟫ = ⟪ proj5 , ⟪ rb-black key₁ value x₂ proj3 proj5 , proj4 ⟫  ⟫
-PGtoRBinvariant tree (node _ _ tree tree₁) rb2@(rb-red _ value x₁ x₂ x₃ rb rb₁) (tree ∷ .(node _ ⟪ Red , value ⟫ tree tree₁ ∷ [])) (s-left .tree .(node _ ⟪ Red , value ⟫ tree tree₁) tree₁ x s-nil) = ⟪ rb , rb2 ⟫
-PGtoRBinvariant tree (node _ _ tree tree₁) rb2@(rb-black _ value x₁ rb rb₁) (tree ∷ .(node _ ⟪ Black , value ⟫ tree tree₁ ∷ [])) (s-left .tree .(node _ ⟪ Black , value ⟫ tree tree₁) tree₁ x s-nil) = ⟪ rb , rb2 ⟫
-PGtoRBinvariant tree orig rb (tree ∷ (node _ _ tree tree₁ ∷ tail)) (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with PGtoRBinvariant _ orig rb _ si2
-... | ⟪ rb-red _ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ = ⟪ proj3 , ⟪ rb-red _ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ ⟫
-... | ⟪ rb-black _ value x₂ proj3 proj5 , proj4 ⟫ = ⟪ proj3 , ⟪ rb-black _ value x₂ proj3 proj5 , proj4 ⟫ ⟫
-PGtoRBinvariant tree orig rb (tree ∷ (node _ _ tree tree₁ ∷ tail)) (s-left .tree .orig tree₁ x si2@(s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with PGtoRBinvariant _ orig rb _ si2
-... | ⟪ rb-red _ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ = ⟪ proj3 , ⟪ rb-red _ value x₂ x₃ x₄ proj3 proj5 , proj4 ⟫ ⟫
-... | ⟪ rb-black _ value x₂ proj3 proj5 , proj4 ⟫ = ⟪ proj3 , ⟪ rb-black _ value x₂ proj3 proj5 , proj4 ⟫ ⟫
 
 PGtoRBinvariant1 : {n : Level} {A : Set n} 
            → (tree orig : bt (Color ∧ A) )
@@ -1591,8 +1573,12 @@
            →  (stack : List (bt (Color ∧ A)))  → (si : stackInvariant key tree orig stack )
            →  RBtreeInvariant tree
 PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb
-PGtoRBinvariant1 tree orig rb .(tree ∷ _) (s-right .tree .orig tree₁ x si) = ?
-PGtoRBinvariant1 tree orig rb .(tree ∷ _) (s-left .tree .orig tree₁ x si) = ?
+PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-right .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si
+... | rb-red _ value x₁ x₂ x₃ t t₁ = t₁
+... | rb-black _ value x₁ t t₁ = t₁
+PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-left .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si
+... | rb-red _ value x₁ x₂ x₃ t t₁ = t
+... | rb-black _ value x₁ t t₁ = t
 
 RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) →  RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr)
 RBI-child-replaced {n} {A} leaf key rbi = rbi
@@ -1783,7 +1769,10 @@
          black-depth right ≡⟨ (sym (RBtreeEQ (RBI.origrb r))) ⟩
          black-depth left ∎
             where open ≡-Reasoning  
-... | case2 (case2 pg) with PG.uncle pg in uneq
+... | case2 (case2 pg) with (PG.parent pg) in preq
+... | leaf = {!!} -- can't happen
+... | node kp ⟪ Black , vp₁ ⟫ t₁ t₂ = ?  -- insertCase1 -- parent is Black 
+... | node kp ⟪ Red , vp₁ ⟫ t₁₁ t₁₂ with PG.uncle pg in uneq
 ... | leaf = {!!} -- insertCase5
 ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5
 ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg
@@ -1792,16 +1781,21 @@
          tree = PG.grand pg
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
-         ; treerb = ?
-         ; replrb = {!!}
+         ; treerb = rb01
+         ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) ? (rb-black _ _ ? (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
          ; si = stackCase2 (PG.rest pg) (RBI.tree r) (PG.parent pg) (PG.grand pg) orig _  rb00
-         ; state = rotate refl {!!} {!!}
+         ; state = rotate refl ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym ?) refl  (rbr-flip-ll repl-red ? ? rot))
      }  ? where
        rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
        rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
-       rb01 :  PGtoRBinvariantT (RBI.tree r) orig (RBI.origrb r) (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
-            (subst (stackInvariant key (RBI.tree r) orig) (PG.stack=gp pg) (RBI.si r))
-       rb01 = PGtoRBinvariant _ orig (RBI.origrb r) _ rb00 
+       rb01 :  RBtreeInvariant (PG.grand pg)
+       rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (stackCase2 (PG.rest pg) (RBI.tree r) (PG.parent pg) (PG.grand pg) orig _  rb00)
+       rb02 : RBtreeInvariant (PG.uncle pg)
+       rb02 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
+       rb03 : RBtreeInvariant (PG.parent pg)
+       rb03 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
+       rb04 : RBtreeInvariant n1
+       rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}