Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 37:2db6120a02e6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Fri, 13 Dec 2019 19:54:28 +0900
parents 320b765a6424
children 7049fbaf5e18
comparison
equal deleted inserted replaced
36:320b765a6424 37:2db6120a02e6
175 loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t 175 loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t
176 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit 176 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
177 177
178 178
179 {-# TERMINATING #-} 179 {-# TERMINATING #-}
180 loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c)) 180 loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
181 → Pre c → (exit : (c2 : Context) → (P c2) → Post c2 → t) 181 → Inv c → (exit : (c2 : Context) → (P c2) → Inv c2 → t)
182 (f : Context → (exit : (c2 : Context) → (P c2) → Post c2 → t) → t) → t 182 (f : Context → (exit : (c2 : Context) → (P c2) → Inv c2 → t) → t) → t
183 loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt if pre exit f = lem cxt 183 loopProof {l} {t} {P} {Inv} cxt if inv exit f = lem cxt inv
184 where 184 where
185 lem : (c : Context) → t 185 lem : (c : Context) → Inv c → t
186 lem c with if c 186 lem c inv with if c
187 lem c | no ¬p = f c exit 187 lem c inv | no ¬p = f c (λ c1 inv1 inv2 → lem c1 {!!} )
188 lem c | yes p = exit c p {!!} 188 lem c inv | yes p = exit {!!} {!!} {!!}
189 189
190 190
191 191
192 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 192 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
193 $ λ cxt → whileConvProof cxt 193 $ λ cxt → whileConvProof cxt