Gears/GearsAgda: hoareBinaryTree.agda annotate

annotate hoareBinaryTree.agda @ 611:db42d1033857

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 05 Nov 2021 09:21:38 +0900
parents	8239583dac0b
children	57d6c594da08

rev	line source
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	1 module hoareBinaryTree where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	2
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	3 open import Level renaming (zero to Z ; suc to succ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	4
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	5 open import Data.Nat hiding (compare)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	6 open import Data.Nat.Properties as NatProp
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	7 open import Data.Maybe
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	8 -- open import Data.Maybe.Properties
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	9 open import Data.Empty
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	10 open import Data.List
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	11 open import Data.Product
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	12
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	13 open import Function as F hiding (const)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	14
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	15 open import Relation.Binary
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	16 open import Relation.Binary.PropositionalEquality
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	17 open import Relation.Nullary
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	18 open import logic
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	19
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	20
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	21 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	22 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	23
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	24 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	25 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	26
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	27 --
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	28 --
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	29 -- no children , having left node , having right node , having both
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	30 --
597 89fd7cf09b2a fix ryokka parents: 596 diff changeset	31 data bt {n : Level} (A : Set n) : Set n where
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	32 leaf : bt A
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	33 node : (key : ℕ) → (value : A) →
610 8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	34 (left : bt A ) → (right : bt A ) → bt A
600 016a8deed93d fix old binary tree ryokka parents: 597 diff changeset	35
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	36 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	37 bt-depth leaf = 0
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	38 bt-depth (node key value t t₁) = Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )
606 61a0491a627b with Hoare condition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 605 diff changeset	39
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	40 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	41 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	42 find key leaf st _ exit = exit leaf st
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	43 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	44 find key n st _ exit \| tri≈ ¬a b ¬c = exit n st
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	45 find key n@(node key₁ v tree tree₁) st next _ \| tri< a ¬b ¬c = next tree (n ∷ st)
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	46 find key n@(node key₁ v tree tree₁) st next _ \| tri> ¬a ¬b c = next tree₁ (n ∷ st)
597 89fd7cf09b2a fix ryokka parents: 596 diff changeset	47
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	48 {-# TERMINATING #-}
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	49 find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	50 find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	51 find-loop1 : bt A → List (bt A) → t
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	52 find-loop1 tree st = find key tree st find-loop1 exit
600 016a8deed93d fix old binary tree ryokka parents: 597 diff changeset	53
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	54 replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	55 replaceNode k v leaf next = next (node k v leaf leaf)
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	56 replaceNode k v (node key value t t₁) next = next (node k v t t₁)
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	57
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	58 replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	59 replace key value tree [] next exit = exit tree
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	60 replace key value tree (leaf ∷ st) next exit = next key value tree st
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	61 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	62 ... \| tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	63 ... \| tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	64 ... \| tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	65
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	66 {-# TERMINATING #-}
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	67 replace-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	68 replace-loop {_} {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	69 replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t
2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	70 replace-loop1 key value tree st = replace key value tree st replace-loop1 exit
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	71
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	72 insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	73 insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	74
604 2075785a124a new approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 601 diff changeset	75 insertTest1 = insertTree leaf 1 1 (λ x → x )
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	76 insertTest2 = insertTree insertTest1 2 1 (λ x → x )
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	77
605 f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	78 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_)
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	79
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	80 treeInvariant : {n : Level} {A : Set n} → (tree : bt A) → Set
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	81 treeInvariant leaf = ⊤
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	82 treeInvariant (node key value leaf leaf) = ⊤
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	83 treeInvariant (node key value leaf n@(node key₁ value₁ t₁ t₂)) = (key < key₁) ∧ treeInvariant n
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	84 treeInvariant (node key value n@(node key₁ value₁ t t₁) leaf) = treeInvariant n ∧ (key < key₁)
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	85 treeInvariant (node key value n@(node key₁ value₁ t t₁) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n ∧ (key < key₁) ∧ (key₁ < key₂) ∧ treeInvariant m
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	86
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	87 treeInvariantTest1 = treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf)))
f8cc98fcc34b define invariant Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 604 diff changeset	88
610 8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	89 stackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack : List (bt A)) → Set n
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	90 stackInvariant {_} {A} _ [] = Lift _ ⊤
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	91 stackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	92 stackInvariant {_} {A} tree (x ∷ tail @ (node key value leaf right ∷ _) ) = (right ≡ x) ∧ stackInvariant tree tail
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	93 stackInvariant {_} {A} tree (x ∷ tail @ (node key value left leaf ∷ _) ) = (left ≡ x) ∧ stackInvariant tree tail
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	94 stackInvariant {_} {A} tree (x ∷ tail @ (node key value left right ∷ _ )) = ( (left ≡ x) ∧ stackInvariant tree tail) ∨ ( (right ≡ x) ∧ stackInvariant tree tail)
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	95 stackInvariant {_} {A} tree s = Lift _ ⊥
606 61a0491a627b with Hoare condition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 605 diff changeset	96
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	97 rstackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack : List (bt A)) → Set n
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	98 rstackInvariant {_} {A} _ [] = Lift _ ⊤
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	99 rstackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	100 rstackInvariant {_} {A} tree (node key value leaf right ∷ x ∷ y ) = (right ≡ x) ∧ rstackInvariant tree (x ∷ y)
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	101 rstackInvariant {_} {A} tree (node key value left leaf ∷ x ∷ y ) = (left ≡ x) ∧ rstackInvariant tree (x ∷ y)
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	102 rstackInvariant {_} {A} tree (node key value left right ∷ x ∷ y ) = ( (left ≡ x) ∧ rstackInvariant tree (x ∷ y)) ∨ ( (right ≡ x) ∧ rstackInvariant tree (x ∷ y))
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	103 rstackInvariant {_} {A} tree s = Lift _ ⊥
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	104
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	105 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
610 8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	106 → treeInvariant tree ∧ stackInvariant tree stack
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	107 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack → bt-depth tree1 < bt-depth tree → t )
8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	108 → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack → t ) → t
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	109 findP key leaf st Pre _ exit = exit leaf st {!!}
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	110 findP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	111 findP key n st Pre _ exit \| tri≈ ¬a b ¬c = exit n st {!!}
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	112 findP key n@(node key₁ v tree tree₁) st Pre next _ \| tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!}
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	113 findP key n@(node key₁ v tree tree₁) st Pre next _ \| tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!}
606 61a0491a627b with Hoare condition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 605 diff changeset	114
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	115 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	116 → ((tree : bt A) → treeInvariant tree → (rstack : List (bt A)) → rstackInvariant tree rstack → t) → t
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	117 replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} {!!}
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	118 replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} {!!}
606 61a0491a627b with Hoare condition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 605 diff changeset	119
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	120 replaceP : {n m : Level} {A : Set n} {t : Set m}
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	121 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree ∧ stackInvariant tree stack ∧ rstackInvariant tree rstack
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	122 → (next : ℕ → A → (tree1 repl : bt A) → (stack rstack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 stack ∧ rstackInvariant repl rstack → bt-depth tree1 < bt-depth tree → t )
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	123 → (exit : (tree1 repl : bt A) → (rstack : List (bt A)) → treeInvariant tree1 ∧ rstackInvariant repl rstack → t) → t
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	124 replaceP key value tree repl [] rs Pre next exit = exit tree repl {!!} {!!}
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	125 replaceP key value tree repl (leaf ∷ st) rs Pre next exit = next key value tree repl st {!!} {!!} {!!}
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	126 replaceP key value tree repl (node key₁ value₁ left right ∷ st) rs Pre next exit with <-cmp key key₁
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	127 ... \| tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) repl st {!!} {!!} {!!}
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	128 ... \| tri≈ ¬a b ¬c = next key value (node key₁ value left right ) repl st {!!} {!!} {!!}
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	129 ... \| tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) repl st {!!} {!!} {!!}
606 61a0491a627b with Hoare condition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 605 diff changeset	130
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	131 open import Relation.Binary.Definitions
606 61a0491a627b with Hoare condition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 605 diff changeset	132
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	133 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	134 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	135 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	136 lemma3 refl ()
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	137 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	138 lemma5 (s≤s z≤n) ()
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	139
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	140 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	141 → (r : Index) → (p : Invraiant r)
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	142 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	143 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	144 ... \| tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	145 ... \| tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	146 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	147 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	148 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	149 ... \| tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	150 ... \| tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	151 ... \| tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	152
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	153 open _∧_
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	154
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	155 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	156 → (exit : (tree repl : bt A) → (rstack : List (bt A)) → treeInvariant tree ∧ rstackInvariant repl rstack → t ) → t
610 8239583dac0b add one more stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 609 diff changeset	157 insertTreeP {n} {m} {A} {t} tree key value P exit =
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	158 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , lift tt ⟫
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	159 $ λ p P loop → findP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	160 $ λ t s P → replaceNodeP key value t (proj1 P)
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	161 $ λ t1 P1 r R → TerminatingLoopS (bt A ∧ List (bt A) ∧ List (bt A))
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	162 {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p)) ∧ rstackInvariant t1 (proj2 (proj2 p))}
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	163 (λ p → bt-depth (proj1 p)) ⟪ t , ⟪ s , r ⟫ ⟫　⟪ proj1 P , ⟪ proj2 P , R ⟫ ⟫
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	164 $ λ p P1 loop → replaceP key value (proj1 p) {!!} (proj1 (proj2 p)) (proj2 (proj2 p)) {!!} (λ k v t repl s s1 P2 lt → loop ⟪ t , ⟪ {!!} , s1 ⟫ ⟫ {!!} {!!} ) exit
609 79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	165
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	166 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	167 top-value leaf = nothing
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	168 top-value (node key value tree tree₁) = just value
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	169
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	170 insertTreeSpec0 : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	171 insertTreeSpec0 _ _ _ = tt
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	172
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	173 insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
79418701a283 add test and speciication Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 606 diff changeset	174 insertTreeSpec1 {n} {A} tree key value P =
611 db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	175 insertTreeP tree key value P (λ (tree₁ repl : bt A) (rstack : List (bt A))
db42d1033857 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 610 diff changeset	176 (P1 : treeInvariant tree₁ ∧ rstackInvariant repl rstack ) → insertTreeSpec0 tree₁ value {!!} )

Mercurial > hg > Gears > GearsAgda

annotate hoareBinaryTree.agda @ 611:db42d1033857