Mercurial > hg > Gears > GearsAgda
changeset 586:0ddfa505d612
isolate search function problem, and add hoareBinaryTree.agda.
| author | ryokka |
|---|---|
| date | Wed, 04 Dec 2019 15:42:47 +0900 |
| parents | 42e8cf963c5c |
| children | f103f07c0552 |
| files | RedBlackTree.agda hoareBinaryTree.agda hoareRedBlackTree.agda logic.agda |
| diffstat | 4 files changed, 604 insertions(+), 88 deletions(-) [+] |
line wrap: on
line diff
--- a/RedBlackTree.agda Thu Nov 07 21:08:14 2019 +0900 +++ b/RedBlackTree.agda Wed Dec 04 15:42:47 2019 +0900 @@ -216,9 +216,9 @@ leafNode : {n : Level } { a : Set n } → a → (k : ℕ) → (Node a k) leafNode v k1 = record { key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red } -putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → {!!} → {!!} → (RedBlackTree {n} {m} {t} a k → t) → t +putRedBlackTree : {n m : Level} {t : Set m} {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} a k → ℕ → ℕ → (RedBlackTree {n} {m} {t} a k → t) → t putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next with (root tree) -putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | nothing = next (record tree {root = just (leafNode {!!} {!!}) }) +putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | nothing = next (record tree {root = just (leafNode val k1) }) putRedBlackTree {n} {m} {t} {a} {k} tree val k1 next | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode {!!} {!!}) n2 (λ tree1 s n1 → insertNode tree1 s n1 next)) -- putRedBlackTree {n} {m} {t} {a} {k} tree value k1 next with (root tree) -- ... | nothing = next (record tree {root = just (leafNode k1 value) }) @@ -285,6 +285,6 @@ -- test = (λ x → (createEmptyRedBlackTreeℕ x x) -ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0 +-- ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0 -- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/hoareBinaryTree.agda Wed Dec 04 15:42:47 2019 +0900 @@ -0,0 +1,116 @@ +module hoareBinaryTree where + +open import Level renaming (zero to Z ; suc to succ) + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp +open import Data.Maybe +open import Data.Maybe.Properties +open import Data.Empty +open import Data.List +open import Data.Product + +open import Function as F hiding (const) + +open import Relation.Binary +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary +open import logic + + +SingleLinkedStack = List + +emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data +emptySingleLinkedStack = [] + +clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t +clearSingleLinkedStack [] cg = cg [] +clearSingleLinkedStack (x ∷ as) cg = cg [] + +pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t +pushSingleLinkedStack stack datum next = next ( datum ∷ stack ) + +popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t +popSingleLinkedStack [] cs = cs [] nothing +popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1) + + + +data bt {n : Level} {a : Set n} : ℕ → ℕ → Set n where + bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt l u + bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) → + bt {n} {a} l' d → bt {n} {a} d u' → l ≤ l' → u' ≤ u → bt l u + +lleaf : {n : Level} {a : Set n} → bt {n} {a} 0 3 +lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) + +rleaf : {n : Level} {a : Set n} → bt {n} {a} 3 4 +rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3)) + +test-node : {n : Level} {a : Set n} → bt {n} {a} 0 4 +test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) + + + +_iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set +d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d)) + +iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y +iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ } + +-- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい +-- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる +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 +bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing +bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg with <-cmp key d +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 +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)) +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 + + +-- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう +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 +bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node + +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 +bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node + + +-- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) +-- up-some (just (fst , snd)) = just fst +-- up-some nothing = nothing + +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) +search-lem {n} {m} {a} {t} key (bt-leaf x) = refl +search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d +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₁ +search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl +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₂ + + +-- bt-find +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 + +find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing +find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d +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)) + +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 = + pushSingleLinkedStack st node + (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L {!!} {!!}) +-- bt が l u の2つの ℕ を受ける、この値はすべてのnodeによって異なるため stack に積むときに型が合わない + +-- find-support ⦃ ll' ⦄ ⦃ d ⦄ key L {!!} {!!}) + + +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 = {!!} + + +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 +bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st (λ cst → find-support key tr cst cg) + + + +-- 証明に insert がはいっててほしい +-- 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 +-- bt-insert = ?
--- a/hoareRedBlackTree.agda Thu Nov 07 21:08:14 2019 +0900 +++ b/hoareRedBlackTree.agda Wed Dec 04 15:42:47 2019 +0900 @@ -1,15 +1,18 @@ + module hoareRedBlackTree where -open import Level hiding (zero) +open import Level renaming (zero to Z ; suc to succ) open import Data.Nat hiding (compare) open import Data.Nat.Properties as NatProp open import Data.Maybe open import Data.Maybe.Properties --- open import Data.Bool open import Data.Empty open import Data.List +open import Data.Product + +open import Function as F hiding (const) open import Relation.Binary open import Relation.Binary.PropositionalEquality @@ -17,6 +20,7 @@ open import logic + record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where field putImpl : treeImpl → a → (treeImpl → t) → t @@ -39,7 +43,11 @@ emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data emptySingleLinkedStack = [] -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t +clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t +clearSingleLinkedStack [] cg = cg [] +clearSingleLinkedStack (x ∷ as) cg = cg [] + +pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t pushSingleLinkedStack stack datum next = next ( datum ∷ stack ) popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t @@ -64,8 +72,7 @@ field root : Maybe (Node a ) nodeStack : SingleLinkedStack (Node a ) - -- compare : k → k → Tri A B C - -- <-cmp + open RedBlackTree @@ -74,91 +81,463 @@ -- key : ℕ -- val : a -data BTree {n : Level} (a : Set n) : Set n where - leaf : BTree a - node : (left : BTree a) → (datum : ℕ) → (right : BTree a) → BTree a +-- leaf nodes key is 0. +-- +-- data BTree {n : Level} (a : Set n) (lk nk rk : ℕ) : Set n where +-- leaf : (l<n : lk < nk) → BTree a lk nk rk +-- node : (left : BTree a lk nk rk) +-- → (datum : ℕ) → (right : BTree a lk nk rk) +-- → BTree a lk nk rk + + +{-- tree に サイズ比較をつけたい(持ち運びたい)が leaf をどう扱うか問題(0にするとright についたときにおわる) +終わってほしくないので node のときだけにしたいがそれだと根本的に厳しい（BTree a の再帰構造なので） + + +--} + +-- data BTree {n : Level} (a : Set n) : Set n where +-- leaf : BTree a +-- node : (left : BTree a ) +-- → (datum : ℕ) +-- → (right : BTree a ) +-- → BTree a + +-- {a b c : ℕ} {a≤b : a ≤ b } {b≤c : b ≤ c} → +-- trans≤ : {n : Level} {a : Set n} → Trans {_} {_} {_} {_} {_} {_} {ℕ} {ℕ} {ℕ} (λ x y → x < y) (λ y z → y < z) (λ x z → (x < z)) -- a≤b b≤c +-- trans≤ {n} {a} {i} {j} {k} i<j j<k = ≤-trans i<j {!!} +-- with i <? k +-- trans≤ {n} {a} {i} {j} {k} i<j j<k | yes p = p +-- trans≤ {n} {a} {i} {j} {k} i<j j<k | no ¬p = {!!} + + +-- data BTree {n : Level} {a : Set n} (p q : ℕ) : ℕ → Set n where +-- leaf : (p<q : p ≤ q ) → BTree p q 0 +-- node : ∀ {hl hr h : ℕ} +-- → (key : ℕ) +-- → (left : BTree {n} {a} p key hl ) +-- → (right : BTree {n} {a} key q hr ) +-- → BTree p q (suc h) + +-- leaf-inj : {n : Level} {a : Set n} {p q : ℕ} {pp qq : p ≤ q} +-- → (leaf {n} {a} pp) ≡ (leaf qq) → pp ≡ qq +-- leaf-inj refl = refl + + + +-- node-inj : {n : Level} {a : Set n} +-- {k1 k2 h : ℕ} {l1 r1 : BTree {n} {a} h} {l2 r2 : BTree {n} {a} h} +-- → ((node {n} {a} {h} l1 k1 r1)) ≡ (node l2 k2 r2) → k1 ≡ k2 +-- node-inj refl = refl + +-- node-inj1 : {n : Level} {a : Set n} +-- {k1 k2 h hl1 hl2 hr1 hr2 p q : ℕ } +-- {l1 : BTree {n} {a} p k1 hl1 } {l2 : BTree {n} {a} p k2 hl2} {l1 : BTree {n} {a} k1 q hr1} {r2 : BTree {n} {a} k2 q hr2} +-- → (node {n} {a} {h} {?} {?} {?} {!!} {!!} ) ≡ (node {!!} {!!} {!!} ) → k1 ≡ k2 +-- node-inj1 as = {!!} -findT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t -findT leaf sd st next = next leaf st -findT (node ltree datum rtree) sd st next with <-cmp sd datum -findT tree@(node ltree datum rtree) sd st next | tri≈ ¬a b ¬c = next tree st -findT tree@(node ltree datum rtree) sd st next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findT ltree sd st2 next) -findT tree@(node ltree datum rtree) sd st next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findT rtree sd st2 next) +--- add relation find functions +-- fTree is start codeGear. findT2 is loop codeGear. +-- findT2 : {n m : Level } {a : Set n} {b lk rk kk1 kk2 : ℕ} {t : Set m} +-- → (k1<k2 : kk1 ≤ kk2) → BTree {n} {a} b lk rk → (key : ℕ) +-- → SingleLinkedStack (BTree {n} {a} b lk rk) +-- → ( (lk ≤ rk) → BTree {n} {a} b lk rk → SingleLinkedStack (BTree {n} {a} b lk rk) → t) → t +-- findT2 k1<k2 (leaf p<q) key stack cg = cg {!!} (leaf p<q) stack +-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg with <-cmp key1 key +-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri≈ ¬a b ¬c = {!!} +-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri< a ¬b ¬c = {!!} +-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri> ¬a ¬b c = {!!} + +-- cg k1<k2 (leaf p<q) stack +-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 lt) key stack cg with <-cmp key1 key +-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 tree@(node rt key1 lt) key stack cg | tri≈ ¬lt eq ¬gt = cg {!!} tree stack +-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri< lt ¬eq ¬gt = {!!} +-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri> ¬lt ¬eq gt = {!!} + + +-- fTree : {n m : Level } {a : Set n} {b k1 k2 : ℕ} {t : Set m} +-- → BTree {n} {a} b → (key : ℕ) +-- → SingleLinkedStack (BTree {n} {a} b) → ( k1 < k2 → BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t +-- fTree {n} {m} {a} {b} tree key stack cg = clearSingleLinkedStack stack (λ cstack → findT2 {n} {m} {a} {b} {0} {key} z≤n tree key cstack λ x x₁ x₂ → {!!}) + +{-- +そもそも Tree は 高さを受け取るのではなく 関係だけを持つ +leaf は関係を受け取って tran で (0 < n < m)をつくる +--} -testTreeType : {n : Level} {a : Set n} → BTree {n} a -testTreeType = (node (node leaf 1 leaf) 2 (node leaf 3 leaf)) +{-- 思いつき + Max Hight を持ち運んで必ず規定回数で止まるようにするのはあり…ｎきがする + Tree を作ったあとに 左右の最大 hight を比較して Max にするのは良い + 操作時はMaxが減る。 途中で終わった場合や、値が見つかった場合は + 受け取って Max を減らすだけの関数で既定回数数を減らすだけ + + 関数に持たせる?データに持たせる? + とりあえず関数(Data だと 再帰的な構造上定義が難しい) + +--} + +data BTree {n : Level} {a : Set n} : (hight : ℕ) → Set n where + leaf : {p q h : ℕ } → (p<q : p ≤ q ) → BTree (suc h) + node : { h : ℕ } + → (left : BTree {n} {a} (suc h) ) + → (key : ℕ) + → (right : BTree {n} {a} (suc h) ) + → BTree h --- findT testTreeType 44 [] (λ t st → t) --- leaf +maxHight : {n m : Level} {a : Set n} {t : Set m} {h : ℕ} → (searchHight : ℕ) → (BTree {n} {a} h) → ℕ +maxHight {n} {m} {a} {t} zero (leaf p<q) = 0 -- root is leaf +maxHight {n} {m} {a} {t} (suc hi) (leaf p<q) = (suc hi) -- max +maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) with (maxHight {n} {m} {a} {t} hi tree₁) | (maxHight {n} {m} {a} {t} hi tree₂) +... | lh | rh with <-cmp lh rh +maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri< a₁ ¬b ¬c = rh +maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri≈ ¬a b ¬c = lh +maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri> ¬a ¬b c = lh +-- maxHight {n} {m} {a} {t} hi (rnode tree₁ key₁ tree₂) = {!!} + --- findT testTreeType 44 [] (λ t st → st) --- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ [] +LastNodeIsLeaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool +LastNodeIsLeaf h (leaf p<q) P = true +LastNodeIsLeaf h (node rt k1 lt) P = (P rt k1 lt) /\ LastNodeIsLeaf (suc h) lt (λ _ z _ → P lt z lt) /\ LastNodeIsLeaf (suc h) rt λ _ z _ → P lt z lt + +-- allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool +-- allnodes leafEx p = true +-- allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p + +-- MaxHightStop? : {n : Level} {a : Set n} → {h : ℕ} → (hight : ℕ) → (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool +-- MaxHightStop? {n} {a} {.(suc _)} zero (leaf p<q) P = true +-- MaxHightStop? {n} {a} {.(suc _)} (suc allh) (leaf p<q) P = false +-- MaxHightStop? {n} {a} {h} zero (node lt k rt) P = false +-- MaxHightStop? {n} {a} {h} (suc allh) (node lt k rt) P = (P lt k lt) /\ (MaxHightStop? allh lt λ _ z _ → ) /\ (MaxHightStop? allh rt λ _ z _ → P rt z rt) + + +SearchLeaf : {n : Level} {a : Set n} → (h : ℕ) → (t : BTree {n} {a} h) → Bool +SearchLeaf h tree = LastNodeIsLeaf h tree (λ l k r → LastNodeIsLeaf (suc h) l (λ _ j _ → j <B? k) /\ LastNodeIsLeaf (suc h) r (λ _ n _ → k <B? n)) --- findT testTreeType 3 [] (λ t st → t) --- node leaf 3 leaf +{-- whats leaf relation...? +i think keys relation... +"leaf relation" maybe 0<"parent node key" ??? +--} +test : {n : Level} {a : Set n} {h : ℕ} → BTree {n} {a} h +test {n} {a} {h} = (node (leaf {n} {a} {0} {2} z≤n) 2 (node (leaf {n} {a} {0} {3} z≤n) 3 (leaf {n} {a} {0} {3} z≤n))) + +c : {n : Level} {a : Set n} → Bool +c {n} {a} = SearchLeaf {n} {a} 3 test + +cm : {n : Level} {a : Set n} → ℕ +cm {n} {a} = maxHight {n} {n} {a} {a} {zero} {!!} test + +lemma-all-leaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → SearchLeaf h tree ≡ true +lemma-all-leaf .(suc _) (leaf p<q) = refl +lemma-all-leaf h tt@(node pltree k1 rtree) = {!!} -- lemma-all-leaf h tt +-- lemma-all-leaf .0 tt@(rnode ltree k1 rtree) = lemma-all-leaf zero tt + +findT : {n m : Level } {a : Set n} {b left current : ℕ} {t : Set m} + → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ) + → SingleLinkedStack (BTree {n} {a} b) + → (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t +findT = {!!} --- findT testTreeType 3 [] (λ t st → st) --- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ [] +-- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st +-- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1 +-- findT l<c (node tree₁ key1 tree₂) key st cg | tri< a ¬b ¬c = {!!} +-- findT l<c (node tree₁ key1 tree₂) key st cg | tri≈ ¬a b ¬c = {!!} +-- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬a ¬b c = {!!} +-- -- findT l<c tree@(node ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st +-- findT {n} {m} {a} {b} {l} {cu} {?} l<c tree@(node {b} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = ? +-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {l} {cu} {!!} ({!!}) key st2 cg) +-- findT の {!!} の部分は trans したやつが入ってほしい(型が合わない) + + +--- nomal find +-- findT : {n m : Level } {a : Set n} {b left current : ℕ} {t : Set m} +-- → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ) +-- → SingleLinkedStack (BTree {n} {a} b) +-- → (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t + +-- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st +-- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1 +-- findT l<c tree@(node ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st + +-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node (leaf p<q) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → {!!}) -- findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} (leaf {n} {a} ⦃ !! ⦄ {cu} {!!}) key st2 cg) + +-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltt@(node ltree key₁ ltree₁) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} {!!} key st2 cg) + +-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {key} {key1} {!!} (rtree) key st2 cg) -replaceT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t -replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf) -replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree +-- findT l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st + +-- findT {n} {m} {a} {b} {l} l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = {!!} -- pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {lh} {rh} {h} {!!} ({!!}) key {!!} λ x x₁ → {!!}) +-- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬lt ¬eq gt = {!!} +-- findT (leaf p<q) key st cg = cg (leaf p<q ) st +-- findT (node tree₁ key₁ tree₂) key st cg with <-cmp key key₁ +-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri≈ ¬a b ¬c = cg tree st +-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri< a ¬b ¬c = {!!} +-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri> ¬a ¬b c = {!!} + -replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next +data BTreeEx {n : Level} {a : Set n} : Set n where + leafEx : BTreeEx + nodeEx :(left : BTreeEx {n} {a} ) + → (key : ℕ) + → (right : BTreeEx {n} {a} ) + → BTreeEx + + +cmpMax : ℕ → ℕ → ℕ +cmpMax lh rh with <-cmp lh rh +cmpMax lh rh | tri< a ¬b ¬c = rh +cmpMax lh rh | tri≈ ¬a b ¬c = lh +cmpMax lh rh | tri> ¬a ¬b c₁ = lh + + +max1 : {n m : Level} {a : Set n} {t : Set m} → ℕ → (BTreeEx {n} {a}) → (ℕ → t) → t +max1 {n} {m} {a} {t} hi leafEx cg = cg hi +max1 {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg = (max1 {n} {m} {a} {t} (suc hi) tree₁ + (λ lh → (max1 {n} {m} {a} {t} (suc hi) tree₂ (λ rh → cg (cmpMax lh rh))) )) -replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum -replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c = replaceT tree n0 rstack next -replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next -replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c = replaceT (node x datum (node leaf n0 leaf)) n0 rstack next +max : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → (ℕ → t) → t +max {n} {m} {a} {t} tree = max1 zero tree + + +maxI : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ℕ +maxI {n} {m} {a} {t} tree = max tree (λ x → x) + +-- bad proof +-- isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max 0 tr (λ n → n ≡ n)) +-- isStopMax? leafEx = refl +-- isStopMax? (nodeEx tree₁ key₁ tree₂) = {!!} + +isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max tr (λ eq → eq ≡ eq)) +isStopMax? leafEx = refl +isStopMax? (nodeEx tree₁ key₁ tree₂) = max (nodeEx tree₁ key₁ tree₂) (λ n₁ → {!!}) + +ltreeSearchLeaf : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ((BTreeEx {n} {a}) → t) → t +ltreeSearchLeaf leafEx cg = cg leafEx +ltreeSearchLeaf (nodeEx tree₁ key₁ tree₂) cg = ltreeSearchLeaf tree₁ cg + +ltreeStop? : {n m : Level} {a : Set n} {t : Set m} → (tree : BTreeEx {n} {a}) → ltreeSearchLeaf tree (λ tt → tt ≡ tt) +ltreeStop? leafEx = refl +ltreeStop? {n} {m} {a} {t} (nodeEx tree₁ key₁ tree₂) = ltreeStop? {n} {m} {a} {t} tree₁ + +ltreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t +ltreeSearchNode key leafEx cg = cg leafEx +ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁ +ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = ltreeSearchNode key tree₁ cg +ltreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt +ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = cg tree₂ + -replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next +-- 何らかの集合のサイズが減っていれば良い…？ +ltreeStoplem : {n m : Level} {a : Set n} {t : Set m} + → (key : ℕ) → (lt : BTreeEx {n} {a}) → (key1 : ℕ) → (rt : BTreeEx {n} {a}) → (p<q : key < key1 ) + → (ℕ → BTreeEx {n} {a} → t ) → t + +ltreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → ltreeSearchNode key tree (λ tt → tt ≡ tt) +ltreeNodeStop? key leafEx = refl +ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁ +ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = {!!} + +-- ltreeNodeStop? {!!} {!!} +{-- +Failed to solve the following constraints: +[720] ltreeSearchNode ?4 ?5 (λ tt → tt ≡ tt) +=< ltreeSearchNode key tree₁ (λ tt → tt ≡ tt) +: Set n +--} +ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl +ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = refl + + + +-- rtreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t +-- rtreeSearchNode key leafEx cg = cg leafEx +-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁ +-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = cg tree₂ +-- rtreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt +-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = rtreeSearchNode key tree₁ cg + + +-- rtreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → rtreeSearchNode key tree (λ tt → tt ≡ tt) +-- rtreeNodeStop? key leafEx = refl +-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁ +-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = refl +-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl +-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = rtreeNodeStop? key {!!} + + +ltreeStoplem key lt key1 rt p<q cg = cg key (nodeEx lt key1 rt) + + + --- bad some code -replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum -replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next - | tri≈ ¬a b ¬c = replaceT tree n0 rstack next -replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next - | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next -replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next - | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next +-- with (max {n} {m} {a} {t} (suc hi) tree₁ cg) | (max {n} {m} {a} {t} (suc hi) tree₂ cg) +-- ... | lh | rh = {!!} + +-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri< a₁ ¬b ¬c = cg rh +-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri≈ ¬a b ¬c = cg lh +-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri> ¬a ¬b c = cg lh + + +-- findStop : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t +-- findStop = {!!} + +findTEx : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t +findTEx leafEx sd st next = next leafEx st +findTEx (nodeEx ltree datum rtree) sd st next with <-cmp sd datum +findTEx tree@(nodeEx ltree datum rtree) sd st next | tri≈ ¬a b ¬c = next tree st +findTEx tree@(nodeEx ltree datum rtree) sd st next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findTEx ltree sd st2 next) +findTEx tree@(nodeEx ltree datum rtree) sd st next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findTEx rtree sd st2 next) -insertT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t -insertT tree n0 st next = findT tree n0 st ( λ new st2 → replaceT new n0 st2 next ) +findL : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t +findL leafEx key stack cg = cg leafEx stack +findL (nodeEx tree₁ key1 tree₂) key stack cg with (key1 ≤? key) +findL (nodeEx tree₁ key1 tree₂) key stack cg | yes p with key1 ≟ key +findL tree@(nodeEx tree₁ key1 tree₂) key stack cg | yes p | yes p₁ = cg tree stack +findL tree@(nodeEx ltree key1 tree₂) key stack cg | yes p | no ¬p = pushSingleLinkedStack stack tree (λ stack1 → findL ltree key stack1 cg) +findL (nodeEx tree₁ key1 tree₂) key stack cg | no ¬p = cg leafEx stack + + + +allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool +allnodes leafEx p = true +allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p + +find-leaf : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → Bool +find-leaf tree = allnodes tree (λ l k r → allnodes l (λ _ j _ → j <B? k) /\ allnodes r (λ _ n _ → k <B? n)) + +testTree : {n : Level} {a : Set n} → BTreeEx {n} {a} +testTree {n} {a} = (nodeEx (nodeEx leafEx 1 leafEx) 2 (nodeEx leafEx 3 (nodeEx (nodeEx leafEx 4 leafEx) 5 (nodeEx leafEx 6 leafEx)))) + +badTree : {n : Level} {a : Set n} → BTreeEx {n} {a} +badTree {n} {a} = (nodeEx (nodeEx leafEx 3 leafEx) 2 leafEx) + + + +lemm : {n : Level} {a : Set n} → find-leaf {n} {a} testTree ≡ true +lemm = refl -c1 : {n : Level} {a : Set n} → BTree {n} a -c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t)))) +bool-⊥ : true ≡ false → ⊥ +bool-⊥ () + +{-- badTree --} +-- lemm1 : {n : level} {a : set n} → find-leaf {n} {a} badtree ≡ true +-- lemm1 {n} {a} with badtree +-- lemm1 {n} {a} | leafex = {!!} +-- lemm1 {n} {a} | nodeex gda key₁ gda₁ = {!!} + +-- lemm-all : {n : Level} {a : Set n} (any-tree : BTreeEx {n} {a}) → find-leaf {n} {a} any-tree ≡ true +-- lemm-all leafEx = refl +-- lemm-all t@(nodeEx ltree k rtree) with (find-leaf t) ≟B true +-- lemm-all (nodeEx ltree k rtree) | yes p = p +-- lemm-all (nodeEx ltree k rtree) | no ¬p = {!!} + +-- findT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} {a} → (key : ℕ) → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t +-- findT = ? + +-- {-- +-- 一旦の方針は hight を使って書く, 大小関係 (片方だけ) を持って証明しながら降りてく +-- --} + + +-- hoge = findTEx testTree 44 [] (λ t s → s) -c2 : {n : Level} {a : Set n} → BTree {n} a -c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t)))) +-- {-- +-- Tree に対して l < x < r の条件を足すときに気になるのは l or r が leaf の場合 +-- leaf のときだけ例外的な証明を書く必要ありそう +-- --} + + +-- {-- AVL Tree メモ +-- - $AGDA-HOME/Data/AVL.agda 関連を眺めた Tips +-- AVL は特徴として すべての枝の長さの差が1以内に収まっている木。バランスもできる。 + +-- AVL Tree には key , value , left right の他にkeyの 上限、下限、高さを持ってるらしい +-- (後ろに付いてるのは高さ+- 1 の関係をもってる) + +-- cast operation は木のサイズの log になる +-- (cast operation は… わすれた) + +-- insert では 同じ key の値があったら Node を置き換え + + +-- --} + +-- -- findT testTreeType 44 [] (λ t st → t) +-- -- leaf + +-- -- findT testTree 44 [] (λ t st → st) +-- -- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ [] -getkey : {n : Level } {a : Set n} → BTree {n} a → Maybe ℕ -getkey leaf = nothing -getkey (node tree₁ datum tree₂) = just datum +-- -- findT testTreeType 3 [] (λ t st → t) +-- -- node leaf 3 leaf + +-- -- findT testTreeType 3 [] (λ t st → st) +-- -- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ [] + + +-- replaceT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t +-- replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf) +-- replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree + +-- replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next + + +-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum +-- replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c = replaceT tree n0 rstack next +-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next +-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c = replaceT (node x datum (node leaf n0 leaf)) n0 rstack next + + + +-- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next -find-insert : {n m : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (just key ≡ (getkey {n} return)))) -find-insert leaf key with <-cmp key key -find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a ) -find-insert leaf key | tri≈ ¬a b ¬c = refl -find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c ) -find-insert tr@(node any₁ datum any₂) key with <-cmp key datum -find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!} -find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!} -find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum -find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!} -find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!} -find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!} +-- -- bad some code +-- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum +-- replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next +-- | tri≈ ¬a b ¬c = replaceT tree n0 rstack next +-- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next +-- | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next +-- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next +-- | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next + +-- insertT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t +-- insertT tree n0 st next = findT tree n0 st ( λ new st2 → replaceT new n0 st2 next ) + + +-- c1 : {n : Level} {a : Set n} → BTree {n} a +-- c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t)))) + +-- c2 : {n : Level} {a : Set n} → BTree {n} a +-- c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t)))) --- where +-- -- -- 末 +-- -- findDownEnd : {n m : Level} {a : Set n} {t : Set m} → (find : ℕ) → (any : BTree a) → findT any find [] (λ tt stack → {!!}) +-- -- findDownEnd d tree = {!!} + +-- find-insert : {n m : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (key ≡ {!!}))) +-- find-insert leaf key with <-cmp key key +-- find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a ) +-- find-insert leaf key | tri≈ ¬a b ¬c = {!!} +-- find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c ) +-- find-insert tr@(node any₁ datum any₂) key with <-cmp key datum +-- find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!} +-- find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!} +-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum +-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!} +-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!} +-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!} + +-- -- where -- find-lemma : {n m : Level} {a : Set n} {t : Set m} → BTree a → ℕ → SingleLinkedStack (BTree a) → (BTree a → SingleLinkedStack (BTree a) → t) → t -- find-lemma leaf ke st nt = nt leaf st -- find-lemma (node tr datum tr₁) ke st nt with <-cmp ke datum @@ -198,7 +577,7 @@ node003 : Node ℕ node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black } -test001 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } ) +tes0t01 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } ) node001 ( λ tree → tree ) test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } ) node001 ( λ tree → tree ) @@ -253,28 +632,28 @@ -- fni-loop : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → FindNodeInvariant st original -findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) - → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t ) - → ( FindNodeInvariant (nodeStack tree) tree) → t -findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev - module FindNodeH where - findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree → t - findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev - findNode2h (just x) st n0 prev with <-cmp (key n0) (key x) - ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? ) - ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) ) - where - nextInvaliant : ({!!}) - nextInvaliant = {!!} - lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a) - lproof ns [] with left ns | right ns - lproof ns [] | just x | just x₁ = {!!} - lproof ns [] | just x | nothing = {!!} - lproof ns [] | nothing | just x = {!!} - lproof ns [] | nothing | nothing = {!!} - lproof ns (x ∷ ss) = {!!} +-- findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) +-- → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t ) +-- → ( FindNodeInvariant (nodeStack tree) tree) → t +-- findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev +-- module FindNodeH where +-- findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree → t +-- findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev +-- findNode2h (just x) st n0 prev with <-cmp (key n0) (key x) +-- ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) prev -- ( fni-Last ? ) +-- ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) ) +-- b where +-- nextInvaliant : (t) +-- nextInvaliant = next tree {!!} +-- lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a) +-- lproof ns [] with left ns | right ns +-- lproof ns [] | just x | just x₁ = {!!} +-- lproof ns [] | just x | nothing = {!!} +-- lproof ns [] | nothing | just x = {!!} +-- lproof ns [] | nothing | nothing = record { proj1 = refl ; proj2 = refl } +-- lproof ns (x ∷ ss) = {!!} - ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) ) +-- ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) ) -- replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t
--- a/logic.agda Thu Nov 07 21:08:14 2019 +0900 +++ b/logic.agda Wed Dec 04 15:42:47 2019 +0900 @@ -3,7 +3,10 @@ open import Level open import Relation.Nullary open import Relation.Binary +open import Relation.Binary.PropositionalEquality + open import Data.Empty +open import Data.Nat hiding (_⊔_) data Bool : Set where @@ -52,6 +55,24 @@ true /\ true = true _ /\ _ = false +_<B?_ : ℕ → ℕ → Bool +ℕ.zero <B? x = true +ℕ.suc x <B? ℕ.zero = false +ℕ.suc x <B? ℕ.suc xx = x <B? xx + +-- _<BT_ : ℕ → ℕ → Set +-- ℕ.zero <BT ℕ.zero = ⊤ +-- ℕ.zero <BT ℕ.suc b = ⊤ +-- ℕ.suc a <BT ℕ.zero = ⊥ +-- ℕ.suc a <BT ℕ.suc b = a <BT b + + +_≟B_ : Decidable {A = Bool} _≡_ +true ≟B true = yes refl +false ≟B false = yes refl +true ≟B false = no λ() +false ≟B true = no λ() + _\/_ : Bool → Bool → Bool false \/ false = false _ \/ _ = true