Mercurial > hg > Gears > GearsAgda

changeset 924:69aab3105ac4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
createRBT done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 07 Jun 2024 17:36:01 +0900
parents 62393055b0dd
children 9a67eb8e71ac
files hoareBinaryTree1.agda
diffstat 1 files changed, 8 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Jun 07 17:18:41 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Jun 07 17:36:01 2024 +0900
@@ -1781,8 +1781,7 @@
              crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
              crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) (keq eq) rbr-node
 createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ leaf ∷ stack) si P exit = ⊥-elim (si-property-parent-node _ _ _ si refl)
-createRBT {n} {m} {A} {t} key value orig rbi ti tree sp@(x ∷ node kp vp pleft pright ∷ stack) si P exit with <-cmp key kp
-... | tri< a ¬b ¬c = crbt00 tree P refl where
+createRBT {n} {m} {A} {t} key value orig rbi ti tree sp@(x ∷ node kp vp pleft pright ∷ stack) si P exit = crbt00 tree P refl where
      crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ tree → t
      crbt00 leaf P refl = exit sp record {  
          tree = leaf
@@ -1801,8 +1800,8 @@
          ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right 
          ; origti = ti
          ; origrb = rbi
-         ; treerb = ?
-         ; replrb = ?
+         ; treerb = treerb
+         ; replrb = crbt03 value₁ treerb
          ; si = si
          ; state = rebuild refl (crbt01 value₁ ) crbt04
          }  where 
@@ -1812,10 +1811,12 @@
              crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
              crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁
              crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁
+             keq : ( just key₁ ≡ just key ) → key₁ ≡ key
+             keq refl = refl
              crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
-             crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) ? rbr-node
-... | tri≈ ¬a b ¬c = ⊥-elim (si-property-pne _ _ _ refl si b)
-... | tri> ¬a ¬b c = ?
+             crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) (keq eq) rbr-node
+             treerb : RBtreeInvariant (node key₁ value₁ left right)
+             treerb = PGtoRBinvariant1 _ orig rbi _ si
 
 --
 --   rotate and rebuild replaceTree and rb-invariant