Mercurial > hg > Gears > GearsAgda

changeset 895:cce6181558ce

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 04:01:25 +0900
parents 9570d950d440
children 1d22e0be980e
files hoareBinaryTree1.agda
diffstat 1 files changed, 48 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon May 27 17:32:41 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed May 29 04:01:25 2024 +0900
@@ -1526,6 +1526,7 @@
 ... | s2-s12p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 ... | s2-1s2p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 
+
 stackCase2 : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
            → ( tree parent grand orig : bt (Color ∧ A)) →  (key : ℕ)
            → stackInvariant key tree  orig ( tree ∷ parent ∷ grand ∷ rest )
@@ -1549,11 +1550,49 @@
      sc01 (s-left .parent .orig tree x si2) with si-property1 si2
      ... | refl = si2
 
--- PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
---            →  RBtreeInvariant orig
---            →  (stack : List (bt (Color ∧ A)))  → (pg : PG (Color ∧ A) tree stack )
---            →  RBtreeInvariant tree ∧  RBtreeInvariant (PG.parent pg) ∧  RBtreeInvariant (PG.grand pg)
--- PGtoRBinvariant = {!!}
+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) )
+           → {key : ℕ } 
+           →  (rb : RBtreeInvariant orig)
+           →  (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) = ?
 
 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
@@ -1753,13 +1792,16 @@
          tree = PG.grand pg
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
-         ; treerb = {!!}
+         ; treerb = ?
          ; replrb = {!!}
          ; si = stackCase2 (PG.rest pg) (RBI.tree r) (PG.parent pg) (PG.grand pg) orig _  rb00
          ; state = rotate refl {!!} {!!}
      }  ? 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 
 ... | 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₁ = {!!}