Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 81:0122f980427c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Jan 2020 15:33:49 +0900
parents 148feaa1e346
children 33a6fd61c3e6
comparison
equal deleted inserted replaced
80:148feaa1e346 81:0122f980427c
10 open import Agda.Builtin.Unit 10 open import Agda.Builtin.Unit
11 11
12 open import utilities 12 open import utilities
13 open _/\_ 13 open _/\_
14 14
15 -- original codeGear (with non terminatinng )
16
15 record Env : Set (succ Zero) where 17 record Env : Set (succ Zero) where
16 field 18 field
17 varn : ℕ 19 varn : ℕ
18 vari : ℕ 20 vari : ℕ
19 open Env 21 open Env
29 whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next 31 whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
30 32
31 test1 : Env 33 test1 : Env
32 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) 34 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
33 35
34
35 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) 36 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
36 proof1 = refl 37 proof1 = refl
37 38
39 -- codeGear with pre-condtion and post-condition
40 --
38 -- ↓PostCondition 41 -- ↓PostCondition
39 whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env ) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t 42 whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env ) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
40 whileTest' {_} {_} {c10} next = next env proof2 43 whileTest' {_} {_} {c10} next = next env proof2
41 where 44 where
42 env : Env 45 env : Env
90 c10 + 0 93 c10 + 0
91 ≡⟨ +-sym {c10} {0} ⟩ 94 ≡⟨ +-sym {c10} {0} ⟩
92 c10 95 c10
93 ∎ 96 ∎
94 97
95 98 -- all proofs are connected
96 proofGears : {c10 : ℕ } → Set 99 proofGears : {c10 : ℕ } → Set
97 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) 100 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))
98 101
102 -- but we cannot prove the soundness of the last condition
103 --
99 -- proofGearsMeta : {c10 : ℕ } → proofGears {c10} 104 -- proofGearsMeta : {c10 : ℕ } → proofGears {c10}
100 -- proofGearsMeta {c10} = {!!} -- net yet done 105 -- proofGearsMeta {c10} = {!!} -- net yet done
101 106
102 -- 107 --
103 -- openended Env c <=> Context 108 -- codeGear with loop step and closed environment
104 -- 109 --
105 110
106 open import Relation.Nullary hiding (proof)
107 open import Relation.Binary 111 open import Relation.Binary
108 112
109 record Envc : Set (succ Zero) where 113 record Envc : Set (succ Zero) where
110 field 114 field
111 c10 : ℕ 115 c10 : ℕ
120 whileLoopP env next exit with <-cmp 0 (varn env) 124 whileLoopP env next exit with <-cmp 0 (varn env)
121 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env 125 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
122 whileLoopP env next exit | tri< a ¬b ¬c = 126 whileLoopP env next exit | tri< a ¬b ¬c =
123 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) 127 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
124 128
129 -- equivalent of whileLoopP but it looks like an induction on varn
125 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t 130 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
126 whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env 131 whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env
127 whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari }) 132 whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari })
128 133
129 134 -- normal loop without termination
130 {-# TERMINATING #-} 135 {-# TERMINATING #-}
131 loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t 136 loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
132 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit 137 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
133 138
134 whileTestPCall : (c10 : ℕ ) → Envc 139 whileTestPCall : (c10 : ℕ ) → Envc
135 whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env → env)) 140 whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env → env))
136 141
142 --
143 -- codeGears with states of condition
144 --
137 data whileTestState : Set where 145 data whileTestState : Set where
138 s1 : whileTestState 146 s1 : whileTestState
139 s2 : whileTestState 147 s2 : whileTestState
140 sf : whileTestState 148 sf : whileTestState
141 149
155 whileLoopPwP env s next exit with <-cmp 0 (varn env) 163 whileLoopPwP env s next exit with <-cmp 0 (varn env)
156 whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s) 164 whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
157 where 165 where
158 lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env 166 lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
159 lem p1 p2 rewrite p1 = p2 167 lem p1 p2 rewrite p1 = p2
160
161 whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a) 168 whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
162 where 169 where
163 1<0 : 1 ≤ zero → ⊥ 170 1<0 : 1 ≤ zero → ⊥
164 1<0 () 171 1<0 ()
165 proof5 : (suc zero ≤ (varn env)) → (varn env - 1) + (vari env + 1) ≡ c10 env 172 proof5 : (suc zero ≤ (varn env)) → (varn env - 1) + (vari env + 1) ≡ c10 env
178 varn env + vari env 185 varn env + vari env
179 ≡⟨ s ⟩ 186 ≡⟨ s ⟩
180 c10 env 187 c10 env
181 ∎ 188 ∎
182 189
190 {-# TERMINATING #-}
191 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
192 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
193
194 -- all codtions are correctly connected and required condtion is proved in the continuation
195 -- use required condition as t in (env → t) → t
196 whileTestPCallwP : (c : ℕ ) → Set
197 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where
198 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
199 conv e record { pi1 = refl ; pi2 = refl } = +zero
200
201 --
202 -- Using imply relation to make soundness explicit
203 -- termination is shown by induction on varn
204 --
205
183 data _implies_ (A B : Set ) : Set (succ Zero) where 206 data _implies_ (A B : Set ) : Set (succ Zero) where
184 proof : ( A → B ) → A implies B 207 proof : ( A → B ) → A implies B
185 208
186 implies2p : {A B : Set } → A implies B → A → B 209 implies2p : {A B : Set } → A implies B → A → B
187 implies2p (proof x) = x 210 implies2p (proof x) = x
199 GearsUnitSound e0 e1 f fsem = fsem e0 222 GearsUnitSound e0 e1 f fsem = fsem e0
200 223
201 whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) 224 whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
202 whileTestPSemSound c output refl = whileTestPSem c 225 whileTestPSemSound c output refl = whileTestPSem c
203 226
227 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
228 loopPP zero input refl = input
229 loopPP (suc n) input refl =
230 loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl
231
204 whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input 232 whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input
205 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t)
206 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t
207 whileLoopPSem env s next exit with <-cmp 0 (varn env)
208 whileLoopPSem env s next exit | tri≈ ¬a b ¬c rewrite (sym b) = exit env (proof (λ z → z))
209 whileLoopPSem env s next exit | tri< a ¬b ¬c = next env (proof (λ z → z))
210
211
212
213 whileLoopPSem' : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input
214 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) 233 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t)
215 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t 234 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t
216 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z)) 235 whileLoopPSem env s next exit with varn env | s
217 whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next exit = 236 ... | zero | _ = exit env (proof (λ z → z))
218 next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari) 237 ... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) )
219 238
220 239 loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl
221 {--
222 (((⊤ implies varn ≡ 0 ∧ vari ≡ c10 ) implies (varn + vari ≡ c10)) implies vari ≡ c10)
223
224
225 --}
226 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
227 loopPP zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
228 loopPP (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP input (λ x → loopPP n (record x { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl) λ x → x -- ?
229
230 loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
231
232 loopPP' zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
233 loopPP' (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = loopPP' n (record { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl -- ?
234
235 loopPPSem : (input output : Envc ) → output ≡ loopPP' (varn input) input refl
236 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) 240 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
237 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p 241 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p
238 where 242 where
239 -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡ Envc.c10 output
240 -- lem output eq with <-cmp 0 (Envc.varn input)
241 -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!}
242 -- lem output refl | tri≈ ¬a refl ¬c = s2p
243 lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) 243 lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
244 lem n env = +-suc (n) (vari env) 244 lem n env = +-suc (n) (vari env)
245 loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP' n current eq) 245 loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq)
246 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) 246 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
247 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) -- loopeq には output ≡ loopPP zero current (zero = varn current) 247 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
248 248 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
249 -- n を減らして loop を回しつつ証明したい 249 whileLoopPSem current refl
250 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = whileLoopPSem' current refl (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) 250 (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
251 251 (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
252 -- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl)
253
254 252
255 whileLoopPSemSound : {l : Level} → (input output : Envc ) 253 whileLoopPSemSound : {l : Level} → (input output : Envc )
256 → whileTestStateP s2 input 254 → whileTestStateP s2 input
257 → output ≡ loopPP' (varn input) input refl 255 → output ≡ loopPP (varn input) input refl
258 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) 256 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
259 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre 257 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
260 258
261
262 -- induction にする
263 {-# TERMINATING #-}
264 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
265 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
266
267 -- wP を Env のRel にする Env → Env → Set にしちゃう
268 whileTestPCallwP : (c : ℕ ) → Set
269 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where
270 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
271 conv e record { pi1 = refl ; pi2 = refl } = +zero
272
273
274 conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
275 conv1 e record { pi1 = refl ; pi2 = refl } = +zero
276
277 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
278
279
280 -- data GComm : Set (succ Zero) where
281 -- Skip : GComm
282 -- Abort : GComm
283 -- PComm : Set → GComm
284 -- -- Seq : GComm → GComm → GComm
285 -- -- If : whileTestState → GComm → GComm → GComm
286 -- while : whileTestState → GComm → GComm
287
288 -- gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
289 -- gearsSem pre post = {!!}
290
291 -- unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
292 -- unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
293
294 -- comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
295 -- comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
296
297 -- -- repeat : ℕ -> rel set zero -> rel set zero
298 -- -- repeat ℕ.zero r = λ x x₁ → ⊤
299 -- -- repeat (ℕ.suc m) r = comp (repeat m r) r
300
301 -- GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
302 -- GSemComm Skip = λ x x₁ → ⊤
303 -- GSemComm Abort = λ x x₁ → ⊥
304 -- GSemComm (PComm x) = λ x₁ x₂ → x
305 -- -- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
306 -- -- GSemComm (If x con con₁) = {!!}
307 -- GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) → {!!}) {!!} {!!}
308
309 ProofConnect : {l : Level} {t : Set l}
310 → (pr1 : Envc → Set → Set)
311 → (Envc → Set → (Envc → Set → t))
312 → (Envc → Set → Set)
313 ProofConnect prev f env post = {!!} -- with f env ({!!}) {!!}
314
315 Proof2 : (env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env
316 Proof2 _ refl = refl
317
318
319 -- Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → ((env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env) → vari env ≡ c10 env
320 Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → loopPwP env s ( λ env s → vari env ≡ c10 env )
321 Proof1 env s = {!!}
322
323 Proof : (c : ℕ ) → whileTestPCallwP c
324 Proof c = {!!}