Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 39:2eb30c8e5a20

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
whileLoopStep
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Dec 2019 09:25:45 +0900
parents 7049fbaf5e18
children a9cac7960e81
comparison
equal deleted inserted replaced
38:7049fbaf5e18 39:2eb30c8e5a20
124 open import Relation.Nullary 124 open import Relation.Nullary
125 open import Relation.Binary 125 open import Relation.Binary
126 126
127 127
128 {-# TERMINATING #-} 128 {-# TERMINATING #-}
129 whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 1 ≤ varn e → t) (Code : (e : Env) → 0 ≡ varn e → t) → t 129 whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → 1 ≤ varn e → t) (exit : (e : Env) → 0 ≡ varn e → t) → t
130 whileLoopStep env next exit with <-cmp 0 (varn env) 130 whileLoopStep env next exit with <-cmp 0 (varn env)
131 whileLoopStep env next exit | tri≈ _ eq _ = exit env eq 131 whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
132 whileLoopStep env next exit | tri< gt ¬eq _ = {!!} 132 whileLoopStep env next exit | tri< gt ¬eq _ = next env gt
133 where 133 whileLoopStep env next exit | tri> _ _ c = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl)
134 lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1)
135 lem env (s≤s 1<varn) with 1 ≤? varn env
136 lem env (s≤s 1<varn) | no ¬p = {!!}
137 lem env (s≤s 1<varn) | yes p = ⊥-elim (¬eq ({!!}))
138 -- n が 0 の時 は正しい、　n が1の時正しくない
139
140 whileLoopStep env next exit | tri> _ _ c = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen
141 134
142 whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t 135 whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
143 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where 136 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
144 out : Env 137 out : Env
145 out = whileTest (c10 cxt) ( λ e → e ) 138 out = whileTest (c10 cxt) ( λ e → e )