|
1
|
1 module whileTestPrimProof where
|
|
|
2
|
|
|
3 open import Function
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.Bool hiding ( _≟_ )
|
|
|
6 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
7 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9
|
|
|
10 open import utilities hiding ( _/\_ )
|
|
|
11 open import whileTestPrim
|
|
|
12
|
|
|
13 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
|
|
|
14
|
|
|
15 open Env
|
|
|
16
|
|
|
17 initCond : Cond
|
|
|
18 initCond env = true
|
|
|
19
|
|
|
20 stmt1Cond : {c10 : ℕ} → Cond
|
|
|
21 stmt1Cond {c10} env = Equal (varn env) c10
|
|
|
22
|
|
|
23 init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true
|
|
|
24 init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
|
|
|
25
|
|
|
26 init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10})
|
|
|
27 init-type {c10} env = init-case env
|
|
|
28
|
|
|
29 stmt2Cond : {c10 : ℕ} → Cond
|
|
|
30 stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
|
|
|
31
|
|
|
32 lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
|
|
|
33 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
34 begin
|
|
|
35 (Equal (varn env) c10 ) ∧ true
|
|
|
36 ≡⟨ ∧true ⟩
|
|
|
37 Equal (varn env) c10
|
|
|
38 ≡⟨ cond ⟩
|
|
|
39 true
|
|
|
40 ∎ )
|
|
|
41
|
|
|
42 -- simple : ℕ → Comm
|
|
|
43 -- simple c10 =
|
|
|
44 -- Seq ( PComm (λ env → record env {varn = c10}))
|
|
|
45 -- $ PComm (λ env → record env {vari = 0})
|
|
|
46
|
|
|
47 proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
|
|
|
48 proofs c10 =
|
|
|
49 SeqRule {initCond} ( PrimRule (init-case {c10} ))
|
|
|
50 $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10})
|
|
|
51
|
|
|
52 open import Data.Empty
|
|
|
53
|
|
|
54 open import Data.Nat.Properties
|
|
|
55
|
|
|
56 whileInv : {c10 : ℕ} → Cond
|
|
|
57 whileInv {c10} env = Equal ((varn env) + (vari env)) c10
|
|
|
58
|
|
|
59 whileInv' : {c10 : ℕ} → Cond
|
|
|
60 whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
|
|
|
61
|
|
|
62 termCond : {c10 : ℕ} → Cond
|
|
|
63 termCond {c10} env = Equal (vari env) c10
|
|
|
64
|
|
|
65
|
|
|
66 -- program : ℕ → Comm
|
|
|
67 -- program c10 =
|
|
|
68 -- Seq ( PComm (λ env → record env {varn = c10}))
|
|
|
69 -- $ Seq ( PComm (λ env → record env {vari = 0}))
|
|
|
70 -- $ While (λ env → lt zero (varn env ) )
|
|
|
71 -- (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
|
|
|
72 -- $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
|
|
|
73
|
|
|
74
|
|
|
75 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
|
|
|
76 proof1 c10 =
|
|
|
77 SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
|
|
|
78 $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 )
|
|
|
79 $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 (
|
|
|
80 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
|
|
|
81 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
|
|
|
82 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
|
|
|
83 where
|
|
|
84 lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
|
|
|
85 lemma21 eq = Equal→≡ (∧-pi1 eq)
|
|
|
86 lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
|
|
|
87 lemma22 eq = Equal→≡ (∧-pi2 eq)
|
|
|
88 lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
|
|
|
89 lemma23 {env} {c10} eq = let open ≡-Reasoning in
|
|
|
90 begin
|
|
|
91 varn env + vari env
|
|
|
92 ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩
|
|
|
93 c10 + vari env
|
|
|
94 ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
|
|
|
95 c10 + 0
|
|
|
96 ≡⟨ +-sym {c10} {0} ⟩
|
|
|
97 0 + c10
|
|
|
98 ≡⟨⟩
|
|
|
99 c10
|
|
|
100 ∎
|
|
|
101 lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv
|
|
|
102 lemma2 {c10} env = bool-case (stmt2Cond env) (
|
|
|
103 λ eq → let open ≡-Reasoning in
|
|
|
104 begin
|
|
|
105 (stmt2Cond env) ⇒ (whileInv env)
|
|
|
106 ≡⟨⟩
|
|
|
107 (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 )
|
|
|
108 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
|
|
|
109 (stmt2Cond env) ⇒ (Equal c10 c10)
|
|
|
110 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩
|
|
|
111 (stmt2Cond {c10} env) ⇒ true
|
|
|
112 ≡⟨ ⇒t ⟩
|
|
|
113 true
|
|
|
114 ∎
|
|
|
115 ) (
|
|
|
116 λ ne → let open ≡-Reasoning in
|
|
|
117 begin
|
|
|
118 (stmt2Cond env) ⇒ (whileInv env)
|
|
|
119 ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩
|
|
|
120 false ⇒ (whileInv {c10} env)
|
|
|
121 ≡⟨ f⇒ {whileInv {c10} env} ⟩
|
|
|
122 true
|
|
|
123 ∎
|
|
|
124 )
|
|
|
125 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
|
|
|
126 lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
127 begin
|
|
|
128 whileInv' (record { varn = varn env ; vari = vari env + 1 })
|
|
|
129 ≡⟨⟩
|
|
|
130 Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
|
|
|
131 ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩
|
|
|
132 Equal (varn env + (vari env + 1)) (suc c10) ∧ true
|
|
|
133 ≡⟨ ∧true ⟩
|
|
|
134 Equal (varn env + (vari env + 1)) (suc c10)
|
|
|
135 ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
|
|
|
136 Equal ((varn env + vari env) + 1) (suc c10)
|
|
|
137 ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
|
|
|
138 Equal (suc (varn env + vari env)) (suc c10)
|
|
|
139 ≡⟨ sym Equal+1 ⟩
|
|
|
140 Equal ((varn env + vari env) ) c10
|
|
|
141 ≡⟨ ∧-pi1 cond ⟩
|
|
|
142 true
|
|
|
143 ∎ )
|
|
|
144 lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true
|
|
|
145 lemma41 env {c10} c1 c2 = let open ≡-Reasoning in
|
|
|
146 begin
|
|
|
147 Equal ((varn env - 1) + vari env) c10
|
|
|
148 ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩
|
|
|
149 Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
|
|
|
150 ≡⟨⟩
|
|
|
151 Equal ((predℕ {varn env} c2 ) + vari env) c10
|
|
|
152 ≡⟨ Equal+1 ⟩
|
|
|
153 Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
|
|
|
154 ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩
|
|
|
155 Equal (varn env + vari env) (suc c10)
|
|
|
156 ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
|
|
|
157 Equal (suc c10) (suc c10)
|
|
|
158 ≡⟨ ≡→Equal refl ⟩
|
|
|
159 true
|
|
|
160 ∎
|
|
|
161 lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
|
|
|
162 lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
163 begin
|
|
|
164 whileInv (record { varn = varn env - 1 ; vari = vari env })
|
|
|
165 ≡⟨⟩
|
|
|
166 Equal ((varn env - 1) + vari env) c10
|
|
|
167 ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩
|
|
|
168 true
|
|
|
169 ∎
|
|
|
170 )
|
|
|
171 lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
|
|
|
172 lemma51 z cond with varn z
|
|
|
173 lemma51 z refl | zero = refl
|
|
|
174 lemma51 z () | suc x
|
|
|
175 lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
|
|
|
176 lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
177 begin
|
|
|
178 termCond env
|
|
|
179 ≡⟨⟩
|
|
|
180 Equal (vari env) c10
|
|
|
181 ≡⟨⟩
|
|
|
182 Equal (zero + vari env) c10
|
|
|
183 ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩
|
|
|
184 Equal (varn env + vari env) c10
|
|
|
185 ≡⟨ ∧-pi1 cond ⟩
|
|
|
186 true
|
|
|
187 ∎
|
|
|
188 )
|
|
|
189
|
|
|
190 --- necessary definitions for Hoare.agda ( Soundness )
|
|
|
191
|
|
|
192 State : Set
|
|
|
193 State = Env
|
|
|
194
|
|
|
195 open import RelOp
|
|
|
196 module RelOpState = RelOp State
|
|
|
197
|
|
|
198 open import Data.Product
|
|
|
199 open import Relation.Binary
|
|
|
200
|
|
|
201 NotP : {S : Set} -> Pred S -> Pred S
|
|
|
202 NotP X s = ¬ X s
|
|
|
203
|
|
|
204 _/\_ : Cond -> Cond -> Cond
|
|
|
205 b1 /\ b2 = b1 and b2
|
|
|
206
|
|
|
207 _\/_ : Cond -> Cond -> Cond
|
|
|
208 b1 \/ b2 = neg (neg b1 /\ neg b2)
|
|
|
209
|
|
|
210 SemCond : Cond -> State -> Set
|
|
|
211 SemCond c p = c p ≡ true
|
|
|
212
|
|
|
213 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
|
|
|
214 (s : State) -> SemCond b1 s -> SemCond b2 s
|
|
|
215 tautValid b1 b2 taut s cond with b1 s | b2 s | taut s
|
|
|
216 tautValid b1 b2 taut s () | false | false | refl
|
|
|
217 tautValid b1 b2 taut s _ | false | true | refl = refl
|
|
|
218 tautValid b1 b2 taut s _ | true | false | ()
|
|
|
219 tautValid b1 b2 taut s _ | true | true | refl = refl
|
|
|
220
|
|
|
221 respNeg : (b : Cond) -> (s : State) ->
|
|
|
222 Iff (SemCond (neg b) s) (¬ SemCond b s)
|
|
|
223 respNeg b s = ( left , right ) where
|
|
|
224 left : not (b s) ≡ true → (b s) ≡ true → ⊥
|
|
|
225 left ne with b s
|
|
|
226 left refl | false = λ ()
|
|
|
227 left () | true
|
|
|
228 right : ((b s) ≡ true → ⊥) → not (b s) ≡ true
|
|
|
229 right ne with b s
|
|
|
230 right ne | false = refl
|
|
|
231 right ne | true = ⊥-elim ( ne refl )
|
|
|
232
|
|
|
233 respAnd : (b1 b2 : Cond) -> (s : State) ->
|
|
|
234 Iff (SemCond (b1 /\ b2) s)
|
|
|
235 ((SemCond b1 s) × (SemCond b2 s))
|
|
|
236 respAnd b1 b2 s = ( left , right ) where
|
|
|
237 left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true)
|
|
|
238 left and with b1 s | b2 s
|
|
|
239 left () | false | false
|
|
|
240 left () | false | true
|
|
|
241 left () | true | false
|
|
|
242 left refl | true | true = ( refl , refl )
|
|
|
243 right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true
|
|
|
244 right ( x1 , x2 ) with b1 s | b2 s
|
|
|
245 right (() , ()) | false | false
|
|
|
246 right (() , _) | false | true
|
|
|
247 right (_ , ()) | true | false
|
|
|
248 right (refl , refl) | true | true = refl
|
|
|
249
|
|
|
250 PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
|
|
|
251 PrimSemComm prim s1 s2 = Id State (prim s1) s2
|
|
|
252
|
|
|
253
|
|
|
254
|
|
|
255 axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
|
|
|
256 (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
|
|
|
257 SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2
|
|
|
258 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
|
|
|
259 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
|
|
|
260 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
|
|
|
261 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
|
|
|
262 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
|
|
|
263
|
|
|
264 open import HoareSoundness
|
|
|
265 Cond
|
|
|
266 PrimComm
|
|
|
267 neg
|
|
|
268 _and_
|
|
|
269 Tautology
|
|
|
270 State
|
|
|
271 SemCond
|
|
|
272 tautValid
|
|
|
273 respNeg
|
|
|
274 respAnd
|
|
|
275 PrimSemComm
|
|
|
276 Axiom
|
|
|
277 axiomValid
|
|
|
278
|
|
|
279 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
|
|
|
280 HTProof bPre cm bPost -> Satisfies bPre cm bPost
|
|
|
281 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
|
|
|
282
|
|
|
283
|
|
|
284 proofOfProgram : (c10 : ℕ) → (input output : Env )
|
|
|
285 → initCond input ≡ true
|
|
|
286 → (SemComm (program c10) input output)
|
|
|
287 → termCond {c10} output ≡ true
|
|
|
288 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem
|
