Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 657:f7090788789b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
s-left0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Nov 2021 14:40:55 +0900
parents 30690aed1819
children be2fd2884eef
comparison
equal deleted inserted replaced
656:30690aed1819 657:f7090788789b
103 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 103 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
104 104
105 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where 105 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where
106 s-nil : {tree : bt A} → stackInvariant key tree tree [] 106 s-nil : {tree : bt A} → stackInvariant key tree tree []
107 s-right0 : {tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } 107 s-right0 : {tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A }
108 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree (node key₁ v1 tree₁ tree) (tree ∷ (node key₁ v1 tree₁ tree) ∷ []) 108 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree tree (tree ∷ [])
109 s-left0 : {tree₁ tree : bt A} → {key₁ : ℕ } → {v1 : A } 109 s-left0 : {tree₁ tree : bt A} → {key₁ : ℕ } → {v1 : A }
110 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree₁ (node key₁ v1 tree₁ tree) (tree₁ ∷ (node key₁ v1 tree₁ tree) ∷ []) 110 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree₁ tree₁ (tree₁ ∷ [])
111 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 111 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
112 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree tree0 (tree ∷ st) 112 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree tree0 (tree ∷ st)
113 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 113 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
114 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree₁ tree0 (tree₁ ∷ st) 114 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
115 115
149 stack-last [] = nothing 149 stack-last [] = nothing
150 stack-last (x ∷ []) = just x 150 stack-last (x ∷ []) = just x
151 stack-last (x ∷ s) = stack-last s 151 stack-last (x ∷ s) = stack-last s
152 152
153 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) 153 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
154 stackInvariantTest1 = s-right0 (add< 2) s-nil 154 stackInvariantTest1 = s-right (add< 2) (s-right0 (add< 2) s-nil) (λ ())
155 155
156 si-nil : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → (si : stackInvariant key tree tree0 []) → tree ≡ tree0 156 si-nil : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → (si : stackInvariant key tree tree0 []) → tree ≡ tree0
157 si-nil s-nil = refl 157 si-nil s-nil = refl
158 158
159 si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → stackInvariant key tree tree0 stack 159 si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → stackInvariant key tree tree0 stack
160 → stack-top stack ≡ just tree 160 → stack-top stack ≡ just tree
161 si-property1 key t t0 [] ne (s-nil ) = ⊥-elim ( ne refl ) 161 si-property1 key t t0 [] ne (s-nil ) = ⊥-elim ( ne refl )
162 si-property1 key t t0 (t ∷ _ ∷ []) ne (s-right0 _ _) = refl 162 si-property1 key t t0 (t ∷ []) ne (s-right0 _ _) = refl
163 si-property1 key t t0 (t ∷ _ ∷ []) ne (s-left0 _ _) = refl 163 si-property1 key t t0 (t ∷ []) ne (s-left0 _ _) = refl
164 si-property1 key t t0 (t ∷ st) _ (s-right _ _ si) = refl 164 si-property1 key t t0 (t ∷ st) _ (s-right _ _ si) = refl
165 si-property1 key t t0 (t ∷ st) _ (s-left _ _ si) = refl 165 si-property1 key t t0 (t ∷ st) _ (s-left _ _ si) = refl
166 166
167 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → stackInvariant key tree tree0 stack 167 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → stackInvariant key tree tree0 stack
168 → stack-last stack ≡ just tree0 168 → stack-last stack ≡ just tree0
169 si-property-last key t t0 [] ne s-nil = ⊥-elim ( ne refl ) 169 si-property-last key t t0 [] ne s-nil = ⊥-elim ( ne refl )
170 si-property-last key t t0 (t ∷ _ ∷ []) _ (s-left0 _ _) = {!!} 170 si-property-last key t t0 (t ∷ []) _ (s-left0 _ _) = {!!}
171 si-property-last key t t0 (t ∷ _ ∷ []) _ (s-right0 _ _) = {!!} 171 si-property-last key t t0 (t ∷ []) _ (s-right0 _ _) = {!!}
172 si-property-last key t t0 (t ∷ []) _ (s-right _ _ ne) = ⊥-elim ( ne refl ) 172 si-property-last key t t0 (t ∷ []) _ (s-right _ _ ne) = ⊥-elim ( ne refl )
173 si-property-last key t t0 (t ∷ []) _ (s-left _ _ ne) = ⊥-elim ( ne refl ) 173 si-property-last key t t0 (t ∷ []) _ (s-left _ _ ne) = ⊥-elim ( ne refl )
174 si-property-last key t t0 (.t ∷ x ∷ st) ne (s-right _ si _) with si-property1 key _ _ (x ∷ st) (λ ()) si 174 si-property-last key t t0 (.t ∷ x ∷ st) ne (s-right _ si _) with si-property1 key _ _ (x ∷ st) (λ ()) si
175 ... | refl = si-property-last key x t0 (x ∷ st) (λ ()) si 175 ... | refl = si-property-last key x t0 (x ∷ st) (λ ()) si
176 si-property-last key t t0 (.t ∷ x ∷ st) ne (s-left _ si _) with si-property1 key _ _ (x ∷ st) (λ ()) si 176 si-property-last key t t0 (.t ∷ x ∷ st) ne (s-left _ si _) with si-property1 key _ _ (x ∷ st) (λ ()) si
189 ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti 189 ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti
190 190
191 stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A)) 191 stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A))
192 → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub 192 → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub
193 stackTreeInvariant {_} {A} key sub tree [] ti s-nil = ti 193 stackTreeInvariant {_} {A} key sub tree [] ti s-nil = ti
194 stackTreeInvariant {_} {A} key sub tree (sub ∷ _ ∷ []) ti (s-left0 _ _) = {!!} 194 stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-left0 _ _) = {!!}
195 stackTreeInvariant {_} {A} key sub tree (sub ∷ _ ∷ []) ti (s-right0 _ _) = {!!} 195 stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-right0 _ _) = {!!}
196 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si _) = ti-right (si1 si) where 196 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si _) = ti-right (si1 si) where
197 si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant (node key₁ v1 tree₁ sub ) 197 si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant (node key₁ v1 tree₁ sub )
198 si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si 198 si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si
199 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si _) = ti-left ( si2 si) where 199 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si _) = ti-left ( si2 si) where
200 si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 sub tree₁ ) tree st → treeInvariant (node key₁ v1 sub tree₁ ) 200 si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 sub tree₁ ) tree st → treeInvariant (node key₁ v1 sub tree₁ )
246 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl) 246 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
247 findP {_} {_} {A} key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) 247 findP {_} {_} {A} key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st)
248 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where 248 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where
249 findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st) 249 findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
250 findP1 a (x ∷ st) si = s-left a si (λ ()) 250 findP1 a (x ∷ st) si = s-left a si (λ ())
251 findP1 a [] s-nil = {!!} 251 findP1 a [] s-nil = ? -- s-left0 a s-nil
252 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) {!!} ⟫ depth-2< 252 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) {!!} ⟫ depth-2<
253 253
254 replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁) 254 replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
255 replaceTree1 k v1 value (t-single .k .v1) = t-single k value 255 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
256 replaceTree1 k v1 value (t-right x t) = t-right x t 256 replaceTree1 k v1 value (t-right x t) = t-right x t