Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 50:2edb44c5bf52

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add s1~3, proofs
author ryokka
date Wed, 18 Dec 2019 20:08:58 +0900
parents 91d6d8097a39
children 3f4f93ac841d
comparison
equal deleted inserted replaced
49:91d6d8097a39 50:2edb44c5bf52
131 c10 : ℕ 131 c10 : ℕ
132 cx : whileTestStateP c10 (vari env) (varn env) 132 cx : whileTestStateP c10 (vari env) (varn env)
133 133
134 open EnvP 134 open EnvP
135 135
136 s1 : (c10 : ℕ) → EnvP
137 s1 c10 = record {env = record {vari = 0 ; varn = c10} ; c10 = c10 ; cx = pstate1 (record {pi1 = refl ; pi2 = refl})}
138
139 s2 : (e : EnvP) → varn (env e) > 0 → varn (env e) < c10 e → EnvP
140 s2 e n>0 n<c10 with <-cmp 0 (varn (env e))
141 s2 e n>0 n<c10 | tri< a ¬b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pstate2 {!!} {!!} {!!} }
142 s2 e n>0 n<c10 | tri≈ ¬a b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pfinstate {!!} {!!} }
143
144 s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e
145 s3 record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl = {!!}
146
147 proofs : (c : ℕ) (e : EnvP) → vari (env e) ≡ c10 e
148 proofs c e = s3 (s2 (s1 {!!}) {!!} {!!}) {!!}
149
150
136 whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t 151 whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t
137 whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where 152 whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where
138 env1 : Env 153 env1 : Env
139 env1 = whileTestP c10 ( λ e → e ) 154 env1 = whileTestP c10 ( λ e → e )
140 cx1 : whileTestStateP c10 (vari env1) (varn env1) 155 cx1 : whileTestStateP c10 (vari env1) (varn env1)