Gears/GearsAgda: hoareBinaryTree.agda annotate

annotate hoareBinaryTree.agda @ 596:4be84ddbf593

...

author	ryokka
date	Thu, 16 Jan 2020 17:53:47 +0900
parents	0927df986552
children	89fd7cf09b2a

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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	21 SingleLinkedStack = List
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	22
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	23 emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	24 emptySingleLinkedStack = []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	25
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	26 clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	27 clearSingleLinkedStack [] cg = cg []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	28 clearSingleLinkedStack (x ∷ as) cg = cg []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	29
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	30 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	31 pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	32
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	33
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	34 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	35 popSingleLinkedStack [] cs = cs [] nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	36 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	37
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	38
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	39
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	40 emptySigmaStack : {n : Level } { Data : Set n} → List Data
f103f07c0552 add insert code ryokka parents: 586 diff changeset	41 emptySigmaStack = []
f103f07c0552 add insert code ryokka parents: 586 diff changeset	42
f103f07c0552 add insert code ryokka parents: 586 diff changeset	43 pushSigmaStack : {n m : Level} {d d2 : Set n} {t : Set m} → d2 → List d → (List (d × d2) → t) → t
f103f07c0552 add insert code ryokka parents: 586 diff changeset	44 pushSigmaStack {n} {m} {d} d2 st next = next (Data.List.zip (st) (d2 ∷ []) )
f103f07c0552 add insert code ryokka parents: 586 diff changeset	45
f103f07c0552 add insert code ryokka parents: 586 diff changeset	46 tt = pushSigmaStack 3 (true ∷ []) (λ st → st)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	47
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	48 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	49 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	50
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	51 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	52 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	53
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	54
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	55 {--
f103f07c0552 add insert code ryokka parents: 586 diff changeset	56 data A B : C → D → Set where の A B と C → D の差は？
f103f07c0552 add insert code ryokka parents: 586 diff changeset	57
f103f07c0552 add insert code ryokka parents: 586 diff changeset	58 --}
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	59
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	60 data bt {n : Level} {a : Set n} : Set n where -- (a : Setn)
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	61 bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	62 bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	63 bt {n} {a} → bt {n} {a} → l ≤ l' → u' ≤ u → bt
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	64
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	65 --
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	66 --
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	67 -- no children , having left node , having right node , having both
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	68 --
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	69 data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) → Set n where -- (a : Setn)
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	70 bt'-leaf : (key : ℕ) → bt' A key
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	71 bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	72 bt' {n} {{!!}} {{!!}} A l → bt' {n} {{!!}} {{!!}} A r → l ≤ key → key ≤ r → bt' A key
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	73
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	74 data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn)
4be84ddbf593 ... ryokka parents: 595 diff changeset	75 bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key
4be84ddbf593 ... ryokka parents: 595 diff changeset	76 bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	77
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	78
593 063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	79 test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n)))
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	80
594 4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	81
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	82
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	83 -- reverse1 : List (bt' A tn) → List (bt' A tn) → List (bt' A tn)
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	84 -- reverse1 [] s1 = s1
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	85 -- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1)
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	86 -- ... \| as = {!!}
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	87
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	88 {--
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	89 find でステップ毎にみている node と stack の top を一致させる
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	90 find 中はnode と stack の top が一致する(root に来た時 stack top がなくなる)
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	91 -- どうやって経路の入ったstackを手に入れるか?(find 実行後でよい?)
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	92
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	93
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	94 tree+stack≡tree は find 後の tree と stack をもって
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	95 reverse した stack を使って find をチェックするかんじ?
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	96 --}
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	97
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	98
595 0927df986552 fix ryokka parents: 594 diff changeset	99 tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn )
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	100 → (stack : List (bt'-path A tn)) → Set n
4be84ddbf593 ... ryokka parents: 595 diff changeset	101 tree+stack tree mtree [] = tree ≡ mtree -- fin case
4be84ddbf593 ... ryokka parents: 595 diff changeset	102 tree+stack {n} {m} {A} {t} {.key₁} tree mtree@(bt'-leaf key₁) (bt'-left key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree {!!} stack)
4be84ddbf593 ... ryokka parents: 595 diff changeset	103 tree+stack {n} {m} {A} {t} {.key₁} tree mtree@(bt'-node {l} {r} key₁ value lmtree rmtree x₂ x₃) (bt'-left key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} {{!!}} tree {!!} stack)
4be84ddbf593 ... ryokka parents: 595 diff changeset	104 tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} {tn} tree {!!} stack)
595 0927df986552 fix ryokka parents: 594 diff changeset	105 -- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう
0927df986552 fix ryokka parents: 594 diff changeset	106
594 4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	107 tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn )
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	108 → (stack : List (bt'-path A tn)) → (reverse stack) ≡ {!!}
594 4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	109 tree+stack≡tree tree (bt'-leaf key) stack = {!!}
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	110 tree+stack≡tree tree (bt'-node key value mtree mtree₁ x x₁) stack = {!!}
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	111
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	112 bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn)
4be84ddbf593 ... ryokka parents: 595 diff changeset	113 → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t
589 37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	114 bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	115 bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
589 37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	116 bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next \| tri< a ¬b ¬c =
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	117 bt-find' key tree ( (bt'-left key {!!} ({!!}) ) ∷ {!!}) next
589 37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	118 bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next \| tri≈ ¬a b ¬c = next found stack
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	119 bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next \| tri> ¬a ¬b c =
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	120 bt-find' key tree ( (bt'-right key {!!} {!!} ) ∷ {!!}) next
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	121
594 4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	122
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	123 bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn)
4be84ddbf593 ... ryokka parents: 595 diff changeset	124 → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t
594 4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	125 bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	126 bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!}
4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	127
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	128 a<sa : { a : ℕ } → a < suc a
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	129 a<sa {zero} = s≤s z≤n
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	130 a<sa {suc a} = s≤s a<sa
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	131
592 7fb57243a8c9 fix ryokka parents: 591 diff changeset	132 a≤sa : { a : ℕ } → a ≤ suc a
7fb57243a8c9 fix ryokka parents: 591 diff changeset	133 a≤sa {zero} = z≤n
7fb57243a8c9 fix ryokka parents: 591 diff changeset	134 a≤sa {suc a} = s≤s a≤sa
7fb57243a8c9 fix ryokka parents: 591 diff changeset	135
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	136 pa<a : { a : ℕ } → pred (suc a) < suc a
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	137 pa<a {zero} = s≤s z≤n
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	138 pa<a {suc a} = s≤s pa<a
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	139
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	140 bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!})
594 4bbeb8d9e250 add comment ryokka parents: 593 diff changeset	141 → ({key1 : ℕ } → bt' A key1 → t ) → t
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	142 bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
596 4be84ddbf593 ... ryokka parents: 595 diff changeset	143 bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	144 bt-replace0 node [] = next node
592 7fb57243a8c9 fix ryokka parents: 591 diff changeset	145 bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!}
7fb57243a8c9 fix ryokka parents: 591 diff changeset	146 bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value node x₂ {!!} x₄ ) stack
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	147 bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	148 bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t
591 8ab2e2f9469f use <= Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 590 diff changeset	149 bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value
592 7fb57243a8c9 fix ryokka parents: 591 diff changeset	150 (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack
590 7c424dd0945d ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 589 diff changeset	151 bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	152
593 063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	153 tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	154 tree->key {n} {.key} (A) (bt'-leaf key) = key
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	155 tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	156
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	157
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	158 bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	159 bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) → (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1))
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	160
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	161
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	162 bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn )
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	163 → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	164 bt-replace-hoare key value tree stack = {!!}
063274f64a77 bt-replace-hoare kono parents: 592 diff changeset	165
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	166
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	167
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	168 -- find'-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → ( (bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	169
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	170 -- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt'-leaf x) st cg = cg leaf st nothing
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	171 -- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt'-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	172 -- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node d tree₁ tree₂ x x₁) st cg \| tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	173
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	174 -- find'-support {n} {m} {a} {t} key node@(bt'-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg \| tri< a₁ ¬b ¬c =
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	175 -- pushSingleLinkedStack st node
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	176 -- (λ st2 → find'-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	177
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	178 -- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg \| tri> ¬a ¬b c = pushSingleLinkedStack st node
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	179 -- (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	180
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	181
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	182
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	183 lleaf : {n : Level} {a : Set n} → bt {n} {a}
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	184 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	185
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	186 lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	187 lleaf1 0<3 a d = bt'-leaf d
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	188
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	189 test-node1 : bt' ℕ 3
591 8ab2e2f9469f use <= Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 590 diff changeset	190 test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!})))
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	191
8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	192
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	193 rleaf : {n : Level} {a : Set n} → bt {n} {a}
588 8627d35d4bff add data bt', and some function ryokka parents: 587 diff changeset	194 rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n))))
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	195
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	196 test-node : {n : Level} {a : Set n} → bt {n} {a}
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	197 test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	198
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	199 -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	200 -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) )
f103f07c0552 add insert code ryokka parents: 586 diff changeset	201
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	202
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	203
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	204 -- search の {{ l }} {{ u }} はその時みている node の大小。 l が小さく u が大きい
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	205 -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	206 bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	207 bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	208 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d
f103f07c0552 add insert code ryokka parents: 586 diff changeset	209 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg \| tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
f103f07c0552 add insert code ryokka parents: 586 diff changeset	210 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg \| tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
f103f07c0552 add insert code ryokka parents: 586 diff changeset	211 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg \| tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
f103f07c0552 add insert code ryokka parents: 586 diff changeset	212
f103f07c0552 add insert code ryokka parents: 586 diff changeset	213 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg \| tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
f103f07c0552 add insert code ryokka parents: 586 diff changeset	214 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg \| tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
f103f07c0552 add insert code ryokka parents: 586 diff changeset	215 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg \| tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	216
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	217
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	218 -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	219 bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	220 bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	221
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	222 bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	223 bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	224
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	225
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	226 -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	227 -- up-some (just (fst , snd)) = just fst
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	228 -- up-some nothing = nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	229
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	230 search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	231 search-lem {n} {m} {a} {t} key (bt-leaf x) = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	232 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	233 search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) \| tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	234 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) \| tri≈ ¬lt eq ¬gt = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	235 search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) \| tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	236
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	237
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	238 -- bt-find
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	239 find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	240
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	241 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	242 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	243 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg \| tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	244
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	245 find-support {n} {m} {a} {t} key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg \| tri< a₁ ¬b ¬c =
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	246 pushSingleLinkedStack st node
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	247 (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	248
f103f07c0552 add insert code ryokka parents: 586 diff changeset	249 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg \| tri> ¬a ¬b c = pushSingleLinkedStack st node
f103f07c0552 add insert code ryokka parents: 586 diff changeset	250 (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	251
f103f07c0552 add insert code ryokka parents: 586 diff changeset	252 bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
f103f07c0552 add insert code ryokka parents: 586 diff changeset	253 bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st
f103f07c0552 add insert code ryokka parents: 586 diff changeset	254 (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg)
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	255
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	256 find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ?
f103f07c0552 add insert code ryokka parents: 586 diff changeset	257 find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	258 {-- result
f103f07c0552 add insert code ryokka parents: 586 diff changeset	259 λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ →
f103f07c0552 add insert code ryokka parents: 586 diff changeset	260 bt-node 3 (bt-leaf z≤n) (bt-leaf (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ []
f103f07c0552 add insert code ryokka parents: 586 diff changeset	261 --}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	262
f103f07c0552 add insert code ryokka parents: 586 diff changeset	263 find-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	264 find-lem d (bt-leaf x) st = refl
f103f07c0552 add insert code ryokka parents: 586 diff changeset	265 find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁
f103f07c0552 add insert code ryokka parents: 586 diff changeset	266 find-lem d (bt-node d₁ tree tree₁ x x₁) st \| tri≈ ¬a b ¬c = refl
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	267
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	268
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	269 find-lem d (bt-node d₁ tree tree₁ x x₁) st \| tri< a ¬b ¬c with tri< a ¬b ¬c
f103f07c0552 add insert code ryokka parents: 586 diff changeset	270 find-lem {n} {m} {a} {t} {{l}} {{u}} d (bt-node d₁ tree tree₁ x x₁) st \| tri< lt ¬b ¬c \| tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	271 find-lem d (bt-node d₁ tree tree₁ x x₁) st \| tri< a ¬b ¬c \| tri≈ ¬a b ¬c₁ = {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	272 find-lem d (bt-node d₁ tree tree₁ x x₁) st \| tri< a ¬b ¬c \| tri> ¬a ¬b₁ c = {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	273
f103f07c0552 add insert code ryokka parents: 586 diff changeset	274 find-lem d (bt-node d₁ tree tree₁ x x₁) st \| tri> ¬a ¬b c = {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	275
f103f07c0552 add insert code ryokka parents: 586 diff changeset	276 bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t
f103f07c0552 add insert code ryokka parents: 586 diff changeset	277 bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	278
f103f07c0552 add insert code ryokka parents: 586 diff changeset	279
f103f07c0552 add insert code ryokka parents: 586 diff changeset	280 singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
f103f07c0552 add insert code ryokka parents: 586 diff changeset	281 singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	282
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	283
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	284 replace-helper : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t
f103f07c0552 add insert code ryokka parents: 586 diff changeset	285 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree
f103f07c0552 add insert code ryokka parents: 586 diff changeset	286 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(bt-node d L R x₁ x₂) (bt-leaf x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case
f103f07c0552 add insert code ryokka parents: 586 diff changeset	287 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁
f103f07c0552 add insert code ryokka parents: 586 diff changeset	288 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg \| tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
f103f07c0552 add insert code ryokka parents: 586 diff changeset	289 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg \| tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
f103f07c0552 add insert code ryokka parents: 586 diff changeset	290 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg \| tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg
f103f07c0552 add insert code ryokka parents: 586 diff changeset	291 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case
f103f07c0552 add insert code ryokka parents: 586 diff changeset	292
f103f07c0552 add insert code ryokka parents: 586 diff changeset	293
f103f07c0552 add insert code ryokka parents: 586 diff changeset	294
f103f07c0552 add insert code ryokka parents: 586 diff changeset	295 bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄
f103f07c0552 add insert code ryokka parents: 586 diff changeset	296 → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} )
f103f07c0552 add insert code ryokka parents: 586 diff changeset	297 → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t
f103f07c0552 add insert code ryokka parents: 586 diff changeset	298 bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	299
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	300
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	301
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: diff changeset	302 -- 証明に insert がはいっててほしい
587 f103f07c0552 add insert code ryokka parents: 586 diff changeset	303 bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
f103f07c0552 add insert code ryokka parents: 586 diff changeset	304 → ((bt {n} {a}) → t) → t
f103f07c0552 add insert code ryokka parents: 586 diff changeset	305
f103f07c0552 add insert code ryokka parents: 586 diff changeset	306 bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg )
f103f07c0552 add insert code ryokka parents: 586 diff changeset	307
f103f07c0552 add insert code ryokka parents: 586 diff changeset	308 pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ
f103f07c0552 add insert code ryokka parents: 586 diff changeset	309 pickKey (bt-leaf x) = nothing
f103f07c0552 add insert code ryokka parents: 586 diff changeset	310 pickKey (bt-node d tree tree₁ x x₁) = just d
f103f07c0552 add insert code ryokka parents: 586 diff changeset	311
f103f07c0552 add insert code ryokka parents: 586 diff changeset	312 insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
f103f07c0552 add insert code ryokka parents: 586 diff changeset	313 insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x
f103f07c0552 add insert code ryokka parents: 586 diff changeset	314
f103f07c0552 add insert code ryokka parents: 586 diff changeset	315 insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
f103f07c0552 add insert code ryokka parents: 586 diff changeset	316 insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x
f103f07c0552 add insert code ryokka parents: 586 diff changeset	317
f103f07c0552 add insert code ryokka parents: 586 diff changeset	318
f103f07c0552 add insert code ryokka parents: 586 diff changeset	319 insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
f103f07c0552 add insert code ryokka parents: 586 diff changeset	320 → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 []
f103f07c0552 add insert code ryokka parents: 586 diff changeset	321 (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) )
f103f07c0552 add insert code ryokka parents: 586 diff changeset	322
f103f07c0552 add insert code ryokka parents: 586 diff changeset	323
f103f07c0552 add insert code ryokka parents: 586 diff changeset	324 insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!})
f103f07c0552 add insert code ryokka parents: 586 diff changeset	325 insert-lem d (bt-leaf x) \| tri< a ¬b ¬c = ⊥-elim (¬b refl)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	326 insert-lem d (bt-leaf x) \| tri≈ ¬a b ¬c = refl
f103f07c0552 add insert code ryokka parents: 586 diff changeset	327 insert-lem d (bt-leaf x) \| tri> ¬a ¬b c = ⊥-elim (¬b refl)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	328 insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁
f103f07c0552 add insert code ryokka parents: 586 diff changeset	329 -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!})
f103f07c0552 add insert code ryokka parents: 586 diff changeset	330 insert-lem d (bt-node d₁ tree tree₁ x x₁) \| tri≈ ¬a b ¬c with <-cmp d d
f103f07c0552 add insert code ryokka parents: 586 diff changeset	331 insert-lem d (bt-node d₁ tree tree₁ x x₁) \| tri≈ ¬a b ¬c \| tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	332 insert-lem d (bt-node d₁ tree tree₁ x x₁) \| tri≈ ¬a b ¬c \| tri≈ ¬a₁ b₁ ¬c₁ = refl
f103f07c0552 add insert code ryokka parents: 586 diff changeset	333 insert-lem d (bt-node d₁ tree tree₁ x x₁) \| tri≈ ¬a b ¬c \| tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
f103f07c0552 add insert code ryokka parents: 586 diff changeset	334
f103f07c0552 add insert code ryokka parents: 586 diff changeset	335 insert-lem d (bt-node d₁ tree tree₁ x x₁) \| tri< a ¬b ¬c = {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	336 where
f103f07c0552 add insert code ryokka parents: 586 diff changeset	337 lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (bt-node d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (bt-node ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (bt-leaf ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d)))
f103f07c0552 add insert code ryokka parents: 586 diff changeset	338 lem-helper = {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	339
f103f07c0552 add insert code ryokka parents: 586 diff changeset	340 insert-lem d (bt-node d₁ tree tree₁ x x₁) \| tri> ¬a ¬b c = {!!}
f103f07c0552 add insert code ryokka parents: 586 diff changeset	341

Mercurial > hg > Gears > GearsAgda

annotate hoareBinaryTree.agda @ 596:4be84ddbf593