Mercurial > hg > Gears > GearsAgda
changeset 907:fb6644858d1a
s-nil with non-leaf is no good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 31 May 2024 18:12:15 +0900 |
| parents | a1b7703f8551 |
| children | 0c41ca92c9ba |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 43 insertions(+), 41 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri May 31 17:23:46 2024 +0900 +++ b/hoareBinaryTree1.agda Fri May 31 18:12:15 2024 +0900 @@ -77,7 +77,7 @@ -- stack always contains original top at end (path of the tree) -- data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where - s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) + s-nil : {tree0 : bt A} → ¬ (tree0 ≡ leaf) → stackInvariant key tree0 tree0 (tree0 ∷ []) s-right : (tree tree0 tree₁ : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) s-left : (tree₁ tree0 tree : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} @@ -127,16 +127,16 @@ stack-last (x ∷ s) = stack-last s stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) -stackInvariantTest1 = s-right _ _ _ (add< 3) (s-nil ) +stackInvariantTest1 = s-right _ _ _ (add< 3) (s-nil ? ) si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] ) -si-property0 (s-nil ) () +si-property0 (s-nil _ ) () si-property0 (s-right _ _ _ x si) () si-property0 (s-left _ _ _ x si) () si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack) → tree1 ≡ tree -si-property1 (s-nil ) = refl +si-property1 (s-nil _ ) = refl si-property1 (s-right _ _ _ _ si) = refl si-property1 (s-left _ _ _ _ si) = refl @@ -152,12 +152,12 @@ → treeInvariant (node kp value₂ tree tree₃ ) → stackInvariant key tree orig (tree ∷ node kp value₂ tree tree₃ ∷ stack) → key < kp -si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂) +si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-nil _)) = ⊥-elim (nat-<> x₁ x₂) si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂) si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂) si-property-< ne ti (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = x si-property-< ne ti (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree₁ x₁ si)) = x -si-property-< ne ti (s-left _ _ _ x s-nil) = x +si-property-< ne ti (s-left _ _ _ x (s-nil _)) = x si-property-< ne (t-single _ _) (s-right _ _ tree₁ x si) = ⊥-elim ( ne refl ) si-property-> : {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack : List (bt A)} @@ -165,28 +165,30 @@ → treeInvariant (node kp value₂ tree₃ tree ) → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃ tree ∷ stack) → kp < key -si-property-> ne ti (s-right _ _ tree₁ x s-nil) = x +si-property-> ne ti (s-right _ _ tree₁ x (s-nil _)) = x si-property-> ne ti (s-right _ _ tree₁ x (s-right .(node _ _ tree₁ _) _ tree₂ x₁ si)) = x si-property-> ne ti (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ si)) = x -si-property-> ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left _ _ _ x s-nil) = ⊥-elim (nat-<> x₁ x₂) +si-property-> ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left _ _ _ x (s-nil _)) = ⊥-elim (nat-<> x₁ x₂) si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = ⊥-elim (nat-<> x₂ x₃) si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree x₁ si)) = ⊥-elim (nat-<> x₂ x₃) -si-property-> ne (t-single _ _) (s-left _ _ _ x s-nil) = ⊥-elim ( ne refl ) +si-property-> ne (t-single _ _) (s-left _ _ _ x (s-nil _)) = ⊥-elim ( ne refl ) si-property-> ne (t-single _ _) (s-left _ _ _ x (s-right .(node _ _ leaf leaf) _ tree₁ x₁ si)) = ⊥-elim ( ne refl ) si-property-> ne (t-single _ _) (s-left _ _ _ x (s-left .(node _ _ leaf leaf) _ tree x₁ si)) = ⊥-elim ( ne refl ) 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 +si-property-last key t t0 (t ∷ []) (s-nil _) = refl si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ _ _ _ si ) with si-property1 si ... | refl = si-property-last key x t0 (x ∷ st) si 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 -si-property-not-orig-leaf : {n : Level} {A : Set} {stack : List ( bt A)} {tree orig : bt A} {key : ℕ} → stackInvariant key tree orig stack → ¬ ( orig ≡ leaf ) -si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-nil ) = ? -si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-right _ _ _ _ si) = ? -si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-left _ _ _ _ si) = ? +si-property-not-orig-leaf : {n : Level} (A : Set n) (stack : List ( bt A)) {tree orig : bt A} {key : ℕ} → stackInvariant key tree orig stack → ¬ ( orig ≡ leaf ) +si-property-not-orig-leaf {n} A .(tree ∷ []) {tree} {.tree} {key} (s-nil x) = x +si-property-not-orig-leaf {n} A (tree ∷ s2@(x₁ ∷ stack)) {tree} {orig} {key} (s-right .tree .orig tree₁ x si) with si-property1 si +... | refl = si-property-not-orig-leaf {n} A s2 {x₁} {orig} {key} si +si-property-not-orig-leaf {n} A (tree ∷ x₁ ∷ stack) {tree} {orig} {key} (s-left .tree .orig tree₁ x si) with si-property1 si +... | refl = si-property-not-orig-leaf A (x₁ ∷ stack) {x₁} si -- rb04 refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl -- rb04 refl refl (s-left tree₁ leaf tree x si) = si-property2 _ (s-left tree₁ leaf tree x si) refl @@ -671,7 +673,7 @@ insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t insertTreeP {n} {m} {A} {t} tree key value P0 exit = - TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ⟫ + TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ? ⟫ $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) $ λ t s P C → replaceNodeP key value t C (proj1 P) $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A ) @@ -832,7 +834,7 @@ → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) - {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫ + {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ? ⟫ $ λ p RBP loop → findRBT k (proj1 p) tr0 (proj2 p) RBP (λ t1 s1 P2 lt1 → loop ⟪ t1 , s1 ⟫ P2 lt1 ) $ λ tr1 st P2 O → exit tr1 st P2 O @@ -1609,28 +1611,28 @@ stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) → (stack : List (bt A)) → stackInvariant key tree orig stack → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack -stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl -stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl) -stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ s-nil)) = case2 (case2 +stackToPG {n} {A} {key} tree .tree .(tree ∷ []) (s-nil _) = case1 refl +stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x (s-nil _)) = case2 (case1 refl) +stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ (s-nil _ ))) = case2 (case2 record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) -stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ s-nil)) = case2 (case2 +stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-nil _))) = case2 (case2 record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } ) -stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x s-nil) = case2 (case1 refl) -stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ s-nil)) = case2 (case2 +stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-nil _)) = case2 (case1 refl) +stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-nil _))) = case2 (case2 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } ) -stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ s-nil)) = case2 (case2 +stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-nil _))) = case2 (case2 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) @@ -1640,7 +1642,7 @@ stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } → {stack : List (bt A)} → stackInvariant key tree orig stack → stack ≡ orig ∷ [] → tree ≡ orig -stackCase1 s-nil refl = refl +stackCase1 (s-nil _) refl = refl pg-prop-1 : {n : Level} (A : Set n) → (tree orig : bt A ) → (stack : List (bt A)) → (pg : PG A tree stack) @@ -1670,11 +1672,11 @@ → treeInvariant orig → stackInvariant key tree orig ( tree ∷ rest ) → treeInvariant tree -siToTreeinvariant .[] tree .tree key ti s-nil = ti -siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf -siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x s-nil) = ti -siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf -siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁ +siToTreeinvariant .[] tree .tree key ti (s-nil _) = ti +siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x (s-nil _)) = t-leaf +siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x (s-nil _)) = ti +siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x (s-nil _)) = t-leaf +siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x (s-nil _)) = ti₁ siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 ... | t-single _ _ = t-leaf ... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ @@ -1685,10 +1687,10 @@ ... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ ... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ -siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf -siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x s-nil) = t-leaf -siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x s-nil) = ti -siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x s-nil) = ti +siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x (s-nil _)) = t-leaf +siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x (s-nil _)) = t-leaf +siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x (s-nil _)) = ti +siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x (s-nil _)) = ti siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 ... | t-single _ _ = t-leaf ... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf @@ -1706,7 +1708,7 @@ → (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 .tree rb .(tree ∷ []) (s-nil _) = rb PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-right .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si ... | rb-red _ value x₁ x₂ x₃ t t₁ = t₁ ... | rb-black _ value x₁ t t₁ = t₁ @@ -1837,12 +1839,12 @@ ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)) - ; si = s-nil + ; si = s-nil ? ; state = top-black refl (rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)) } where rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r - rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl - rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si + rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x (s-nil _)) refl refl = refl + rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x (s-nil _)) refl refl with si-property1 si ... | refl = ⊥-elim ( nat-<> x a ) rb05 : child-replaced key (node key₁ value₁ left right) ≡ left rb05 with <-cmp key key₁ @@ -1861,8 +1863,8 @@ → 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) + 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 | cr = exit (to-black (node key₁ value₁ left repl)) (orig ∷ []) refl record { tree = orig ; ¬leaf = λ () @@ -1870,11 +1872,11 @@ ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = rb-black _ _ (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r) - ; si = s-nil + ; si = s-nil ? ; state = top-black refl (rbr-black-right repl-red c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)) } 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 + rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x (s-nil _)) refl refl = refl rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si ... | refl = ⊥-elim ( nat-<> x c ) rb05 : child-replaced key (node key₁ value₁ left right) ≡ right