Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 56:34601fe34b71

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Sat, 21 Dec 2019 15:47:30 +0900
parents 1be7bb658cf0
children 990d1d892398
comparison
equal deleted inserted replaced
55:1be7bb658cf0 56:34601fe34b71
141 whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t 141 whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
142 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where 142 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
143 env : Envc 143 env : Envc
144 env = whileTestP c10 ( λ env → env ) 144 env = whileTestP c10 ( λ env → env )
145 145
146 whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env 146 whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env
147 → (next : (env : Envc ) → whileTestStateP s2 env → t) 147 → (next : (env : Envc ) → whileTestStateP s2 env → t)
148 → (exit : (env : Envc ) → whileTestStateP sf env → t) → t 148 → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
149 whileLoopPwP env s next exit with <-cmp 0 (varn env) 149 whileLoopPwP env s next exit with <-cmp 0 (varn env)
150 whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s) 150 whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
151 where 151 where
152 lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env 152 lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
153 lem p1 p2 rewrite p1 = p2 153 lem p1 p2 rewrite p1 = p2
154 154
155 whileLoopPwP env s next exit | tri< a ¬b ¬c = 155 whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
156 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!} 156 where
157 1<0 : 1 ≤ zero → ⊥
158 1<0 ()
159 proof5 : (suc zero ≤ (varn env)) → (varn env - 1) + (vari env + 1) ≡ c10 env
160 proof5 (s≤s lt) with varn env
161 proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
162 proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
163 begin
164 n' + (vari env + 1)
165 ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩
166 n' + (1 + vari env )
167 ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩
168 (n' + 1) + vari env
169 ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩
170 (suc n' ) + vari env
171 ≡⟨⟩
172 varn env + vari env
173 ≡⟨ s ⟩
174 c10 env
175 ∎
157 176
158 {-# TERMINATING #-} 177 {-# TERMINATING #-}
159 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t 178 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
160 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit 179 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
161 180
163 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where 182 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where
164 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env 183 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
165 conv e record { pi1 = refl ; pi2 = refl } = +zero 184 conv e record { pi1 = refl ; pi2 = refl } = +zero
166 185
167 Proof : (c : ℕ ) → whileTestPCallwP c 186 Proof : (c : ℕ ) → whileTestPCallwP c
168 Proof c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → {!!} ) ) where 187 Proof zero = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → refl))
188 where
169 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env 189 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
170 conv e record { pi1 = refl ; pi2 = refl } = +zero 190 conv e record { pi1 = refl ; pi2 = refl } = +zero
171 191 Proof (suc c) = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → {!!})) -- Proof c したいが with <-cmp 0 c とか with 0 ≤ c とかするとAgda の check が終わらない
172 192 where
173 193 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
174 194 conv e record { pi1 = refl ; pi2 = refl } = +zero
175