Mercurial > hg > Gears > GearsAgda
changeset 627:967547859521
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Nov 2021 23:17:35 +0900 |
| parents | 6465673df5bc |
| children | ec2506b532ba |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 29 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Mon Nov 08 22:45:19 2021 +0900 +++ b/hoareBinaryTree.agda Mon Nov 08 23:17:35 2021 +0900 @@ -98,26 +98,26 @@ treeInvariantTest1 : treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))) treeInvariantTest1 = {!!} -data stackInvariant {n : Level} {A : Set n} : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where - s-nil : stackInvariant leaf leaf [] - s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] ) +data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where + s-nil : stackInvariant key0 leaf leaf [] + s-single : (tree : bt A) → stackInvariant key0 tree tree (tree ∷ [] ) s-< : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} - → stackInvariant (node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant tree tree0 (tree ∷ node key value left tree ∷ st ) + → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st ) s-> : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} - → stackInvariant (node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant tree tree0 (tree ∷ node key value tree right ∷ st ) + → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ 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) r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) r-right : {k : ℕ } {v : A} → {t t1 t2 : bt A} - → k > key → ( replacedTree key value t1 t2 → replacedTree key value (node k v t t1) (node k v t t2) ) + → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v t t1) (node k v t t2) r-left : {k : ℕ } {v : A} → {t t1 t2 : bt A} - → k < key → ( replacedTree key value t1 t2 → replacedTree key value (node k v t1 t) (node k v t2 t) ) + → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v t1 t) (node k v t2 t) 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 → t ) → t + → 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 → t ) → t findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!} findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁ findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!} @@ -130,8 +130,8 @@ replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} replaceP : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant repl tree stack ∧ replacedTree key value tree repl - → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant repl tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree → t ) + → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant key repl tree stack ∧ replacedTree key value tree repl + → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key repl tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree → t ) → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t replaceP key value tree repl [] Pre next exit = exit tree repl {!!} replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!} @@ -175,11 +175,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 → replaceNodeP key value t (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 → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫ ⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫ $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit @@ -191,25 +191,25 @@ insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ insertTreeSpec0 _ _ _ = tt -record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where +record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where field tree0 : bt A ti : treeInvariant tree0 - si : stackInvariant tree tree0 stack + si : stackInvariant key tree tree0 stack ci : C tree stack findPP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) - → (Pre : findPR tree stack (λ t s → Lift n ⊤)) - → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t ) - → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t + → (Pre : findPR key tree stack (λ t s → Lift n ⊤)) + → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR key tree1 stack1 (λ t s → Lift n ⊤) → t) → t findPP key leaf st Pre next exit = exit leaf st (case1 refl) Pre findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (case2 {!!}) P findPP {_} {_} {A} key n@(node key₁ v 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₁ v tree tree₁ ∷ st) + findPP2 : (st : List (bt A)) → stackInvariant key {!!} tree0 st → stackInvariant key {!!} tree0 (node key₁ v tree tree₁ ∷ st) findPP2 = {!!} findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) findPP1 = {!!} @@ -220,11 +220,11 @@ insertTreePP : {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 insertTreePP {n} {m} {A} {t} tree key value P exit = - TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} + TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} 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 → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫ ⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit @@ -240,23 +240,19 @@ findPPC : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) - → (Pre : findPR tree stack findP-contains) - → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t ) - → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR tree1 stack1 findP-contains → t) → t + → (Pre : findPR key tree stack findP-contains) + → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR key tree1 stack1 findP-contains → t) → t findPPC = {!!} containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ containsTree {n} {m} {A} {t} tree tree1 key value P RT = TerminatingLoopS (bt A ∧ List (bt A) ) - {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) + {λ p → findPR key (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) ⟪ tree1 , [] ⟫ {!!} $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) - $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where + $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} {!!} found? ) where lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } → - replacedTree key value1 tree t1 → stackInvariant t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → node-key t1 ≡ just key - lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case1 ()) - lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case2 x) = x - lemma7 {.key₁} {value1} {.(node key₁ value1 s1 s2)} {node key₁ value s1 s2} r-node s or = {!!} - lemma7 {key} {value1} {.(node key₁ value s1 _)} {node key₁ value s1 s2} (r-right x r) s or = {!!} - lemma7 {key} {value1} {.(node key₁ value _ s2)} {node key₁ value s1 s2} (r-left x r) s or = {!!} + replacedTree key value1 tree t1 → stackInvariant key t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value + lemma7 = ?