Mercurial > hg > Members > ryokka > HoareLogic
changeset 9:46b301ad4478
add some proof
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Dec 2018 11:57:18 +0900 |
| parents | e4f087b823d4 |
| children | bc819bdda374 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 10 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Sat Dec 15 11:38:55 2018 +0900 +++ b/whileTestGears.agda Sat Dec 15 11:57:18 2018 +0900 @@ -90,11 +90,6 @@ proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) proof1 = refl - - --- stmt2Cond : {l : Level} → EnvWithCond {l} → --- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0) - whileTest' : {l : Level} {t : Set l} -> (Code : (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t whileTest' next = next env proof2 where @@ -105,13 +100,15 @@ {-# TERMINATING #-} whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> ((varn env) + (vari env) ≡ 10) -> (Code : Env -> t) -> t -whileLoop' env proof next with lt 0 (varn env) -whileLoop' env proof next | false = next env -whileLoop' env proof next | true = whileLoop' env1 proof3 next +whileLoop' env proof next with ( suc zero ≤? (varn env) ) +whileLoop' env proof next | no p = next env +whileLoop' env proof next | yes p = whileLoop' env1 (proof3 p ) next where env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} - proof3 : varn env1 + vari env1 ≡ 10 - proof3 = {!!} + proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ 10 + proof3 (s≤s lt) with varn env + proof3 (s≤s z≤n) | zero = {!!} + proof3 (s≤s lt) | suc n = {!!} conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) @@ -133,3 +130,6 @@ proofGears : Set proofGears = whileTest' (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ 10 )))) + +proofGearsMeta : whileTest' (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ 10 )))) +proofGearsMeta = refl