Mercurial > hg > Gears > GearsAgda

changeset 920:368b9be0b312

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, 05 Jun 2024 09:54:19 +0900
parents 4d379ebc53c8
children 46ec01e94947
files hoareBinaryTree1.agda
diffstat 1 files changed, 28 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Jun 04 17:29:33 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Jun 05 09:54:19 2024 +0900
@@ -183,16 +183,15 @@
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
--- Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) →  (tree : bt A) → (stack  : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set
--- Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ?
--- Diffkey A (node key₁ value tree0 tree1) key .(node key₁ value tree0 tree1) .(node key₁ value tree0 tree1 ∷ []) s-nil = ?
--- Diffkey A tree0 key leaf .(leaf ∷ _) (s-right .leaf .tree0 tree₁ x si) = ?
--- Diffkey A tree0 key (node key₁ value tree tree₂) .(node key₁ value tree tree₂ ∷ _) (s-right .(node key₁ value tree tree₂) .tree0 tree₁ x si) = ?
--- Diffkey A tree0 key tree .(tree ∷ _) (s-left .tree .tree0 tree₁ x si) = ?
+si-property-pne :  {n : Level} {A : Set n}  {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right : bt A} → (stack  : List (bt A)) {rest : List (bt A)}
+    → stack ≡ tree ∷ node key₁ value₁ left right ∷ rest
+    → stackInvariant key tree orig stack
+    → ¬ ( key ≡ key₁ )
+si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-right .tree .orig tree₁ x si) eq with si-property1 si
+... | refl = ⊥-elim ( nat-≡< (sym eq) x)
+si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-left .tree .orig tree₁ x si) eq with si-property1 si
+... | refl = ⊥-elim ( nat-≡< eq x)
 
--- si-property-ne :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
---    → length stack > 1 → ¬ ( node-key tree ≡ just key )
--- si-property-ne = ?
 
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
@@ -1732,20 +1731,20 @@
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
  → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t
-replaceRBTNode {n} {m} {A}  {t} key value orig rbi ti leaf stack si (case1 refl) exit with stackToPG leaf orig stack si
+replaceRBTNode {n} {m} {A}  {t} key value orig rbi ti tree stack si P exit with stackToPG tree orig stack si
 ... | case1 x = ?
 ... | case2 (case1 x) = ?
-... | case2 (case2 pg) = rp00 where
-   rb00 : stackInvariant key leaf orig (leaf ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
-   rb00 = subst (λ k → stackInvariant key leaf orig k) (PG.stack=gp pg) si
+... | case2 (case2 pg) = rp01 where
+   rb00 : stackInvariant key tree orig (tree ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
+   rb00 = subst (λ k → stackInvariant key tree orig k) (PG.stack=gp pg) si
    treerb :  RBtreeInvariant (PG.parent pg)
    treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
    pti : treeInvariant (PG.parent pg)
    pti = siToTreeinvariant _ _ _ _ ti (popStackInvariant _ _ _ _ _ rb00)
-   rp00 : t
-   rp00 with PG.pg pg
-   ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with proj1 vp in pcolor
-   ... | Red = rotateCase1 where
+   rp01 : t
+   rp01 with PG.pg pg
+   ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with <-cmp key kp | proj1 vp in pcolor 
+   ... | tri< a ¬b ¬c | Red = rotateCase1 where
        rotateCase1 : t
        rotateCase1 = exit (PG.grand pg ∷ PG.rest pg) record {
              tree = PG.grand pg
@@ -1756,11 +1755,11 @@
            ; replrb = rb-red _ ? ? ? ? ? ? 
            ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
            ; state = rotate ? ? ? ? }
-   ... | Black = buildCase1 where
+   ... | tri< a ¬b ¬c | Black = buildCase1 where
        rb01 : bt (Color ∧ A)
        rb01 = node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1
-       rb03 : 1 ≡ black-depth n1
-       rb03 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
+       rb03 : ? -- 1 ≡ black-depth n1
+       rb03 = ? -- RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
        rb02 : RBtreeInvariant (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1)
        rb02 = rb-black kp (proj2 vp) rb03 (rb-red _ _ refl refl refl rb-leaf rb-leaf) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb))
        rb04 : proj1 vp ≡ Black → ⟪ Black , proj2 vp ⟫ ≡ vp
@@ -1770,14 +1769,14 @@
            black-depth (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ cong (λ k → black-depth (node kp k _ n1)) (sym (rb04 pcolor)) ⟩
            black-depth (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ refl  ⟩
            black-depth (node kp ⟪ Black , proj2 vp ⟫  leaf n1 )  ≡⟨ cong (λ k → black-depth (node kp k leaf n1)) (rb04 pcolor) ⟩
-           black-depth (node kp vp leaf n1)  ≡⟨ cong black-depth (sym x)  ⟩
+           black-depth (node kp vp leaf n1)  ≡⟨ ? ⟩
            black-depth (PG.parent pg) ∎ where 
               open ≡-Reasoning
        rb07 : key < kp
        rb07 = si-property-<  ? (subst (λ k → treeInvariant k) x pti) (subst₂ (λ j k → stackInvariant key j orig k) refl (trans (PG.stack=gp pg) ? ) si)
        rb06 : replacedRBTree key value (PG.parent pg) (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)
-       rb06 = subst₂ (λ j k → replacedRBTree key value k  (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor) 
-           (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf )
+       rb06 = ? -- subst₂ (λ j k → replacedRBTree key value k  (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor) 
+           -- (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf )
        buildCase1 : t
        buildCase1 = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
              tree = PG.parent pg
@@ -1788,18 +1787,11 @@
            ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k (node key ⟪ Red , value ⟫ leaf leaf) n1) (rb04 pcolor))  rb02
            ; si = popStackInvariant _ _ _ _ _ rb00
            ; state = rebuild  (cong color x) rb05 rb06 } 
-   rp00 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
-   rp00 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
-   rp00 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
-replaceRBTNode {n} {m} {A}  key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit ? record {
-     tree = tree
-   ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
-   ; origti = ti
-   ; origrb = rbi
-   ; treerb = PGtoRBinvariant1 tree orig rbi stack si
-   ; replrb = ?
-   ; si = si
-   ; state = rebuild ? ? ? }
+   ... | tri≈ ¬a b ¬c | t = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → tree ∷ k ∷ _) x) ) si b )
+   ... | tri> ¬a ¬b c | t = ?
+   rp01 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+   rp01 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+   rp01 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 
 --
 --   rotate and rebuild replaceTree and rb-invariant
@@ -1875,13 +1867,7 @@
          ; si = s-nil
          ; state = top-black  refl (case2 (rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)))
          }
-    ... | tri≈ ¬a b ¬c = ⊥-elim ( rb06 _ eq (RBI.si r) b ) where -- can't happen
-       rb06 : (stack    : List (bt (Color ∧ A))) → stack ≡ RBI.tree r ∷ node key₁ value₁ left right ∷ []
-         →  stackInvariant key (RBI.tree r) (node key₁ value₁ left right) stack
-         → key ≡ key₁
-         → ⊥
-       rb06 (.right ∷ node key₁ value₁ left right ∷ []) refl (s-right .right .(node key₁ value₁ left right) .left x s-nil) eq = ⊥-elim ( nat-≡< (sym eq) x)
-       rb06 (.left ∷ node key₁ value₁ left right ∷ []) refl (s-left .left .(node key₁ value₁ left right) .right x s-nil) eq = ⊥-elim ( nat-≡< eq x)
+    ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack eq si b ) -- can't happen
     ... | tri> ¬a ¬b c = rb07 col where
        rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
        rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl