Mercurial > hg > Members > ryokka > HoareLogic
changeset 36:320b765a6424
fix loopProof
| author | ryokka |
|---|---|
| date | Fri, 13 Dec 2019 19:45:34 +0900 |
| parents | 7c739972cd26 |
| children | 2db6120a02e6 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 11 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Fri Dec 13 19:23:15 2019 +0900 +++ b/whileTestGears.agda Fri Dec 13 19:45:34 2019 +0900 @@ -176,13 +176,17 @@ loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit - -loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (d : Dec (P c)) - → Pre c → (Context → (continue : (c1 : Context) → ¬ (P c1) → Inv c1 → t) - → (exit : (c2 : Context) → (P c2) → Post c2 → t) → t) → t -loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (false because proof₁) f = - loopProof {!!} {!!} {!!} -loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (true because proof₁) f = {!!} +{-# TERMINATING #-} +loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c)) + → Pre c → (exit : (c2 : Context) → (P c2) → Post c2 → t) + (f : Context → (exit : (c2 : Context) → (P c2) → Post c2 → t) → t) → t +loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt if pre exit f = lem cxt + where + lem : (c : Context) → t + lem c with if c + lem c | no ¬p = f c exit + lem c | yes p = exit c p {!!} + proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })