Mercurial > hg > Members > ryokka > HoareLogic
changeset 66:9071e5a77a13
implies
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 Dec 2019 09:48:54 +0900 |
| parents | bef5d4281ac8 |
| children | 946d6b82aad5 |
| files | whileTestGears.agda whileTestPrimProof.agda |
| diffstat | 2 files changed, 20 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Sun Dec 22 15:41:41 2019 +0900 +++ b/whileTestGears.agda Mon Dec 23 09:48:54 2019 +0900 @@ -176,14 +176,26 @@ c10 env ∎ -whileTestPwPSound : (c : ℕ) → whileTestPwP c ( λ env s → whileTestStateP s1 env ) -whileTestPwPSound c = record { pi1 = refl ; pi2 = refl } +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A → B ) → A implies B + +implies2p : {A B : Set } → A implies B → A → B +implies2p (proof x) = x + +whileTestPwPSound : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) +whileTestPwPSound c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) -GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t ) → post (f env ( λ env s → env )) -GearsIdSound env {post} f = ? +GearsIdSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} + (f : {l : Level } {t : Set l } → (e0 : Envc ) → pre e0 → ((e : Envc) → post e → t) → t ) + → (p : pre e0) + → e1 ≡ ( f e0 p ( λ e1 s → e1 )) + → (pre e0) implies (post e1) +GearsIdSound e0 _ {pre} {post} f p refl = proof (λ p → (f e0 p (λ e1 s → {!!} ))) where + lemma : post (f e0 p (λ e1 s → e1)) + lemma = subst (λ k → post k ) {!!} {!!} --- hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → (vari e ≡ 0) /\ (varn e ≡ c)) --- hoge c env = GearsIdSound env (λ e → whileTestPwP c ) +hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → ⊤ implies ((vari e ≡ 0) /\ (varn e ≡ c))) +hoge c env = {!!} -- GearsIdSound env (λ e → whileTestPwP c ) -- induction にする {-# TERMINATING #-}
--- a/whileTestPrimProof.agda Sun Dec 22 15:41:41 2019 +0900 +++ b/whileTestPrimProof.agda Mon Dec 23 09:48:54 2019 +0900 @@ -250,6 +250,8 @@ PrimSemComm : ∀ {l} -> PrimComm -> Rel State l PrimSemComm prim s1 s2 = Id State (prim s1) s2 + + axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2