Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/agda-hoare-soundness.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 Soundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
2 HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost
3 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
4 = axiomValid bPre cm bPost pr s1 s2 q1 q2
5 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
6 = substId1 State {Level.zero} {State} {s1} {s2} (proj@$\_{2}$@ q2) (SemCond bPost) q1
7 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
8 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
9 s1 s2 q1 q2
10 = let hyp : Satisfies bPre' cm bPost'
11 hyp = Soundness pr
12 in tautValid bPost' bPost tautPost s2 (hyp s1 s2 (tautValid bPre bPre' tautPre s1 q1) q2)
13 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
14 s1 s2 q1 q2
15 = let hyp1 : Satisfies bPre cm1 bMid
16 hyp1 = Soundness pr1
17 hyp2 : Satisfies bMid cm2 bPost
18 hyp2 = Soundness pr2
19 in hyp2 (proj@$\_{1}$@ q2) s2 (hyp1 s1 (proj@$\_{1}$@ q2) q1 (proj@$\_{1}$@ (proj@$\_{2}$@ q2))) (proj@$\_{2}$@ (proj@$\_{2}$@ q2))
20 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
21 s1 s2 q1 q2
22 = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost
23 hypThen = Soundness pThen
24 hypElse : Satisfies (bPre @$\wedge$@ neg b) cmElse bPost
25 hypElse = Soundness pElse
26 rThen : RelOpState.comp (RelOpState.delta (SemCond b))
27 (SemComm cmThen) s1 s2 @$\rightarrow$@ SemCond bPost s2
28 rThen = @$\lambda$@ h @$\rightarrow$@ hypThen s1 s2 ((proj@$\_{2}$@ (respAnd bPre b s1)) (q1 , proj@$\_{1}$@ t1))
29 (proj@$\_{2}$@ ((proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h))
30 rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
31 (SemComm cmElse) s1 s2 @$\rightarrow$@ SemCond bPost s2
32 rElse = @$\lambda$@ h @$\rightarrow$@
33 let t10 : (NotP (SemCond b) s1) @$\times$@ (SemComm cmElse s1 s2)
34 t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre
35 (NotP (SemCond b)) (SemComm cmElse) s1 s2) h
36 in hypElse s1 s2 (proj@$\_{2}$@ (respAnd bPre (neg b) s1)
37 (q1 , (proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)))) (proj@$\_{2}$@ t10)
38 in when rThen rElse q2
39 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
40 = proj@$\_{2}$@ (respAnd bInv (neg b) s2)
41 (lem1 (proj@$\_{1}$@ q2) s2 (proj@$\_{1}$@ t15) , proj@$\_{2}$@ (respNeg b s2) (proj@$\_{2}$@ t15))
42 where
43 hyp : Satisfies (bInv @$\wedge$@ b) cm' bInv
44 hyp = Soundness pr
45 Rel1 : @$\mathbb{N}$@ @$\rightarrow$@ Rel State (Level.zero)
46 Rel1 = @$\lambda$@ m @$\rightarrow$@
47 RelOpState.repeat
48 m
49 (RelOpState.comp (RelOpState.delta (SemCond b))
50 (SemComm cm'))
51 t15 : (Rel1 (proj@$\_{1}$@ q2) s1 s2) @$\times$@ (NotP (SemCond b) s2)
52 t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost
53 (NotP (SemCond b)) (Rel1 (proj@$\_{1}$@ q2)) s1 s2) (proj@$\_{2}$@ q2)
54 lem1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ SemCond bInv ss2
55 lem1 zero ss2 h = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1
56 lem1 (suc n) ss2 h
57 = let hyp2 : (z : State) @$\rightarrow$@ Rel1 (proj@$\_{1}$@ q2) s1 z @$\rightarrow$@
58 SemCond bInv z
59 hyp2 = lem1 n
60 t22 : (SemCond b (proj@$\_{1}$@ h)) @$\times$@ (SemComm cm' (proj@$\_{1}$@ h) ss2)
61 t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') (proj@$\_{1}$@ h) ss2)
62 (proj@$\_{2}$@ (proj@$\_{2}$@ h))
63 t23 : SemCond (bInv @$\wedge$@ b) (proj@$\_{1}$@ h)
64 t23 = proj@$\_{2}$@ (respAnd bInv b (proj@$\_{1}$@ h))
65 (hyp2 (proj@$\_{1}$@ h) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) , proj@$\_{1}$@ t22)
66 in hyp (proj@$\_{1}$@ h) ss2 t23 (proj@$\_{2}$@ t22)