Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 35:7c739972cd26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add loopProof
author ryokka
date Fri, 13 Dec 2019 19:23:15 +0900
parents 9caff4e4a402
children 320b765a6424
comparison
equal deleted inserted replaced
34:9caff4e4a402 35:7c739972cd26
121 open import Relation.Nullary 121 open import Relation.Nullary
122 open import Relation.Binary 122 open import Relation.Binary
123 123
124 124
125 {-# TERMINATING #-} 125 {-# TERMINATING #-}
126 whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 0 < varn e → t) (Code : (e : Env) → 0 ≡ varn e → t) → t 126 whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 1 ≤ varn e → t) (Code : (e : Env) → 0 ≡ varn e → t) → t
127 whileLoopStep env next exit with <-cmp 0 (varn env) 127 whileLoopStep env next exit with <-cmp 0 (varn env)
128 whileLoopStep env next exit | tri≈ _ eq _ = exit env eq 128 whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
129 whileLoopStep env next exit | tri< gt _ _ = 129 whileLoopStep env next exit | tri< gt _ _ = {!!}
130 next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) (lem env gt)
131 where 130 where
132 lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1) 131 lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1)
133 lem record { varn = (suc na) ; vari = vari } (s≤s gt) with na ≟ 0 132 lem env 1<varn = {!!}
134 lem record { varn = (suc na) ; vari = vari } (s≤s gt) | does₁ because proof₁ = {!!} 133 -- n が 0 の時 は正しい、　n が1の時正しくない
135 -- n が 0 の時正しくない
136 134
137 whileLoopStep env next exit | tri> _ _ c = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen 135 whileLoopStep env next exit | tri> _ _ c = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen
138 136
139 whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t 137 whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
140 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where 138 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
175 173
176 {-# TERMINATING #-} 174 {-# TERMINATING #-}
177 loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t 175 loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t
178 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit 176 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
179 177
178
179
180 loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (d : Dec (P c))
181 → Pre c → (Context → (continue : (c1 : Context) → ¬ (P c1) → Inv c1 → t)
182 → (exit : (c2 : Context) → (P c2) → Post c2 → t) → t) → t
183 loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (false because proof₁) f =
184 loopProof {!!} {!!} {!!}
185 loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (true because proof₁) f = {!!}
186
187
180 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 188 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
181 $ λ cxt → whileConvProof cxt 189 $ λ cxt → whileConvProof cxt
182 $ λ cxt → loop cxt 190 $ λ cxt → loop cxt
183 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt 191 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
184 proofWhileGear c cxt = {!!} 192 proofWhileGear c cxt = {!!}
185 193
194
195 CodeGear : {l : Level} {t : Set l} → (cont : Set → t) → (exit : Set → t) → t
196 CodeGear = {!!}
197