Mercurial > hg > Members > ryokka > HoareLogic
comparison whileTestGears.agda @ 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 |
comparison
equal
deleted
inserted
replaced
| 67:946d6b82aad5 | 68:def072b6c016 |
|---|---|
| 179 proof : ( A → B ) → A implies B | 179 proof : ( A → B ) → A implies B |
| 180 | 180 |
| 181 implies2p : {A B : Set } → A implies B → A → B | 181 implies2p : {A B : Set } → A implies B → A → B |
| 182 implies2p (proof x) = x | 182 implies2p (proof x) = x |
| 183 | 183 |
| 184 whileTestPwPSound : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) | 184 whileTestPSem : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) |
| 185 whileTestPwPSound c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) | 185 whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) |
| 186 | 186 |
| 187 SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t) → t ) → Set (succ Zero) | 187 SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t) → t ) → Set (succ Zero) |
| 188 SemGears f = Envc → Envc → Set | 188 SemGears f = Envc → Envc → Set |
| 189 | 189 |
| 190 GearsIdSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} | 190 GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} |
| 191 (f : {l : Level } {t : Set l } → (e0 : Envc ) → pre e0 → ((e : Envc) → post e → t) → t ) | 191 → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t) → t ) |
| 192 → pre e0 → post e1 | 192 → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1))) |
| 193 GearsIdSound e0 e1 f p0 = {!!} | 193 → e1 ≡ f e0 (λ e → e ) |
| 194 | 194 → f e0 (λ e1 → pre e0 implies post e1) |
| 195 hoge : (c : ℕ ) (input output : Envc ) → ? → (vari output ≡ 0) /\ (varn output ≡ c) | 195 GearsUnitSound e0 e1 f fsem refl = fsem e0 |
| 196 hoge c input output sem = GearsIdSound input output {λ e → ⊤} ? tt | 196 |
| 197 whileTestPSemSound : (c : ℕ ) (input output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) | |
| 198 whileTestPSemSound c input output refl = whileTestPSem c | |
| 199 | |
| 197 | 200 |
| 198 -- induction にする | 201 -- induction にする |
| 199 {-# TERMINATING #-} | 202 {-# TERMINATING #-} |
| 200 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t | 203 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t |
| 201 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit | 204 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit |