Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 587:f103f07c0552

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add insert code
author ryokka
date Thu, 05 Dec 2019 18:11:22 +0900
parents 0ddfa505d612
children 8627d35d4bff
comparison
equal deleted inserted replaced
586:0ddfa505d612 587:f103f07c0552
28 clearSingleLinkedStack (x ∷ as) cg = cg [] 28 clearSingleLinkedStack (x ∷ as) cg = cg []
29 29
30 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t 30 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
31 pushSingleLinkedStack stack datum next = next ( datum ∷ stack ) 31 pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
32 32
33
33 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t 34 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
34 popSingleLinkedStack [] cs = cs [] nothing 35 popSingleLinkedStack [] cs = cs [] nothing
35 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1) 36 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1)
36 37
37 38
38 39
39 data bt {n : Level} {a : Set n} : ℕ → ℕ → Set n where 40 emptySigmaStack : {n : Level } { Data : Set n} → List Data
40 bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt l u 41 emptySigmaStack = []
42
43 pushSigmaStack : {n m : Level} {d d2 : Set n} {t : Set m} → d2 → List d → (List (d × d2) → t) → t
44 pushSigmaStack {n} {m} {d} d2 st next = next (Data.List.zip (st) (d2 ∷ []) )
45
46 tt = pushSigmaStack 3 (true ∷ []) (λ st → st)
47
48 {--
49 data A B : C → D → Set where の A B と C → D の差は？
50
51 --}
52 data bt {n : Level} {a : Set n} : Set n where
53 bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt
41 bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) → 54 bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
42 bt {n} {a} l' d → bt {n} {a} d u' → l ≤ l' → u' ≤ u → bt l u 55 bt {n} {a} → bt {n} {a} → l ≤ l' → u' ≤ u → bt
43 56
44 lleaf : {n : Level} {a : Set n} → bt {n} {a} 0 3 57 lleaf : {n : Level} {a : Set n} → bt {n} {a}
45 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) 58 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
46 59
47 rleaf : {n : Level} {a : Set n} → bt {n} {a} 3 4 60 rleaf : {n : Level} {a : Set n} → bt {n} {a}
48 rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3)) 61 rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3))
49 62
50 test-node : {n : Level} {a : Set n} → bt {n} {a} 0 4 63 test-node : {n : Level} {a : Set n} → bt {n} {a}
51 test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) 64 test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
65
66 -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!}
67 -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) )
52 68
53 69
54 70
55 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set 71 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
56 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d)) 72 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
58 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y 74 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
59 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ } 75 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
60 76
61 -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい 77 -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
62 -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる 78 -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
63 bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} l u → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t 79 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
64 bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing 80 bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing
65 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg with <-cmp key d 81 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
66 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 82 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
67 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)) 83 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))
68 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 84 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
85
86 -- 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
87 -- 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))
88 -- 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
69 89
70 90
71 -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう 91 -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
72 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 92 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
73 bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node 93 bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node
78 98
79 -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) 99 -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ)
80 -- up-some (just (fst , snd)) = just fst 100 -- up-some (just (fst , snd)) = just fst
81 -- up-some nothing = nothing 101 -- up-some nothing = nothing
82 102
83 search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} l u) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata) 103 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)
84 search-lem {n} {m} {a} {t} key (bt-leaf x) = refl 104 search-lem {n} {m} {a} {t} key (bt-leaf x) = refl
85 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d 105 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d
86 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₁ 106 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₁
87 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl 107 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
88 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₂ 108 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₂
89 109
90 110
91 -- bt-find 111 -- bt-find
92 find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t 112 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
93 113
94 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing 114 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing
95 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d 115 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
96 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)) 116 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))
97 117
98 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 = 118 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 =
99 pushSingleLinkedStack st node 119 pushSingleLinkedStack st node
100 (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L {!!} {!!}) 120 (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)
101 -- bt が l u の2つの ℕ を受ける、この値はすべてのnodeによって異なるため stack に積むときに型が合わない 121
102 122 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
103 -- find-support ⦃ ll' ⦄ ⦃ d ⦄ key L {!!} {!!}) 123 (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
104 124
105 125 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
106 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 = {!!} 126 bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st
107 127 (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg)
108 128
109 bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t 129 find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ?
110 bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st (λ cst → find-support key tr cst cg) 130 find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st)
131 {-- result
132 λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ →
133 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)))) ∷ []
134 --}
135
136 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)
137 find-lem d (bt-leaf x) st = refl
138 find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁
139 find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl
140
141
142 find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c
143 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 {!!}
144 find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
145 find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
146
147 find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!}
148
149 bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t
150 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)
151
152
153 singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
154 singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x
155
156
157 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
158 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree
159 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
160 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₁
161 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
162 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
163 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
164
165 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case
166
167
168
169
170 bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄
171 → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} )
172 → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t
173
174 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
111 175
112 176
113 177
114 -- 証明に insert がはいっててほしい 178 -- 証明に insert がはいっててほしい
115 -- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → bt-search d tree (λ pt → ) → t 179 bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
116 -- bt-insert = ? 180 → ((bt {n} {a}) → t) → t
181
182 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 )
183
184 pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ
185 pickKey (bt-leaf x) = nothing
186 pickKey (bt-node d tree tree₁ x x₁) = just d
187
188 insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
189 insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x
190
191 insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
192 insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x
193
194
195 insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
196 → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 []
197 (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) )
198
199
200 insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!})
201 insert-lem d (bt-leaf x) | tri< a ¬b ¬c = ⊥-elim (¬b refl)
202 insert-lem d (bt-leaf x) | tri≈ ¬a b ¬c = refl
203 insert-lem d (bt-leaf x) | tri> ¬a ¬b c = ⊥-elim (¬b refl)
204 insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁
205 -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!})
206 insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d
207 insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
208 insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
209 insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
210
211 insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!}
212 where
213 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)))
214 lem-helper = {!!}
215
216 insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}
217