Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestPrim.agda @ 10:bc819bdda374

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proof completed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Dec 2018 16:59:52 +0900
parents e4f087b823d4
children a622d1700a1b
comparison
equal deleted inserted replaced
9:46b301ad4478 10:bc819bdda374
5 open import Data.Bool hiding ( _≟_ ) 5 open import Data.Bool hiding ( _≟_ )
6 open import Level renaming ( suc to succ ; zero to Zero ) 6 open import Level renaming ( suc to succ ; zero to Zero )
7 open import Relation.Nullary using (¬_; Dec; yes; no) 7 open import Relation.Nullary using (¬_; Dec; yes; no)
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 open import utilities
10 11
11 record Env : Set where 12 record Env : Set where
12 field 13 field
13 varn : ℕ 14 varn : ℕ
14 vari : ℕ 15 vari : ℕ
25 Abort : Comm 26 Abort : Comm
26 PComm : PrimComm -> Comm 27 PComm : PrimComm -> Comm
27 Seq : Comm -> Comm -> Comm 28 Seq : Comm -> Comm -> Comm
28 If : Cond -> Comm -> Comm -> Comm 29 If : Cond -> Comm -> Comm -> Comm
29 While : Cond -> Comm -> Comm 30 While : Cond -> Comm -> Comm
30
31 _-_ : ℕ -> ℕ -> ℕ
32 x - zero = x
33 zero - _ = zero
34 (suc x) - (suc y) = x - y
35
36 lt : ℕ -> ℕ -> Bool
37 lt x y with suc x ≤? y
38 lt x y | yes p = true
39 lt x y | no ¬p = false
40
41 Equal : ℕ -> ℕ -> Bool
42 Equal x y with x ≟ y
43 Equal x y | yes p = true
44 Equal x y | no ¬p = false
45
46 ---------------------------
47
48 implies : Bool → Bool → Bool
49 implies false _ = true
50 implies true true = true
51 implies true false = false
52
53 impl-1 : {x : Bool} → implies x true ≡ true
54 impl-1 {x} with x
55 impl-1 {x} | false = refl
56 impl-1 {x} | true = refl
57
58 impl-2 : {x : Bool} → implies false x ≡ true
59 impl-2 {x} with x
60 impl-2 {x} | false = refl
61 impl-2 {x} | true = refl
62
63 and-lemma-1 : { x y : Bool } → x ∧ y ≡ true → x ≡ true
64 and-lemma-1 {x} {y} eq with x | y | eq
65 and-lemma-1 {x} {y} eq | false | b | ()
66 and-lemma-1 {x} {y} eq | true | false | ()
67 and-lemma-1 {x} {y} eq | true | true | refl = refl
68
69 and-lemma-2 : { x y : Bool } → x ∧ y ≡ true → y ≡ true
70 and-lemma-2 {x} {y} eq with x | y | eq
71 and-lemma-2 {x} {y} eq | false | b | ()
72 and-lemma-2 {x} {y} eq | true | false | ()
73 and-lemma-2 {x} {y} eq | true | true | refl = refl
74
75 bool-case : ( x : Bool ) { p : Set } → ( x ≡ true → p ) → ( x ≡ false → p ) → p
76 bool-case x T F with x
77 bool-case x T F | false = F refl
78 bool-case x T F | true = T refl
79
80 impl : {x y : Bool} → (x ≡ true → y ≡ true ) → implies x y ≡ true
81 impl {x} {y} p = bool-case x (λ x=t → let open ≡-Reasoning in
82 begin
83 implies x y
84 ≡⟨ cong ( \ z -> implies x z ) (p x=t ) ⟩
85 implies x true
86 ≡⟨ impl-1 ⟩
87 true
88 ∎
89 ) ( λ x=f → let open ≡-Reasoning in
90 begin
91 implies x y
92 ≡⟨ cong ( \ z -> implies z y ) x=f ⟩
93 true
94 ∎
95 )
96
97 eqlemma : { x y : ℕ } → Equal x y ≡ true → x ≡ y
98 eqlemma {x} {y} eq with x ≟ y
99 eqlemma {x} {y} refl | yes refl = refl
100 eqlemma {x} {y} () | no ¬p
101
102 eqlemma1 : { x y : ℕ } → Equal x y ≡ Equal (suc x) (suc y)
103 eqlemma1 {x} {y} with x ≟ y
104 eqlemma1 {x} {.x} | yes refl = refl
105 eqlemma1 {x} {y} | no ¬p = refl
106
107 add-lemma1 : { x : ℕ } → x + 1 ≡ suc x
108 add-lemma1 {zero} = refl
109 add-lemma1 {suc x} = cong ( \ z -> suc z ) ( add-lemma1 {x} )
110 31
111 --------------------------- 32 ---------------------------
112 33
113 program : Comm 34 program : Comm
114 program = 35 program =
149 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 70 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true
150 empty-case _ = refl 71 empty-case _ = refl
151 72
152 73
153 Axiom : Cond -> PrimComm -> Cond -> Set 74 Axiom : Cond -> PrimComm -> Cond -> Set
154 Axiom pre comm post = ∀ (env : Env) → implies (pre env) ( post (comm env)) ≡ true 75 Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true
155 76
156 Tautology : Cond -> Cond -> Set 77 Tautology : Cond -> Cond -> Set
157 Tautology pre post = ∀ (env : Env) → implies (pre env) (post env) ≡ true 78 Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true
158 79
159 _/\_ : Cond -> Cond -> Cond 80 _and_ : Cond -> Cond -> Cond
160 x /\ y = λ env → x env ∧ y env 81 x and y = λ env → x env ∧ y env
161 82
162 neg : Cond -> Cond 83 neg : Cond -> Cond
163 neg x = λ env → not ( x env ) 84 neg x = λ env → not ( x env )
164 85
165 data HTProof : Cond -> Comm -> Cond -> Set where 86 data HTProof : Cond -> Comm -> Cond -> Set where
181 HTProof bMid cm2 bPost -> 102 HTProof bMid cm2 bPost ->
182 HTProof bPre (Seq cm1 cm2) bPost 103 HTProof bPre (Seq cm1 cm2) bPost
183 IfRule : {cmThen : Comm} -> {cmElse : Comm} -> 104 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
184 {bPre : Cond} -> {bPost : Cond} -> 105 {bPre : Cond} -> {bPost : Cond} ->
185 {b : Cond} -> 106 {b : Cond} ->
186 HTProof (bPre /\ b) cmThen bPost -> 107 HTProof (bPre and b) cmThen bPost ->
187 HTProof (bPre /\ neg b) cmElse bPost -> 108 HTProof (bPre and neg b) cmElse bPost ->
188 HTProof bPre (If b cmThen cmElse) bPost 109 HTProof bPre (If b cmThen cmElse) bPost
189 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> 110 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
190 HTProof (bInv /\ b) cm bInv -> 111 HTProof (bInv and b) cm bInv ->
191 HTProof bInv (While b cm) (bInv /\ neg b) 112 HTProof bInv (While b cm) (bInv and neg b)
192 113
193 initCond : Cond 114 initCond : Cond
194 initCond env = true 115 initCond env = true
195 116
196 stmt1Cond : Cond 117 stmt1Cond : Cond
201 122
202 whileInv : Cond 123 whileInv : Cond
203 whileInv env = Equal ((varn env) + (vari env)) 10 124 whileInv env = Equal ((varn env) + (vari env)) 10
204 125
205 whileInv' : Cond 126 whileInv' : Cond
206 whileInv' env = Equal ((varn env) + (vari env)) 11 127 whileInv' env = Equal ((varn env) + (vari env)) 11 ∧ lt zero (varn env)
207 128
208 termCond : Cond 129 termCond : Cond
209 termCond env = Equal (vari env) 10 130 termCond env = Equal (vari env) 10
210 131
211 proofs : HTProof initCond simple stmt2Cond 132 proofs : HTProof initCond simple stmt2Cond
234 lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond 155 lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
235 lemma1 env with stmt1Cond env 156 lemma1 env with stmt1Cond env
236 lemma1 env | false = refl 157 lemma1 env | false = refl
237 lemma1 env | true = refl 158 lemma1 env | true = refl
238 lemma21 : {env : Env } → stmt2Cond env ≡ true → varn env ≡ 10 159 lemma21 : {env : Env } → stmt2Cond env ≡ true → varn env ≡ 10
239 lemma21 eq = eqlemma (and-lemma-1 eq) 160 lemma21 eq = Equal→≡ (∧-pi1 eq)
240 lemma22 : {env : Env } → stmt2Cond env ≡ true → vari env ≡ 0 161 lemma22 : {env : Env } → stmt2Cond env ≡ true → vari env ≡ 0
241 lemma22 eq = eqlemma (and-lemma-2 eq) 162 lemma22 eq = Equal→≡ (∧-pi2 eq)
242 lemma23 : {env : Env } → stmt2Cond env ≡ true → varn env + vari env ≡ 10 163 lemma23 : {env : Env } → stmt2Cond env ≡ true → varn env + vari env ≡ 10
243 lemma23 {env} eq = let open ≡-Reasoning in 164 lemma23 {env} eq = let open ≡-Reasoning in
244 begin 165 begin
245 varn env + vari env 166 varn env + vari env
246 ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ 167 ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩
250 ∎ 171 ∎
251 lemma2 : Tautology stmt2Cond whileInv 172 lemma2 : Tautology stmt2Cond whileInv
252 lemma2 env = bool-case (stmt2Cond env) ( 173 lemma2 env = bool-case (stmt2Cond env) (
253 λ eq → let open ≡-Reasoning in 174 λ eq → let open ≡-Reasoning in
254 begin 175 begin
255 implies (stmt2Cond env) (whileInv env) 176 (stmt2Cond env) ⇒ (whileInv env)
256 ≡⟨⟩ 177 ≡⟨⟩
257 implies (stmt2Cond env) ( Equal (varn env + vari env) 10 ) 178 (stmt2Cond env) ⇒ ( Equal (varn env + vari env) 10 )
258 ≡⟨ cong ( \ x -> implies (stmt2Cond env) ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩ 179 ≡⟨ cong ( \ x -> (stmt2Cond env) ⇒ ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩
259 implies (stmt2Cond env) (Equal 10 10) 180 (stmt2Cond env) ⇒ (Equal 10 10)
260 ≡⟨⟩ 181 ≡⟨⟩
261 implies (stmt2Cond env) true 182 (stmt2Cond env) ⇒ true
262 ≡⟨ impl-1 ⟩ 183 ≡⟨ ⇒t ⟩
263 true 184 true
264 ∎ 185 ∎
265 ) ( 186 ) (
266 λ ne → let open ≡-Reasoning in 187 λ ne → let open ≡-Reasoning in
267 begin 188 begin
268 implies (stmt2Cond env) (whileInv env) 189 (stmt2Cond env) ⇒ (whileInv env)
269 ≡⟨ cong ( \ x -> implies x (whileInv env) ) ne ⟩ 190 ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩
270 implies false (whileInv env) 191 false ⇒ (whileInv env)
271 ≡⟨ impl-2 {whileInv env} ⟩ 192 ≡⟨ f⇒ {whileInv env} ⟩
272 true 193 true
273 ∎ 194 ∎
274 ) 195 )
275 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' 196 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
276 lemma3 env = impl ( λ cond → let open ≡-Reasoning in 197 lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in
277 begin 198 begin
278 whileInv' (record { varn = varn env ; vari = vari env + 1 }) 199 whileInv' (record { varn = varn env ; vari = vari env + 1 })
279 ≡⟨⟩ 200 ≡⟨⟩
201 Equal (varn env + (vari env + 1)) 11 ∧ (lt 0 (varn env) )
202 ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) 11 ∧ z ) (∧-pi2 cond ) ⟩
203 Equal (varn env + (vari env + 1)) 11 ∧ true
204 ≡⟨ ∧true ⟩
280 Equal (varn env + (vari env + 1)) 11 205 Equal (varn env + (vari env + 1)) 11
281 ≡⟨ cong ( \ x -> Equal x 11 ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ 206 ≡⟨ cong ( \ x -> Equal x 11 ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
282 Equal ((varn env + vari env) + 1) 11 207 Equal ((varn env + vari env) + 1) 11
283 ≡⟨ cong ( \ x -> Equal x 11 ) add-lemma1 ⟩ 208 ≡⟨ cong ( \ x -> Equal x 11 ) +1≡suc ⟩
284 Equal (suc (varn env + vari env)) 11 209 Equal (suc (varn env + vari env)) 11
285 ≡⟨ sym eqlemma1 ⟩ 210 ≡⟨ sym Equal+1 ⟩
286 Equal ((varn env + vari env) ) 10 211 Equal ((varn env + vari env) ) 10
287 ≡⟨ and-lemma-1 cond ⟩ 212 ≡⟨ ∧-pi1 cond ⟩
288 true 213 true
289 ∎ ) 214 ∎ )
215 lemma41 : (env : Env ) → (varn env + vari env) ≡ 11 → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) 10 ≡ true
216 lemma41 env c1 c2 = let open ≡-Reasoning in
217 begin
218 Equal ((varn env - 1) + vari env) 10
219 ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) 10 ) (sym (suc-predℕ=n c2) ) ⟩
220 Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) 10
221 ≡⟨⟩
222 Equal ((predℕ {varn env} c2 ) + vari env) 10
223 ≡⟨ Equal+1 ⟩
224 Equal ((suc (predℕ {varn env} c2 )) + vari env) 11
225 ≡⟨ cong ( λ z → Equal (z + vari env ) 11 ) (suc-predℕ=n c2 ) ⟩
226 Equal (varn env + vari env) 11
227 ≡⟨ cong ( λ z → (Equal z 11 )) c1 ⟩
228 Equal 11 11
229 ≡⟨⟩
230 true
231 ∎
290 lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv 232 lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
291 lemma4 env = {!!} 233 lemma4 env = impl⇒ ( λ cond → let open ≡-Reasoning in
292 lemma5 : Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond 234 begin
293 lemma5 env = {!!} 235 whileInv (record { varn = varn env - 1 ; vari = vari env })
294 236 ≡⟨⟩
295 237 Equal ((varn env - 1) + vari env) 10
238 ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩
239 true
240 ∎
241 )
242 lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
243 lemma51 z cond with lt zero (varn z) | (suc zero) ≤? (varn z)
244 lemma51 z () | false | yes p
245 lemma51 z () | true | yes p
246 lemma51 z refl | _ | no ¬p with varn z
247 lemma51 z refl | _ | no ¬p | zero = refl
248 lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) )
249 lemma5 : Tautology ((λ e → Equal (varn e + vari e) 10) and (neg (λ z → lt zero (varn z)))) termCond
250 lemma5 env = impl⇒ ( λ cond → let open ≡-Reasoning in
251 begin
252 termCond env
253 ≡⟨⟩
254 Equal (vari env) 10
255 ≡⟨⟩
256 Equal (zero + vari env) 10
257 ≡⟨ cong ( λ z → Equal (z + vari env) 10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩
258 Equal (varn env + vari env) 10
259 ≡⟨ ∧-pi1 cond ⟩
260 true
261 ∎
262 )
263
264
265