Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 70:fdd31b6808db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Dec 2019 18:20:42 +0900
parents 5b17a3601037
children 57d5a3884898
comparison
equal deleted inserted replaced
69:5b17a3601037 70:fdd31b6808db
201 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t 201 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t
202 whileLoopPSem env s next exit with <-cmp 0 (varn env) 202 whileLoopPSem env s next exit with <-cmp 0 (varn env)
203 whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!} 203 whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!}
204 whileLoopPSem env s next exit | tri< a ¬b ¬c = {!!} 204 whileLoopPSem env s next exit | tri< a ¬b ¬c = {!!}
205 205
206 loopPP : (input : Envc ) → Envc
207 loopPP input with <-cmp 0 (varn input )
208 loopPP input | tri≈ ¬a b ¬c = input
209 loopPP input | tri< a ¬b ¬c = {!!} -- loopPP (whileLoopP ?
210 -- = whileLoopP input (λ next → loopPP next ) (λ output → output )
211
206 whileLoopPSemSound : (input output : Envc ) 212 whileLoopPSemSound : (input output : Envc )
207 → whileTestStateP s2 input 213 → whileTestStateP s2 input
208 → output ≡ whileLoopP input (λ e → whileLoopP e ? (λ e → e ) ) (λ e → e) 214 → output ≡ loopPP input
209 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) 215 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
210 whileLoopPSemSound = {!!} 216 whileLoopPSemSound input output pre refl with <-cmp 0 (varn input )
211 217 ... | ttt = {!!}
212
213 218
214 -- induction にする 219 -- induction にする
215 {-# TERMINATING #-} 220 {-# TERMINATING #-}
216 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t 221 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
217 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit 222 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
218 223
219 -- wP を Env のRel にする Env → Env → Set にしちゃう 224 -- wP を Env のRel にする Env → Env → Set にしちゃう
220 whileTestPCallwP : (c : ℕ ) → Set 225 whileTestPCallwP : (c : ℕ ) → Set
221 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where 226 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where
222 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env 227 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
223 conv e record { pi1 = refl ; pi2 = refl } = +zero 228 conv e record { pi1 = refl ; pi2 = refl } = +zero
224 229
225 230
226 conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env 231 conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
227 conv1 e record { pi1 = refl ; pi2 = refl } = +zero 232 conv1 e record { pi1 = refl ; pi2 = refl } = +zero
228 233