Mercurial > hg > Gears > GearsAgda

annotate hoareBinaryTree.agda @ 586:0ddfa505d612

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isolate search function problem, and add hoareBinaryTree.agda.
author ryokka
date Wed, 04 Dec 2019 15:42:47 +0900
parents
children f103f07c0552
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
586
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
1 module hoareBinaryTree where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
2
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
3 open import Level renaming (zero to Z ; suc to succ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
4
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
5 open import Data.Nat hiding (compare)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
6 open import Data.Nat.Properties as NatProp
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
7 open import Data.Maybe
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
8 open import Data.Maybe.Properties
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
9 open import Data.Empty
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
10 open import Data.List
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
11 open import Data.Product
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
12
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
13 open import Function as F hiding (const)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
14
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
15 open import Relation.Binary
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
16 open import Relation.Binary.PropositionalEquality
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
17 open import Relation.Nullary
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
18 open import logic
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
19
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
20
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
21 SingleLinkedStack = List
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
22
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
23 emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
24 emptySingleLinkedStack = []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
25
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
26 clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
27 clearSingleLinkedStack [] cg = cg []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
28 clearSingleLinkedStack (x ∷ as) cg = cg []
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
29
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
30 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
31 pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
32
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
33 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
34 popSingleLinkedStack [] cs = cs [] nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
35 popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
36
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
37
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
38
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
39 data bt {n : Level} {a : Set n} : ℕ → ℕ → Set n where
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
40 bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt l u
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
41 bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
42 bt {n} {a} l' d → bt {n} {a} d u' → l ≤ l' → u' ≤ u → bt l u
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
43
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
44 lleaf : {n : Level} {a : Set n} → bt {n} {a} 0 3
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
45 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
46
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
47 rleaf : {n : Level} {a : Set n} → bt {n} {a} 3 4
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
48 rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
49
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
50 test-node : {n : Level} {a : Set n} → bt {n} {a} 0 4
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
51 test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
52
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
53
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
54
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
55 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
56 d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
57
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
58 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
59 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
60
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
61 -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
62 -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
63 bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} l u → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
64 bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
65 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg with <-cmp key d
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
66 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
67 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
68 bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
69
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
70
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
71 -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
72 bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
73 bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
74
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
75 bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
76 bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
77
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
78
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
79 -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
80 -- up-some (just (fst , snd)) = just fst
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
81 -- up-some nothing = nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
82
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
83 search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} l u) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
84 search-lem {n} {m} {a} {t} key (bt-leaf x) = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
85 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
86 search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
87 search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
88 search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
89
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
90
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
91 -- bt-find
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
92 find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
93
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
94 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
95 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
96 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
97
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
98 find-support {n} {m} {a} {t} key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
99 pushSingleLinkedStack st node
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
100 (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L {!!} {!!})
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
101 -- bt が l u の2つの ℕ を受ける、この値はすべてのnodeによって異なるため stack に積むときに型が合わない
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
102
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
103 -- find-support ⦃ ll' ⦄ ⦃ d ⦄ key L {!!} {!!})
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
104
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
105
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
106 find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = {!!}
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
107
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
108
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
109 bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
110 bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st (λ cst → find-support key tr cst cg)
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
111
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
112
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
113
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
114 -- 証明に insert がはいっててほしい
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
115 -- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → bt-search d tree (λ pt → ) → t
0ddfa505d612 isolate search function problem, and add hoareBinaryTree.agda.
ryokka
parents:
diff changeset
116 -- bt-insert = ?