Mercurial > hg > Gears > GearsAgda

changeset 897:f09d59c856a1

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 14:23:41 +0900
parents 1d22e0be980e
children e5ac221866c5
files hoareBinaryTree1.agda
diffstat 1 files changed, 12 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed May 29 11:22:24 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed May 29 14:23:41 2024 +0900
@@ -136,6 +136,15 @@
 si-property2 (.leaf ∷ []) (s-left _ _ tree₁ x ()) refl
 si-property2 (x₁ ∷ x₂ ∷ stack) (s-left _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq
 
+si-property-< :  {n : Level} {A : Set n} {key key₁ kp : ℕ} {value₁ value₂ : A} {tree orig tree₁ tree₂ tree₃ : bt A} → {stack  : List (bt A)}
+   → tree ≡ node key₁ value₁ tree₁ tree₂
+   → stackInvariant key orig tree (tree ∷ node kp value₂ tree  tree₃ ∷ stack)
+   → kp < key
+si-property-< refl (s-right _ _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) .(node _ _ _ _) tree₁ x₁ si)) = ?
+si-property-< refl (s-right _ _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) .(node _ _ _ _) tree x₁ si)) = x
+si-property-< refl (s-left _ _ tree x (s-right .(node _ _ (node _ _ _ _) tree) .(node _ _ _ _) tree₁ x₁ si)) = ?
+si-property-< refl (s-left _ _ tree x (s-left .(node _ _ (node _ _ _ _) tree) .(node _ _ _ _) tree₁ x₁ si)) = ?
+
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
 si-property-last key t t0 (t ∷ [])  (s-nil )  = refl
@@ -1784,7 +1793,7 @@
          ; 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 ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym ?) refl  (rbr-flip-ll repl-red ? ? rot))
+         ; state = rotate refl ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym ?) refl  (rbr-flip-ll repl-red (rb05 refl uneq) ? 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)
@@ -1796,6 +1805,8 @@
        rb03 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
        rb04 : RBtreeInvariant n1
        rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
+       rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
+       rb05 refl refl = refl
 ... | 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₁ = {!!}