Mercurial > hg > Gears > GearsAgda
changeset 645:6340956f143e
...ZZ
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Nov 2021 16:47:39 +0900 |
| parents | a3fb9ffa3d60 |
| children | 83ba41589564 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 55 insertions(+), 55 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Fri Nov 19 13:29:01 2021 +0900 +++ b/hoareBinaryTree.agda Fri Nov 19 16:47:39 2021 +0900 @@ -97,12 +97,12 @@ → treeInvariant (node key₂ value₂ t₃ t₄) → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) -data stackInvariant {n : Level} {A : Set n} : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where - s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] ) - s-right : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} - → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree₁ tree0 (tree₁ ∷ st) - s-left : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} - → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree ∷ st) +data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where + s-single : (tree : bt A) → stackInvariant key tree tree (tree ∷ [] ) + s-right : {tree0 tree 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 : {tree0 tree 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) data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where r-leaf : replacedTree key value leaf (node key value leaf leaf) @@ -134,22 +134,27 @@ stack-last (x ∷ []) = just x stack-last (x ∷ s) = stack-last s -stackInvariantTest1 : stackInvariant treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) -stackInvariantTest1 = s-right (s-single treeTest1 ) +stackInvariantTest1 : stackInvariant 2 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) +stackInvariantTest1 = s-right (add< 0) (s-single treeTest1 ) -si-property1 : {n : Level} {A : Set n} (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant tree tree0 stack +si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {st : List (bt A)} → stackInvariant key tree tree0 (leaf ∷ st ) → tree ≡ tree0 +si-property0 {n} {A} {key} {.leaf} {.leaf} {.[]} (s-single .leaf) = refl +si-property0 {n} {A} {key} {.leaf} {tree0} {st} (s-right x si) = {!!} +si-property0 {n} {A} {key} {.leaf} {tree0} {st} (s-left x si) = {!!} + +si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack → stack-top stack ≡ just tree -si-property1 t t0 (x ∷ .[]) (s-single .x) = refl -si-property1 t t0 (t ∷ st) (s-right si) = refl -si-property1 t t0 (t ∷ st) (s-left si) = refl +si-property1 key t t0 (x ∷ .[]) (s-single .x) = refl +si-property1 key t t0 (t ∷ st) (s-right _ si) = refl +si-property1 key t t0 (t ∷ st) (s-left _ si) = refl -si-property-last : {n : Level} {A : Set n} (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant tree tree0 stack +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 t t0 (x ∷ []) (s-single .x) = refl -si-property-last t t0 (.t ∷ x ∷ st) (s-right si) with si-property1 _ _ (x ∷ st) si -... | refl = si-property-last x t0 (x ∷ st) si -si-property-last t t0 (.t ∷ x ∷ st) (s-left si) with si-property1 _ _ (x ∷ st) si -... | refl = si-property-last x t0 (x ∷ st) si +si-property-last key t t0 (x ∷ []) (s-single .x) = refl +si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si) with si-property1 key _ _ (x ∷ st) 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 key _ _ (x ∷ st) si +... | refl = si-property-last key x t0 (x ∷ st) si ti-right : {n : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} → treeInvariant (node key₁ v1 tree₁ repl) → treeInvariant repl ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf @@ -163,15 +168,15 @@ ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti -stackTreeInvariant : {n : Level} {A : Set n} (repl tree : bt A) → (stack : List (bt A)) - → treeInvariant tree → stackInvariant repl tree stack → treeInvariant repl -stackTreeInvariant repl .repl .(repl ∷ []) ti (s-single .repl) = ti -stackTreeInvariant {_} {A} repl tree (repl ∷ st) ti (s-right si) = ti-right (si1 si) where - si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant (node key₁ v1 tree₁ repl) tree st → treeInvariant (node key₁ v1 tree₁ repl) - si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant (node key₁ v1 tree₁ repl) tree st ti si -stackTreeInvariant {_} {A} repl tree (repl ∷ st) ti (s-left si) = ti-left ( si2 si ) where - si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant (node key₁ v1 repl tree₁ ) tree st → treeInvariant (node key₁ v1 repl tree₁ ) - si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant (node key₁ v1 repl tree₁ ) tree st ti si +stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (repl tree : bt A) → (stack : List (bt A)) + → treeInvariant tree → stackInvariant key repl tree stack → treeInvariant repl +stackTreeInvariant key repl .repl .(repl ∷ []) ti (s-single .repl) = ti +stackTreeInvariant {_} {A} key repl tree (repl ∷ st) ti (s-right _ si) = ti-right (si1 si) where + si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ repl) tree st → treeInvariant (node key₁ v1 tree₁ repl) + si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ repl) tree st ti si +stackTreeInvariant {_} {A} key repl tree (repl ∷ st) ti (s-left _ si) = ti-left ( si2 si ) where + si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 repl tree₁ ) tree st → treeInvariant (node key₁ v1 repl tree₁ ) + si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 repl tree₁ ) tree st ti si 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 () @@ -205,17 +210,17 @@ open _∧_ findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) - → treeInvariant tree ∧ stackInvariant tree tree0 stack - → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) - → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl) findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl) findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a (proj2 Pre) ⟫ depth-1< where - findP1 : key < key₁ → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree ∷ st) - findP1 a si = s-left si -findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right (proj2 Pre) ⟫ depth-2< + findP1 : key < key₁ → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st) + findP1 a si = s-left a si +findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2< replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁) @@ -232,34 +237,29 @@ replaceP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A) - → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant tree tree0 stack ∧ replacedTree key value tree repl + → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack ∧ replacedTree key value tree repl → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) - → treeInvariant tree0 ∧ stackInvariant tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) + → 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} repl [] Pre next exit = exit tree0 repl ⟪ proj1 Pre , {!!} ⟫ where - repleq : stackInvariant tree tree0 [] → tree ≡ tree0 - repleq = {!!} - repl7 : replacedTree key value tree repl → replacedTree key value tree0 repl - repl7 = {!!} -replaceP key value {tree0} {tree} repl (leaf ∷ st) Pre next exit with si-property1 _ _ _ (proj1 (proj2 Pre)) | rt-property1 _ _ _ _ (proj2 (proj2 Pre)) -... | refl | t1 = ⊥-elim ( t1 {!!} ) +replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) +... | () +replaceP key value {tree0} {tree} repl (leaf ∷ st) Pre next exit = {!!} 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 (node key₁ value₁ repl right ) st {!!} ≤-refl ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen repleq : tree0 ≡ node key₁ value₁ left right - repleq with si-property1 _ _ _ (proj1 (proj2 Pre)) + repleq with si-property1 _ _ _ _ (proj1 (proj2 Pre)) ... | refl = {!!} repl1 : treeInvariant (node key₁ value₁ left right) -- stackInvariant (node key₁ value₁ left right) tree st - repl1 = stackTreeInvariant _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre) + repl1 = stackTreeInvariant _ _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre) {!!} -- (subst (λ k → stackInvariant k tree (node key₁ value₁ left right ∷ st)) repleq (proj1 (proj2 Pre))) repl3 : replacedTree key value (node key₁ value₁ left right) (node key₁ value left right) repl3 = subst (λ k → replacedTree k value (node key₁ value₁ left right) (node key₁ value left right) ) (sym b) r-node ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl) st ⟪ proj1 Pre , ⟪ {!!} , r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where - repleq : repl ≡ node key₁ value₁ left right - repleq with si-property1 _ _ _ (proj1 (proj2 Pre)) - ... | refl = {!!} - repl2 : stackInvariant tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant (node key₁ value₁ left tree) tree0 st - repl2 = {!!} + repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st + repl2 (s-single .(node key₁ value₁ left right)) = {!!} + repl2 (s-right _ si) = {!!} + repl2 (s-left _ si) = {!!} --- ... next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl ) st ≤-refl where @@ -299,11 +299,11 @@ insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t insertTreeP {n} {m} {A} {t} tree key value P exit = - TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , {!!} ⟫ + TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , {!!} ⟫ $ λ p P loop → findP key (proj1 p) tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) $ λ t _ s P C → replaceNodeP key value t C (proj1 P) $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) - {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } + {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ ⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫ $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) {!!} (λ key value repl1 stack P2 lt → loop ⟪ stack , ⟪ {!!} , repl1 ⟫ ⟫ {!!} lt ) exit @@ -319,7 +319,7 @@ field tree0 : bt A ti : treeInvariant tree0 - si : stackInvariant tree tree0 stack + si : stackInvariant key tree tree0 stack ci : C tree stack -- data continuation findPP : {n m : Level} {A : Set n} {t : Set m} @@ -333,7 +333,7 @@ findPP {_} {_} {A} key n@(node key₁ v1 tree tree₁) st Pre next exit | tri< a ¬b ¬c = next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where tree0 = findPR.tree0 Pre - findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st → stackInvariant {!!} tree0 (node key₁ v1 tree tree₁ ∷ st) + findPP2 : (st : List (bt A)) → stackInvariant key {!!} tree0 st → stackInvariant key {!!} tree0 (node key₁ v1 tree tree₁ ∷ st) findPP2 = {!!} findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) findPP1 = depth-1< @@ -348,7 +348,7 @@ $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) $ λ t s _ P → replaceNodeP key value t {!!} {!!} $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) - {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } + {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ ⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) {!!} (λ key value repl1 stack P2 lt → loop ⟪ stack , ⟪ {!!} , repl1 ⟫ ⟫ {!!} lt ) exit @@ -380,6 +380,6 @@ lemma6 : (t1 : bt A) (s1 : List (bt A)) (found? : (t1 ≡ leaf) ∨ (node-key t1 ≡ just key)) (P2 : findPR key t1 s1 (findPC key value)) → top-value t1 ≡ just value lemma6 t1 s1 found? P2 = lemma7 t1 s1 (findPR.tree0 P2) ( findPC.tree1 (findPR.ci P2)) ( findPC.ci (findPR.ci P2)) (findPR.si P2) found? where lemma7 : (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A) → - replacedTree key value t1 tree1 → stackInvariant t1 tree0 s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value + replacedTree key value t1 tree1 → stackInvariant key t1 tree0 s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value lemma7 = {!!}