Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 36:320b765a6424

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix loopProof
author ryokka
date Fri, 13 Dec 2019 19:45:34 +0900
parents 7c739972cd26
children 2db6120a02e6
comparison
equal deleted inserted replaced
35:7c739972cd26 36:320b765a6424
174 {-# TERMINATING #-} 174 {-# TERMINATING #-}
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 179 {-# TERMINATING #-}
180 loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (d : Dec (P c)) 180 loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
181 → Pre c → (Context → (continue : (c1 : Context) → ¬ (P c1) → Inv c1 → t) 181 → Pre c → (exit : (c2 : Context) → (P c2) → Post c2 → t)
182 → (exit : (c2 : Context) → (P c2) → Post c2 → t) → t) → t 182 (f : Context → (exit : (c2 : Context) → (P c2) → Post c2 → t) → t) → t
183 loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (false because proof₁) f = 183 loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt if pre exit f = lem cxt
184 loopProof {!!} {!!} {!!} 184 where
185 loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (true because proof₁) f = {!!} 185 lem : (c : Context) → t
186 lem c with if c
187 lem c | no ¬p = f c exit
188 lem c | yes p = exit c p {!!}
189
186 190
187 191
188 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 192 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
189 $ λ cxt → whileConvProof cxt 193 $ λ cxt → whileConvProof cxt
190 $ λ cxt → loop cxt 194 $ λ cxt → loop cxt