Gears/GearsAgda: hoareRedBlackTree.agda annotate

annotate hoareRedBlackTree.agda @ 589:37f5826ca7d2

minor fix

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 06 Dec 2019 13:01:53 +0900
parents	8627d35d4bff
children

rev	line source
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	1
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	2 module hoareRedBlackTree where
40d01b368e34 Temporary Push ryokka parents: diff changeset	3
40d01b368e34 Temporary Push ryokka parents: diff changeset	4
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	5 open import Level renaming (zero to Z ; suc to succ)
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	6
40d01b368e34 Temporary Push ryokka parents: diff changeset	7 open import Data.Nat hiding (compare)
40d01b368e34 Temporary Push ryokka parents: diff changeset	8 open import Data.Nat.Properties as NatProp
40d01b368e34 Temporary Push ryokka parents: diff changeset	9 open import Data.Maybe
588 8627d35d4bff add data bt', and some function ryokka parents: 586 diff changeset	10 -- open import Data.Maybe.Properties
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	11 open import Data.Empty
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	12 open import Data.List
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	13 open import Data.Product
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	14
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	15 open import Function as F hiding (const)
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	16
40d01b368e34 Temporary Push ryokka parents: diff changeset	17 open import Relation.Binary
40d01b368e34 Temporary Push ryokka parents: diff changeset	18 open import Relation.Binary.PropositionalEquality
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	19 open import Relation.Nullary
579 821d04c0770b ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 578 diff changeset	20 open import logic
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	21
40d01b368e34 Temporary Push ryokka parents: diff changeset	22
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	23
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	24 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
40d01b368e34 Temporary Push ryokka parents: diff changeset	25 field
40d01b368e34 Temporary Push ryokka parents: diff changeset	26 putImpl : treeImpl → a → (treeImpl → t) → t
40d01b368e34 Temporary Push ryokka parents: diff changeset	27 getImpl : treeImpl → (treeImpl → Maybe a → t) → t
40d01b368e34 Temporary Push ryokka parents: diff changeset	28 open TreeMethods
40d01b368e34 Temporary Push ryokka parents: diff changeset	29
40d01b368e34 Temporary Push ryokka parents: diff changeset	30 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
40d01b368e34 Temporary Push ryokka parents: diff changeset	31 field
40d01b368e34 Temporary Push ryokka parents: diff changeset	32 tree : treeImpl
40d01b368e34 Temporary Push ryokka parents: diff changeset	33 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
40d01b368e34 Temporary Push ryokka parents: diff changeset	34 putTree : a → (Tree treeImpl → t) → t
40d01b368e34 Temporary Push ryokka parents: diff changeset	35 putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
40d01b368e34 Temporary Push ryokka parents: diff changeset	36 getTree : (Tree treeImpl → Maybe a → t) → t
40d01b368e34 Temporary Push ryokka parents: diff changeset	37 getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
40d01b368e34 Temporary Push ryokka parents: diff changeset	38
40d01b368e34 Temporary Push ryokka parents: diff changeset	39 open Tree
40d01b368e34 Temporary Push ryokka parents: diff changeset	40
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	41 SingleLinkedStack = List
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	42
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	43 emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	44 emptySingleLinkedStack = []
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	45
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	46 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: 585 diff changeset	47 clearSingleLinkedStack [] cg = cg []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	48 clearSingleLinkedStack (x ∷ as) cg = cg []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	49
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	50 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	51 pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	52
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	53 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	54 popSingleLinkedStack [] cs = cs [] nothing
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	55 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	56
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	57 data Color {n : Level } : Set n where
40d01b368e34 Temporary Push ryokka parents: diff changeset	58 Red : Color
40d01b368e34 Temporary Push ryokka parents: diff changeset	59 Black : Color
40d01b368e34 Temporary Push ryokka parents: diff changeset	60
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	61 record Node {n : Level } (a : Set n) : Set n where
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	62 inductive
40d01b368e34 Temporary Push ryokka parents: diff changeset	63 field
40d01b368e34 Temporary Push ryokka parents: diff changeset	64 key : ℕ
40d01b368e34 Temporary Push ryokka parents: diff changeset	65 value : a
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	66 right : Maybe (Node a )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	67 left : Maybe (Node a )
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	68 color : Color {n}
40d01b368e34 Temporary Push ryokka parents: diff changeset	69 open Node
40d01b368e34 Temporary Push ryokka parents: diff changeset	70
580 99429fdb3b8b ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 579 diff changeset	71 record RedBlackTree {n : Level } (a : Set n) : Set n where
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	72 field
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	73 root : Maybe (Node a )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	74 nodeStack : SingleLinkedStack (Node a )
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	75
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	76
40d01b368e34 Temporary Push ryokka parents: diff changeset	77 open RedBlackTree
40d01b368e34 Temporary Push ryokka parents: diff changeset	78
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	79 -- record datum {n : Level} (a : Set n) : Set n where
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	80 -- field
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	81 -- key : ℕ
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	82 -- val : a
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	83
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	84 -- leaf nodes key is 0.
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	85 --
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	86 -- data BTree {n : Level} (a : Set n) (lk nk rk : ℕ) : Set n where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	87 -- leaf : (l<n : lk < nk) → BTree a lk nk rk
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	88 -- node : (left : BTree a lk nk rk)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	89 -- → (datum : ℕ) → (right : BTree a lk nk rk)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	90 -- → BTree a lk nk rk
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	91
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	92
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	93 {-- tree にサイズ比較をつけたい(持ち運びたい)が leaf をどう扱うか問題(0にするとright についたときにおわる)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	94 終わってほしくないので node のときだけにしたいがそれだと根本的に厳しい（BTree a の再帰構造なので）
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	95
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	96
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	97 --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	98
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	99 -- data BTree {n : Level} (a : Set n) : Set n where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	100 -- leaf : BTree a
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	101 -- node : (left : BTree a )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	102 -- → (datum : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	103 -- → (right : BTree a )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	104 -- → BTree a
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	105
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	106 -- {a b c : ℕ} {a≤b : a ≤ b } {b≤c : b ≤ c} →
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	107 -- trans≤ : {n : Level} {a : Set n} → Trans {_} {_} {_} {_} {_} {_} {ℕ} {ℕ} {ℕ} (λ x y → x < y) (λ y z → y < z) (λ x z → (x < z)) -- a≤b b≤c
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	108 -- trans≤ {n} {a} {i} {j} {k} i<j j<k = ≤-trans i<j {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	109 -- with i <? k
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	110 -- trans≤ {n} {a} {i} {j} {k} i<j j<k \| yes p = p
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	111 -- trans≤ {n} {a} {i} {j} {k} i<j j<k \| no ¬p = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	112
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	113
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	114 -- data BTree {n : Level} {a : Set n} (p q : ℕ) : ℕ → Set n where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	115 -- leaf : (p<q : p ≤ q ) → BTree p q 0
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	116 -- node : ∀ {hl hr h : ℕ}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	117 -- → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	118 -- → (left : BTree {n} {a} p key hl )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	119 -- → (right : BTree {n} {a} key q hr )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	120 -- → BTree p q (suc h)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	121
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	122 -- leaf-inj : {n : Level} {a : Set n} {p q : ℕ} {pp qq : p ≤ q}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	123 -- → (leaf {n} {a} pp) ≡ (leaf qq) → pp ≡ qq
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	124 -- leaf-inj refl = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	125
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	126
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	127
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	128 -- node-inj : {n : Level} {a : Set n}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	129 -- {k1 k2 h : ℕ} {l1 r1 : BTree {n} {a} h} {l2 r2 : BTree {n} {a} h}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	130 -- → ((node {n} {a} {h} l1 k1 r1)) ≡ (node l2 k2 r2) → k1 ≡ k2
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	131 -- node-inj refl = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	132
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	133 -- node-inj1 : {n : Level} {a : Set n}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	134 -- {k1 k2 h hl1 hl2 hr1 hr2 p q : ℕ }
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	135 -- {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}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	136 -- → (node {n} {a} {h} {?} {?} {?} {!!} {!!} ) ≡ (node {!!} {!!} {!!} ) → k1 ≡ k2
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	137 -- node-inj1 as = {!!}
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	138
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	139
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	140
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	141 --- add relation find functions
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	142 -- fTree is start codeGear. findT2 is loop codeGear.
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	143 -- findT2 : {n m : Level } {a : Set n} {b lk rk kk1 kk2 : ℕ} {t : Set m}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	144 -- → (k1<k2 : kk1 ≤ kk2) → BTree {n} {a} b lk rk → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	145 -- → SingleLinkedStack (BTree {n} {a} b lk rk)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	146 -- → ( (lk ≤ rk) → BTree {n} {a} b lk rk → SingleLinkedStack (BTree {n} {a} b lk rk) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	147 -- findT2 k1<k2 (leaf p<q) key stack cg = cg {!!} (leaf p<q) stack
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	148 -- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg with <-cmp key1 key
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	149 -- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg \| tri≈ ¬a b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	150 -- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg \| tri< a ¬b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	151 -- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg \| tri> ¬a ¬b c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	152
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	153 -- cg k1<k2 (leaf p<q) stack
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	154 -- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 lt) key stack cg with <-cmp key1 key
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	155 -- 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	156 -- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg \| tri< lt ¬eq ¬gt = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	157 -- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg \| tri> ¬lt ¬eq gt = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	158
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	159
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	160 -- fTree : {n m : Level } {a : Set n} {b k1 k2 : ℕ} {t : Set m}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	161 -- → BTree {n} {a} b → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	162 -- → SingleLinkedStack (BTree {n} {a} b) → ( k1 < k2 → BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	163 -- 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₂ → {!!})
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	164
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	165 {--
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	166 そもそも Tree は高さを受け取るのではなく関係だけを持つ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	167 leaf は関係を受け取って tran で (0 < n < m)をつくる
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	168 --}
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	169
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	170
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	171 {-- 思いつき
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	172 Max Hight を持ち運んで必ず規定回数で止まるようにするのはあり…ｎきがする
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	173 Tree を作ったあとに左右の最大 hight を比較して Max にするのは良い
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	174 操作時はMaxが減る。途中で終わった場合や、値が見つかった場合は
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	175 受け取って Max を減らすだけの関数で既定回数数を減らすだけ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	176
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	177 関数に持たせる?データに持たせる?
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	178 とりあえず関数(Data だと再帰的な構造上定義が難しい)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	179
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	180 --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	181
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	182 data BTree {n : Level} {a : Set n} : (hight : ℕ) → Set n where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	183 leaf : {p q h : ℕ } → (p<q : p ≤ q ) → BTree (suc h)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	184 node : { h : ℕ }
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	185 → (left : BTree {n} {a} (suc h) )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	186 → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	187 → (right : BTree {n} {a} (suc h) )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	188 → BTree h
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	189
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	190 maxHight : {n m : Level} {a : Set n} {t : Set m} {h : ℕ} → (searchHight : ℕ) → (BTree {n} {a} h) → ℕ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	191 maxHight {n} {m} {a} {t} zero (leaf p<q) = 0 -- root is leaf
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	192 maxHight {n} {m} {a} {t} (suc hi) (leaf p<q) = (suc hi) -- max
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	193 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₂)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	194 ... \| lh \| rh with <-cmp lh rh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	195 maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) \| lh \| rh \| tri< a₁ ¬b ¬c = rh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	196 maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) \| lh \| rh \| tri≈ ¬a b ¬c = lh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	197 maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) \| lh \| rh \| tri> ¬a ¬b c = lh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	198 -- maxHight {n} {m} {a} {t} hi (rnode tree₁ key₁ tree₂) = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	199
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	200
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	201 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	202 LastNodeIsLeaf h (leaf p<q) P = true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	203 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	204
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	205 -- allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	206 -- allnodes leafEx p = true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	207 -- allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	208
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	209 -- 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	210 -- MaxHightStop? {n} {a} {.(suc _)} zero (leaf p<q) P = true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	211 -- MaxHightStop? {n} {a} {.(suc _)} (suc allh) (leaf p<q) P = false
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	212 -- MaxHightStop? {n} {a} {h} zero (node lt k rt) P = false
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	213 -- 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)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	214
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	215
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	216 SearchLeaf : {n : Level} {a : Set n} → (h : ℕ) → (t : BTree {n} {a} h) → Bool
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	217 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))
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	218
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	219
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	220 {-- whats leaf relation...?
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	221 i think keys relation...
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	222 "leaf relation" maybe 0<"parent node key" ???
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	223 --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	224 test : {n : Level} {a : Set n} {h : ℕ} → BTree {n} {a} h
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	225 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)))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	226
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	227 c : {n : Level} {a : Set n} → Bool
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	228 c {n} {a} = SearchLeaf {n} {a} 3 test
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	229
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	230 cm : {n : Level} {a : Set n} → ℕ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	231 cm {n} {a} = maxHight {n} {n} {a} {a} {zero} {!!} test
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	232
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	233 lemma-all-leaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → SearchLeaf h tree ≡ true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	234 lemma-all-leaf .(suc _) (leaf p<q) = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	235 lemma-all-leaf h tt@(node pltree k1 rtree) = {!!} -- lemma-all-leaf h tt
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	236 -- lemma-all-leaf .0 tt@(rnode ltree k1 rtree) = lemma-all-leaf zero tt
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	237
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	238 findT : {n m : Level } {a : Set n} {b left current : ℕ} {t : Set m}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	239 → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	240 → SingleLinkedStack (BTree {n} {a} b)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	241 → (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	242 findT = {!!}
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	243
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	244 -- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	245 -- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	246 -- findT l<c (node tree₁ key1 tree₂) key st cg \| tri< a ¬b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	247 -- findT l<c (node tree₁ key1 tree₂) key st cg \| tri≈ ¬a b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	248 -- findT l<c (node tree₁ key1 tree₂) key st cg \| tri> ¬a ¬b c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	249 -- -- findT l<c tree@(node ltree key1 rtree) key st cg \| tri≈ ¬lt eq ¬gt = cg tree st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	250 -- findT {n} {m} {a} {b} {l} {cu} {?} l<c tree@(node {b} ltree key1 rtree) key st cg \| tri< lt ¬eq ¬gt = ?
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	251 -- 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)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	252 -- findT の {!!} の部分は trans したやつが入ってほしい(型が合わない)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	253
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	254
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	255 --- nomal find
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	256 -- findT : {n m : Level } {a : Set n} {b left current : ℕ} {t : Set m}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	257 -- → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	258 -- → SingleLinkedStack (BTree {n} {a} b)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	259 -- → (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	260
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	261 -- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	262 -- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	263 -- findT l<c tree@(node ltree key1 rtree) key st cg \| tri≈ ¬lt eq ¬gt = cg tree st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	264
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	265 -- 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)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	266
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	267 -- 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)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	268
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	269 -- 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)
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	270
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	271
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	272 -- findT l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg \| tri≈ ¬lt eq ¬gt = cg tree st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	273
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	274 -- 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₁ → {!!})
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	275 -- findT l<c (node tree₁ key1 tree₂) key st cg \| tri> ¬lt ¬eq gt = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	276 -- findT (leaf p<q) key st cg = cg (leaf p<q ) st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	277 -- findT (node tree₁ key₁ tree₂) key st cg with <-cmp key key₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	278 -- findT tree@(node tree₁ key₁ tree₂) key st cg \| tri≈ ¬a b ¬c = cg tree st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	279 -- findT tree@(node tree₁ key₁ tree₂) key st cg \| tri< a ¬b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	280 -- findT tree@(node tree₁ key₁ tree₂) key st cg \| tri> ¬a ¬b c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	281
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	282
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	283 data BTreeEx {n : Level} {a : Set n} : Set n where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	284 leafEx : BTreeEx
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	285 nodeEx :(left : BTreeEx {n} {a} )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	286 → (key : ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	287 → (right : BTreeEx {n} {a} )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	288 → BTreeEx
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	289
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	290
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	291 cmpMax : ℕ → ℕ → ℕ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	292 cmpMax lh rh with <-cmp lh rh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	293 cmpMax lh rh \| tri< a ¬b ¬c = rh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	294 cmpMax lh rh \| tri≈ ¬a b ¬c = lh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	295 cmpMax lh rh \| tri> ¬a ¬b c₁ = lh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	296
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	297
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	298 max1 : {n m : Level} {a : Set n} {t : Set m} → ℕ → (BTreeEx {n} {a}) → (ℕ → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	299 max1 {n} {m} {a} {t} hi leafEx cg = cg hi
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	300 max1 {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg = (max1 {n} {m} {a} {t} (suc hi) tree₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	301 (λ lh → (max1 {n} {m} {a} {t} (suc hi) tree₂ (λ rh → cg (cmpMax lh rh))) ))
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	302
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	303
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	304 max : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → (ℕ → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	305 max {n} {m} {a} {t} tree = max1 zero tree
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	306
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	307
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	308 maxI : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ℕ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	309 maxI {n} {m} {a} {t} tree = max tree (λ x → x)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	310
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	311 -- bad proof
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	312 -- isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max 0 tr (λ n → n ≡ n))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	313 -- isStopMax? leafEx = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	314 -- isStopMax? (nodeEx tree₁ key₁ tree₂) = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	315
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	316 isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max tr (λ eq → eq ≡ eq))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	317 isStopMax? leafEx = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	318 isStopMax? (nodeEx tree₁ key₁ tree₂) = max (nodeEx tree₁ key₁ tree₂) (λ n₁ → {!!})
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	319
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	320 ltreeSearchLeaf : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ((BTreeEx {n} {a}) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	321 ltreeSearchLeaf leafEx cg = cg leafEx
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	322 ltreeSearchLeaf (nodeEx tree₁ key₁ tree₂) cg = ltreeSearchLeaf tree₁ cg
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	323
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	324 ltreeStop? : {n m : Level} {a : Set n} {t : Set m} → (tree : BTreeEx {n} {a}) → ltreeSearchLeaf tree (λ tt → tt ≡ tt)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	325 ltreeStop? leafEx = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	326 ltreeStop? {n} {m} {a} {t} (nodeEx tree₁ key₁ tree₂) = ltreeStop? {n} {m} {a} {t} tree₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	327
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	328 ltreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	329 ltreeSearchNode key leafEx cg = cg leafEx
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	330 ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	331 ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg \| tri< a ¬b ¬c = ltreeSearchNode key tree₁ cg
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	332 ltreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg \| tri≈ ¬a b ¬c = cg tt
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	333 ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg \| tri> ¬a ¬b c₁ = cg tree₂
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	334
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	335
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	336
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	337
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	338 -- 何らかの集合のサイズが減っていれば良い…？
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	339 ltreeStoplem : {n m : Level} {a : Set n} {t : Set m}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	340 → (key : ℕ) → (lt : BTreeEx {n} {a}) → (key1 : ℕ) → (rt : BTreeEx {n} {a}) → (p<q : key < key1 )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	341 → (ℕ → BTreeEx {n} {a} → t ) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	342
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	343 ltreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → ltreeSearchNode key tree (λ tt → tt ≡ tt)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	344 ltreeNodeStop? key leafEx = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	345 ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	346 ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) \| tri< a ¬b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	347
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	348 -- ltreeNodeStop? {!!} {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	349 {--
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	350 Failed to solve the following constraints:
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	351 [720] ltreeSearchNode ?4 ?5 (λ tt → tt ≡ tt)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	352 =< ltreeSearchNode key tree₁ (λ tt → tt ≡ tt)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	353 : Set n
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	354 --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	355 ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) \| tri≈ ¬a b ¬c = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	356 ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) \| tri> ¬a ¬b c₁ = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	357
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	358
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	359
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	360 -- rtreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	361 -- rtreeSearchNode key leafEx cg = cg leafEx
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	362 -- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	363 -- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg \| tri< a ¬b ¬c = cg tree₂
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	364 -- rtreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg \| tri≈ ¬a b ¬c = cg tt
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	365 -- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg \| tri> ¬a ¬b c₁ = rtreeSearchNode key tree₁ cg
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	366
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	367
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	368 -- rtreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → rtreeSearchNode key tree (λ tt → tt ≡ tt)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	369 -- rtreeNodeStop? key leafEx = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	370 -- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	371 -- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) \| tri< a ¬b ¬c = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	372 -- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) \| tri≈ ¬a b ¬c = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	373 -- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) \| tri> ¬a ¬b c₁ = rtreeNodeStop? key {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	374
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	375
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	376 ltreeStoplem key lt key1 rt p<q cg = cg key (nodeEx lt key1 rt)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	377
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	378
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	379
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	380
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	381 -- with (max {n} {m} {a} {t} (suc hi) tree₁ cg) \| (max {n} {m} {a} {t} (suc hi) tree₂ cg)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	382 -- ... \| lh \| rh = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	383
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	384 -- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg \| lh \| rh \| tri< a₁ ¬b ¬c = cg rh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	385 -- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg \| lh \| rh \| tri≈ ¬a b ¬c = cg lh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	386 -- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg \| lh \| rh \| tri> ¬a ¬b c = cg lh
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	387
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	388
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	389 -- findStop : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	390 -- findStop = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	391
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	392 findTEx : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	393 findTEx leafEx sd st next = next leafEx st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	394 findTEx (nodeEx ltree datum rtree) sd st next with <-cmp sd datum
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	395 findTEx tree@(nodeEx ltree datum rtree) sd st next \| tri≈ ¬a b ¬c = next tree st
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	396 findTEx tree@(nodeEx ltree datum rtree) sd st next \| tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findTEx ltree sd st2 next)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	397 findTEx tree@(nodeEx ltree datum rtree) sd st next \| tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findTEx rtree sd st2 next)
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	398
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	399 findL : {n m : Level } {a : Set n} {t : Set m} → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	400 findL leafEx key stack cg = cg leafEx stack
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	401 findL (nodeEx tree₁ key1 tree₂) key stack cg with (key1 ≤? key)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	402 findL (nodeEx tree₁ key1 tree₂) key stack cg \| yes p with key1 ≟ key
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	403 findL tree@(nodeEx tree₁ key1 tree₂) key stack cg \| yes p \| yes p₁ = cg tree stack
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	404 findL tree@(nodeEx ltree key1 tree₂) key stack cg \| yes p \| no ¬p = pushSingleLinkedStack stack tree (λ stack1 → findL ltree key stack1 cg)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	405 findL (nodeEx tree₁ key1 tree₂) key stack cg \| no ¬p = cg leafEx stack
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	406
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	407
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	408
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	409 allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	410 allnodes leafEx p = true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	411 allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	412
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	413 find-leaf : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → Bool
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	414 find-leaf tree = allnodes tree (λ l k r → allnodes l (λ _ j _ → j <B? k) /\ allnodes r (λ _ n _ → k <B? n))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	415
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	416 testTree : {n : Level} {a : Set n} → BTreeEx {n} {a}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	417 testTree {n} {a} = (nodeEx (nodeEx leafEx 1 leafEx) 2 (nodeEx leafEx 3 (nodeEx (nodeEx leafEx 4 leafEx) 5 (nodeEx leafEx 6 leafEx))))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	418
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	419 badTree : {n : Level} {a : Set n} → BTreeEx {n} {a}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	420 badTree {n} {a} = (nodeEx (nodeEx leafEx 3 leafEx) 2 leafEx)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	421
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	422
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	423
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	424 lemm : {n : Level} {a : Set n} → find-leaf {n} {a} testTree ≡ true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	425 lemm = refl
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	426
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	427
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	428 bool-⊥ : true ≡ false → ⊥
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	429 bool-⊥ ()
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	430
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	431 {-- badTree --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	432 -- lemm1 : {n : level} {a : set n} → find-leaf {n} {a} badtree ≡ true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	433 -- lemm1 {n} {a} with badtree
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	434 -- lemm1 {n} {a} \| leafex = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	435 -- lemm1 {n} {a} \| nodeex gda key₁ gda₁ = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	436
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	437 -- lemm-all : {n : Level} {a : Set n} (any-tree : BTreeEx {n} {a}) → find-leaf {n} {a} any-tree ≡ true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	438 -- lemm-all leafEx = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	439 -- lemm-all t@(nodeEx ltree k rtree) with (find-leaf t) ≟B true
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	440 -- lemm-all (nodeEx ltree k rtree) \| yes p = p
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	441 -- lemm-all (nodeEx ltree k rtree) \| no ¬p = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	442
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	443 -- 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	444 -- findT = ?
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	445
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	446 -- {--
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	447 -- 一旦の方針は hight を使って書く, 大小関係 (片方だけ) を持って証明しながら降りてく
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	448 -- --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	449
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	450
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	451 -- hoge = findTEx testTree 44 [] (λ t s → s)
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	452
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	453 -- {--
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	454 -- Tree に対して l < x < r の条件を足すときに気になるのは l or r が leaf の場合
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	455 -- leaf のときだけ例外的な証明を書く必要ありそう
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	456 -- --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	457
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	458
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	459 -- {-- AVL Tree メモ
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	460 -- - $AGDA-HOME/Data/AVL.agda 関連を眺めた Tips
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	461 -- AVL は特徴としてすべての枝の長さの差が1以内に収まっている木。バランスもできる。
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	462
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	463 -- AVL Tree には key , value , left right の他にkeyの上限、下限、高さを持ってるらしい
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	464 -- (後ろに付いてるのは高さ+- 1 の関係をもってる)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	465
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	466 -- cast operation は木のサイズの log になる
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	467 -- (cast operation は… わすれた)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	468
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	469 -- insert では同じ key の値があったら Node を置き換え
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	470
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	471
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	472 -- --}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	473
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	474 -- -- findT testTreeType 44 [] (λ t st → t)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	475 -- -- leaf
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	476
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	477 -- -- findT testTree 44 [] (λ t st → st)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	478 -- -- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	479
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	480
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	481 -- -- findT testTreeType 3 [] (λ t st → t)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	482 -- -- node leaf 3 leaf
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	483
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	484 -- -- findT testTreeType 3 [] (λ t st → st)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	485 -- -- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	486
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	487
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	488 -- replaceT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	489 -- replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	490 -- replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	491
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	492 -- replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	493
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	494
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	495 -- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	496 -- replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next \| tri≈ ¬a b ¬c = replaceT tree n0 rstack next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	497 -- 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	498 -- 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
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	499
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	500
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	501
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	502 -- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	503
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	504 -- -- bad some code
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	505 -- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	506 -- replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	507 -- \| tri≈ ¬a b ¬c = replaceT tree n0 rstack next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	508 -- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	509 -- \| tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	510 -- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	511 -- \| tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	512
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	513 -- insertT : {n m : Level } {a : Set n} {t : Set m} → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	514 -- insertT tree n0 st next = findT tree n0 st ( λ new st2 → replaceT new n0 st2 next )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	515
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	516
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	517 -- c1 : {n : Level} {a : Set n} → BTree {n} a
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	518 -- c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t))))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	519
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	520 -- c2 : {n : Level} {a : Set n} → BTree {n} a
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	521 -- c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t))))
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	522
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	523 -- -- -- 末
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	524 -- -- findDownEnd : {n m : Level} {a : Set n} {t : Set m} → (find : ℕ) → (any : BTree a) → findT any find [] (λ tt stack → {!!})
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	525 -- -- findDownEnd d tree = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	526
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	527 -- 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 ≡ {!!})))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	528 -- find-insert leaf key with <-cmp key key
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	529 -- find-insert leaf key \| tri< a ¬b ¬c = ⊥-elim (¬c a )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	530 -- find-insert leaf key \| tri≈ ¬a b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	531 -- find-insert leaf key \| tri> ¬a ¬b c = ⊥-elim (¬a c )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	532 -- find-insert tr@(node any₁ datum any₂) key with <-cmp key datum
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	533 -- find-insert (node any₁ datum any₂) key \| tri< a ¬b ¬c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	534 -- find-insert (node any₁ datum any₂) key \| tri> ¬a ¬b c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	535 -- find-insert (node any₁ datum any₂) key \| tri≈ ¬a b ¬c with <-cmp key datum
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	536 -- find-insert (node any₁ datum any₂) key \| tri≈ ¬a b ¬c \| tri< a ¬b ¬c₁ = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	537 -- find-insert (node any₁ datum any₂) key \| tri≈ ¬a b ¬c \| tri> ¬a₁ ¬b c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	538 -- find-insert (node any₁ datum any₂) key \| tri≈ ¬a b ¬c \| tri≈ ¬a₁ b₁ ¬c₁ = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	539
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	540 -- -- where
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	541 -- find-lemma : {n m : Level} {a : Set n} {t : Set m} → BTree a → ℕ → SingleLinkedStack (BTree a) → (BTree a → SingleLinkedStack (BTree a) → t) → t
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	542 -- find-lemma leaf ke st nt = nt leaf st
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	543 -- find-lemma (node tr datum tr₁) ke st nt with <-cmp ke datum
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	544 -- find-lemma tt@(node tr datum tr₁) ke st nt \| tri< a ¬b ¬c = find-lemma tr ke (tt ∷ st) nt
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	545 -- find-lemma tt@(node tr datum tr₁) ke st nt \| tri≈ ¬a b ¬c = nt tt st
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	546 -- find-lemma tt@(node tr datum tr₁) ke st nt \| tri> ¬a ¬b c = find-lemma tr₁ ke (tt ∷ st) nt
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	547
40d01b368e34 Temporary Push ryokka parents: diff changeset	548 ----
40d01b368e34 Temporary Push ryokka parents: diff changeset	549 -- find node potition to insert or to delete, the path will be in the stack
40d01b368e34 Temporary Push ryokka parents: diff changeset	550 --
40d01b368e34 Temporary Push ryokka parents: diff changeset	551
40d01b368e34 Temporary Push ryokka parents: diff changeset	552 {-# TERMINATING #-}
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	553 findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	554 findNode {n} {m} {a} {t} tree n0 next with root tree
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	555 findNode {n} {m} {a} {t} tree n0 next \| nothing = next tree
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	556 findNode {n} {m} {a} {t} tree n0 next \| just x with <-cmp (key x) (key n0)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	557 findNode {n} {m} {a} {t} tree n0 next \| just x \| tri≈ ¬a b ¬c = next tree
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	558 findNode {n} {m} {a} {t} tree n0 next \| just x \| tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	559 findNode {n} {m} {a} {t} tree n0 next \| just x \| tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	560
40d01b368e34 Temporary Push ryokka parents: diff changeset	561
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	562
580 99429fdb3b8b ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 579 diff changeset	563 findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	564 findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
577 ac2293378d7a modify findNode1 ryokka parents: 576 diff changeset	565 module FindNode where
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	566 findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	567 findNode2 nothing st = next record { root = nothing ; nodeStack = st }
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	568 findNode2 (just x) st with <-cmp (key n0) (key x)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	569 ... \| tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st })
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	570 ... \| tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	571 ... \| tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	572
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	573 node001 : Node ℕ
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	574 node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	575 node002 : Node ℕ
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	576 node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	577 node003 : Node ℕ
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	578 node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	579
586 0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda. ryokka parents: 585 diff changeset	580 tes0t01 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	581 node001 ( λ tree → tree )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	582 test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	583 node001 ( λ tree → tree )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	584 test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	585 node001 ( λ tree → tree )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	586 test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	587 node001 ( λ tree → tree )
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	588
583 d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	589 replaceNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	590 replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	591 module FindNodeR where
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	592 replaceNode1 : (Maybe (Node a )) → Node a
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	593 replaceNode1 nothing = record n0 { left = nothing ; right = nothing }
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	594 replaceNode1 (just x) = record n0 { left = left x ; right = right x }
583 d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	595 replaceNode2 : SingleLinkedStack (Node a ) → (Node a → t) → t
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	596 replaceNode2 [] next = next ( replaceNode1 (root tree) )
583 d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	597 replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	598 replaceNode2 (x ∷ st) next \| tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	599 replaceNode2 (x ∷ st) next \| tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	600 replaceNode2 (x ∷ st) next \| tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	601
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	602 insertNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	603 insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )
d18df2e6135d add replaceNode Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 582 diff changeset	604
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	605 createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ)
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	606 → RedBlackTree {n} a
576 40d01b368e34 Temporary Push ryokka parents: diff changeset	607 createEmptyRedBlackTreeℕ a b = record {
40d01b368e34 Temporary Push ryokka parents: diff changeset	608 root = nothing
40d01b368e34 Temporary Push ryokka parents: diff changeset	609 ; nodeStack = emptySingleLinkedStack
40d01b368e34 Temporary Push ryokka parents: diff changeset	610 }
40d01b368e34 Temporary Push ryokka parents: diff changeset	611
581 09e9e8fd7568 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 580 diff changeset	612 findNodeLeft : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n
09e9e8fd7568 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 580 diff changeset	613 findNodeLeft x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing )
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	614 findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h)) -- stack の top と比較するのはたぶん replace ...?
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	615
581 09e9e8fd7568 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 580 diff changeset	616 findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n
09e9e8fd7568 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 580 diff changeset	617 findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing )
09e9e8fd7568 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 580 diff changeset	618 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	619
589 37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	620 data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (node : Maybe (Node a) ) → Set n where
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	621 fni-stackEmpty : (now : Maybe (Node a) ) → FindNodeInvariant [] now
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	622 fni-treeEmpty : (st : SingleLinkedStack (Node a)) → FindNodeInvariant st nothing
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	623 fni-Left : (x : Node a) (st : SingleLinkedStack (Node a)) (node : Maybe (Node a ))
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	624 → FindNodeInvariant ( x ∷ st ) node → findNodeLeft x st → FindNodeInvariant st node
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	625 fni-Right : (x : Node a) (st : SingleLinkedStack (Node a)) (node : Maybe (Node a ))
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	626 → FindNodeInvariant ( x ∷ st ) node → findNodeRight x st → FindNodeInvariant st node
585 42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	627 findNodeLoop : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	628 findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st))
42e8cf963c5c Add 'non inductiove record' tree, findT, replaceT, and insertT ryokka parents: 584 diff changeset	629
589 37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	630 findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a )
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	631 → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) (root new ) → t )
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	632 → ( FindNodeInvariant (nodeStack tree) (root tree) ) → t
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	633 findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	634 module FindNodeH where
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	635 findNode2h : (new : Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s new → t
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	636 findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } prev
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	637 findNode2h (just x) st prev with <-cmp (key n0) (key x)
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	638 ... \| tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) prev
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	639 ... \| tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 {!!} {!!} {!!}) )
37f5826ca7d2 minor fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 588 diff changeset	640 ... \| tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 {!!} {!!} {!!}) )
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	641
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 577 diff changeset	642
584 7e551cef35d7 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 583 diff changeset	643 -- replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t
7e551cef35d7 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 583 diff changeset	644 -- replaceNodeH = {!!}

Mercurial > hg > Gears > GearsAgda

annotate hoareRedBlackTree.agda @ 589:37f5826ca7d2