Mercurial > hg > Gears > GearsAgda
changeset 668:d009198364dc
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 22 Nov 2021 16:04:06 +0900 |
parents | eb3721179793 |
children | 077e2f3e417f |
files | hoareBinaryTree.agda |
diffstat | 1 files changed, 16 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Mon Nov 22 15:14:16 2021 +0900 +++ b/hoareBinaryTree.agda Mon Nov 22 16:04:06 2021 +0900 @@ -265,34 +265,30 @@ replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node replaceP : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A) - → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl - → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A)) - → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) + → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A) + → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 (tree ∷ stack) ∧ replacedTree key value tree repl + → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) + → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t -replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) refl ) -- can't happen -replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (proj1 (proj2 Pre)) -- tree0 ≡ leaf +replaceP key value {tree0} {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) {!!} ) -- can't happen +replaceP key value {tree0} {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (proj1 (proj2 Pre)) -- tree0 ≡ leaf ... | refl = exit tree0 (node key value leaf leaf) ⟪ proj1 Pre , r-leaf ⟫ -replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) - ⟪ proj1 Pre , subst₂ (λ j k → replacedTree key value j k ) repl03 repl04 (r-left a (proj2 (proj2 Pre)) ) ⟫ where - repl02 : node key₁ value₁ left right ≡ tree-st - repl02 = si-property1 (proj1 (proj2 Pre)) - repl03 : node key₁ value₁ tree right ≡ tree0 +replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ repl right ) + ⟪ proj1 Pre , subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) {!!} (r-left a (proj2 (proj2 Pre)) ) ⟫ where + repl03 : node key₁ value₁ left right ≡ tree0 repl03 with si-property-last _ _ _ _ (proj1 (proj2 Pre)) - ... | refl = {!!} - repl04 : node key₁ value₁ repl right ≡ node key₁ value₁ tree right - repl04 = {!!} + ... | refl = refl ... | tri≈ ¬a refl ¬c = exit tree0 (node key₁ value left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} r-node ⟫ ... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ -replaceP {n} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit = +replaceP {n} {_} {A} key value {tree0} {tree} repl (leaf ∷ st@(_ ∷ _)) Pre next exit = next key value {tree0} (node key value leaf leaf) st - ⟪ proj1 Pre , ⟪ repl01 (sym (si-property1 (proj1 (proj2 Pre)))) (proj1 (proj2 Pre)) - , subst (λ k → replacedTree key value k (node key value leaf leaf) ) (si-property1 (proj1 (proj2 Pre))) r-leaf ⟫ ⟫ ≤-refl where - repl01 : {x : bt A} → { xs : List (bt A)} → tree-st ≡ leaf → stackInvariant key tree-st tree0 (leaf ∷ x ∷ xs) → stackInvariant key x tree0 (x ∷ xs) + ⟪ proj1 Pre , ⟪ repl01 (sym (si-property1 (proj1 (proj2 Pre)))) {!!} + , subst (λ k → replacedTree key value k (node key value leaf leaf) ) {!!} r-leaf ⟫ ⟫ ≤-refl where + repl01 : {x : bt A} → { xs : List (bt A)} → {!!} → stackInvariant key tree tree0 (leaf ∷ x ∷ xs) → stackInvariant key x tree0 (x ∷ xs) repl01 {x} {xs} refl (s-right lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si repl01 {x} {xs} refl (s-left lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si -replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁ +replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁ ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl ... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl