Mercurial > hg > Members > ryokka > HoareLogic
changeset 68:def072b6c016
GearsUnitSound
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 Dec 2019 15:57:23 +0900 |
| parents | 946d6b82aad5 |
| children | 5b17a3601037 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 11 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Mon Dec 23 12:54:36 2019 +0900 +++ b/whileTestGears.agda Mon Dec 23 15:57:23 2019 +0900 @@ -181,19 +181,22 @@ 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 } ) +whileTestPSem : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) +whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t) → t ) → Set (succ Zero) SemGears f = Envc → Envc → Set -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 ) - → pre e0 → post e1 -GearsIdSound e0 e1 f p0 = {!!} +GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} + → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t) → t ) + → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1))) + → e1 ≡ f e0 (λ e → e ) + → f e0 (λ e1 → pre e0 implies post e1) +GearsUnitSound e0 e1 f fsem refl = fsem e0 -hoge : (c : ℕ ) (input output : Envc ) → ? → (vari output ≡ 0) /\ (varn output ≡ c) -hoge c input output sem = GearsIdSound input output {λ e → ⊤} ? tt +whileTestPSemSound : (c : ℕ ) (input output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) +whileTestPSemSound c input output refl = whileTestPSem c + -- induction にする {-# TERMINATING #-}