Mercurial > hg > Members > ryokka > HoareLogic
changeset 50:2edb44c5bf52
add s1~3, proofs
| author | ryokka |
|---|---|
| date | Wed, 18 Dec 2019 20:08:58 +0900 |
| parents | 91d6d8097a39 |
| children | 3f4f93ac841d |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 15 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Wed Dec 18 19:26:24 2019 +0900 +++ b/whileTestGears.agda Wed Dec 18 20:08:58 2019 +0900 @@ -133,6 +133,21 @@ open EnvP +s1 : (c10 : ℕ) → EnvP +s1 c10 = record {env = record {vari = 0 ; varn = c10} ; c10 = c10 ; cx = pstate1 (record {pi1 = refl ; pi2 = refl})} + +s2 : (e : EnvP) → varn (env e) > 0 → varn (env e) < c10 e → EnvP +s2 e n>0 n<c10 with <-cmp 0 (varn (env e)) +s2 e n>0 n<c10 | tri< a ¬b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pstate2 {!!} {!!} {!!} } +s2 e n>0 n<c10 | tri≈ ¬a b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pfinstate {!!} {!!} } + +s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e +s3 record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl = {!!} + +proofs : (c : ℕ) (e : EnvP) → vari (env e) ≡ c10 e +proofs c e = s3 (s2 (s1 {!!}) {!!} {!!}) {!!} + + whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where env1 : Env