Mercurial > hg > Gears > GearsAgda

changeset 824:7d73749f097e

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 Sun, 28 Jan 2024 12:19:45 +0900
parents ebee6945c697
children 02f431665ebc
files hoareBinaryTree1.agda
diffstat 1 files changed, 36 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat Jan 27 18:24:40 2024 +0900
+++ b/hoareBinaryTree1.agda	Sun Jan 28 12:19:45 2024 +0900
@@ -776,6 +776,11 @@
                                     (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ t₁ uncle) (node kp ⟪ Red , vp ⟫ t₂ t₃)) 
 
 
+--
+-- Parent Grand Relation
+--   should we require stack-invariant?
+--
+
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
         → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
@@ -854,11 +859,29 @@
            →  stack ≡ orig ∷ [] → tree ≡ orig
 stackCase1 s-nil refl = refl
 
-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 = {!!}
+pg-prop-1 : {n : Level} (A : Set n) → (tree orig : bt A )
+           →  (stack : List (bt A)) → (pg : PG A tree stack)
+           → (¬  PG.grand pg ≡ leaf ) ∧  (¬  PG.parent pg ≡ leaf)
+pg-prop-1 {_} A tree orig stack pg with PG.pg pg
+... | s2-s1p2 refl refl = ⟪ (λ () ) , ( λ () ) ⟫
+... | s2-1sp2 refl refl = ⟪ (λ () ) , ( λ () ) ⟫
+... | s2-s12p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
+... | s2-1s2p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
+
+pg-prop-2 : {n : Level} (A : Set n) → (tree orig : bt A ) → {key : ℕ }
+           →  (stack : List (bt A)) → (si : stackInvariant key tree orig stack)  → (pg : PG A tree stack)
+           → ¬  (node-key (PG.parent pg) ≡ node-key tree) 
+pg-prop-2 {_} A tree orig stack si pg with PG.pg pg | PG.stack=gp pg
+... | s2-s1p2 x x₁ | t = ?
+... | s2-1sp2 x x₁ | t = ?
+... | s2-s12p x x₁ | t = ?
+... | s2-1s2p x x₁ | t = ?
+
+-- 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 = {!!}
 
 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
@@ -869,9 +892,9 @@
 
 -- this is too complacted to extend all arguments at once
 -- 
-RBTtoRBI  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → RBtreeInvariant tree
-     → replacedRBTree key value tree repl → RBtreeInvariant repl
-RBTtoRBI {_} {A} tree repl key value rbi rlt = ?
+-- RBTtoRBI  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → RBtreeInvariant tree
+--      → replacedRBTree key value tree repl → RBtreeInvariant repl
+-- RBTtoRBI {_} {A} tree repl key value rbi rlt = ?
 --
 -- create RBT invariant after findRBT, continue to replaceRBT
 --
@@ -913,18 +936,18 @@
      → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
         → (r : RBI key value orig tree1 stack1 )
         → length stack1 < length stack  → t ) → t
-insertCase5 {n} {m} {A} {t} key value orig tree stack r pg cu=b cp=r next = {!!} where
+insertCase5 {n} {m} {A} {t} key value orig tree stack r pg cu=b cp=r next = insertCase51 tree (PG.grand pg) refl refl where
     -- check inner repl case
     --     node-key parent < node-key repl < node-key grand  → rotateLeft  parent    then insertCase6
     --     node-key grand  < node-key repl < node-key parent → rotateRight parent    then insertCase6
     --     else insertCase6
     insertCase51 : (tree1 grand : bt (Color ∧ A)) → tree1 ≡ tree → grand ≡ PG.grand pg → t
-    insertCase51 leaf grand teq geq = ?    -- can't happen
+    insertCase51 leaf grand teq geq = next ? ? ? ?
     insertCase51 (node kr vr rleft rright) leaf teq geq = ?    -- can't happen
     insertCase51 (node kr vr rleft rright) (node kg vg grand grand₁) teq geq with <-cmp kr kg
-    ... | tri< a ¬b ¬c = ? where
+    ... | tri< a ¬b ¬c = insertCase511 (PG.parent pg) refl where
           insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t
-          insertCase511 leaf peq = ? -- can't happen
+          insertCase511 leaf peq = ⊥-elim (proj2 (pg-prop-1 _ tree orig stack pg) (sym peq) )
           insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂
           ... | tri< a ¬b ¬c = next ? ? ? ?
           ... | tri≈ ¬a b ¬c = ? -- can't happen
@@ -932,7 +955,7 @@
     ... | tri≈ ¬a b ¬c = ? -- can't happen
     ... | tri> ¬a ¬b c = ? where
           insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t
-          insertCase511 leaf peq = ? -- can't happen
+          insertCase511 leaf peq = ⊥-elim (proj2 (pg-prop-1 _ tree orig stack pg) (sym peq) )
           insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂
           ... | tri< a ¬b ¬c = next ? ? ? ? --- rotareLeft → insertCase6 key value orig ? stack ? pg next exit
           ... | tri≈ ¬a b ¬c = ? -- can't happen