Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/agda-hoare-soundness.agda.replaced @ 13:e8655e0264b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix paper, slide
author ryokka
date Tue, 11 Feb 2020 02:31:26 +0900
parents bf3288c36d7e
children
comparison
equal deleted inserted replaced
12:bf3288c36d7e 13:e8655e0264b8
14 s1 s2 q1 q2 14 s1 s2 q1 q2
15 = let hyp1 : Satisfies bPre cm1 bMid 15 = let hyp1 : Satisfies bPre cm1 bMid
16 hyp1 = Soundness pr1 16 hyp1 = Soundness pr1
17 hyp2 : Satisfies bMid cm2 bPost 17 hyp2 : Satisfies bMid cm2 bPost
18 hyp2 = Soundness pr2 18 hyp2 = Soundness pr2
19 sMid : State 19 in hyp2 (proj@$\_{1}$@ q2) s2 (hyp1 s1 (proj@$\_{1}$@ q2) q1 (proj@$\_{1}$@ (proj@$\_{2}$@ q2))) (proj@$\_{2}$@ (proj@$\_{2}$@ q2))
20 sMid = proj@$\_{1}$@ q2
21 r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2
22 r1 = proj@$\_{2}$@ q2
23 r2 : SemComm cm1 s1 sMid
24 r2 = proj@$\_{1}$@ r1
25 r3 : SemComm cm2 sMid s2
26 r3 = proj@$\_{2}$@ r1
27 r4 : SemCond bMid sMid
28 r4 = hyp1 s1 sMid q1 r2
29 in hyp2 sMid s2 r4 r3
30 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) 20 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
31 s1 s2 q1 q2 21 s1 s2 q1 q2
32 = let hypThen : Satisfies (bPre /\ b) cmThen bPost 22 = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost
33 hypThen = Soundness pThen 23 hypThen = Soundness pThen
34 hypElse : Satisfies (bPre /\ neg b) cmElse bPost 24 hypElse : Satisfies (bPre @$\wedge$@ neg b) cmElse bPost
35 hypElse = Soundness pElse 25 hypElse = Soundness pElse
36 rThen : RelOpState.comp 26 rThen : RelOpState.comp (RelOpState.delta (SemCond b))
37 (RelOpState.delta (SemCond b)) 27 (SemComm cmThen) s1 s2 @$\rightarrow$@ SemCond bPost s2
38 (SemComm cmThen) s1 s2 @$\rightarrow$@ 28 rThen = @$\lambda$@ h @$\rightarrow$@ hypThen s1 s2 ((proj@$\_{2}$@ (respAnd bPre b s1)) (q1 , proj@$\_{1}$@ t1))
39 SemCond bPost s2 29 (proj@$\_{2}$@ ((proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h))
40 rThen = @$\lambda$@ h @$\rightarrow$@ 30 rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
41 let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2 31 (SemComm cmElse) s1 s2 @$\rightarrow$@ SemCond bPost s2
42 t1 = (proj@$\_{2}$@ (RelOpState.deltaRestPre
43 (SemCond b)
44 (SemComm cmThen) s1 s2)) h
45 t2 : SemCond (bPre /\ b) s1
46 t2 = (proj@$\_{2}$@ (respAnd bPre b s1))
47 (q1 , proj@$\_{1}$@ t1)
48 in hypThen s1 s2 t2 (proj@$\_{2}$@ t1)
49 rElse : RelOpState.comp
50 (RelOpState.delta (NotP (SemCond b)))
51 (SemComm cmElse) s1 s2 @$\rightarrow$@
52 SemCond bPost s2
53 rElse = @$\lambda$@ h @$\rightarrow$@ 32 rElse = @$\lambda$@ h @$\rightarrow$@
54 let t10 : (NotP (SemCond b) s1) @$\times$@ 33 let t10 : (NotP (SemCond b) s1) @$\times$@ (SemComm cmElse s1 s2)
55 (SemComm cmElse s1 s2)
56 t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre 34 t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre
57 (NotP (SemCond b)) (SemComm cmElse) s1 s2) 35 (NotP (SemCond b)) (SemComm cmElse) s1 s2) h
58 h 36 in hypElse s1 s2 (proj@$\_{2}$@ (respAnd bPre (neg b) s1)
59 t6 : SemCond (neg b) s1 37 (q1 , (proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)))) (proj@$\_{2}$@ t10)
60 t6 = proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)
61 t7 : SemComm cmElse s1 s2
62 t7 = proj@$\_{2}$@ t10
63 t8 : SemCond (bPre /\ neg b) s1
64 t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1)
65 (q1 , t6)
66 in hypElse s1 s2 t8 t7
67 in when rThen rElse q2 38 in when rThen rElse q2
68 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 39 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
69 = proj@$\_{2}$@ (respAnd bInv (neg b) s2) t20 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))
70 where 42 where
71 hyp : Satisfies (bInv /\ b) cm' bInv 43 hyp : Satisfies (bInv @$\wedge$@ b) cm' bInv
72 hyp = Soundness pr 44 hyp = Soundness pr
73 n : $mathbb{N}$ 45 Rel1 : @$\mathbb{N}$@ @$\rightarrow$@ Rel State (Level.zero)
74 n = proj@$\_{1}$@ q2
75 Rel1 : $mathbb{N}$ @$\rightarrow$@ Rel State (Level.zero)
76 Rel1 = @$\lambda$@ m @$\rightarrow$@ 46 Rel1 = @$\lambda$@ m @$\rightarrow$@
77 RelOpState.repeat 47 RelOpState.repeat
78 m 48 m
79 (RelOpState.comp (RelOpState.delta (SemCond b)) 49 (RelOpState.comp (RelOpState.delta (SemCond b))
80 (SemComm cm')) 50 (SemComm cm'))
81 t1 : RelOpState.comp 51 t15 : (Rel1 (proj@$\_{1}$@ q2) s1 s2) @$\times$@ (NotP (SemCond b) s2)
82 (Rel1 n)
83 (RelOpState.delta (NotP (SemCond b))) s1 s2
84 t1 = proj@$\_{2}$@ q2
85 t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2)
86 t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost 52 t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost
87 (NotP (SemCond b)) (Rel1 n) s1 s2) 53 (NotP (SemCond b)) (Rel1 (proj@$\_{1}$@ q2)) s1 s2) (proj@$\_{2}$@ q2)
88 t1 54 lem1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ SemCond bInv ss2
89 t16 : Rel1 n s1 s2 55 lem1 zero ss2 h = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1
90 t16 = proj@$\_{1}$@ t15 56 lem1 (suc n) ss2 h
91 t17 : NotP (SemCond b) s2 57 = let hyp2 : (z : State) @$\rightarrow$@ Rel1 (proj@$\_{1}$@ q2) s1 z @$\rightarrow$@
92 t17 = proj@$\_{2}$@ t15
93 lem1 : (m : $mathbb{N}$) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@
94 SemCond bInv ss2
95 lem1 $mathbb{N}$.zero ss2 h
96 = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1
97 lem1 ($mathbb{N}$.suc n) ss2 h
98 = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@
99 SemCond bInv z 58 SemCond bInv z
100 hyp2 = lem1 n 59 hyp2 = lem1 n
101 s20 : State 60 t22 : (SemCond b (proj@$\_{1}$@ h)) @$\times$@ (SemComm cm' (proj@$\_{1}$@ h) ss2)
102 s20 = proj@$\_{1}$@ h 61 t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') (proj@$\_{1}$@ h) ss2)
103 t21 : Rel1 n s1 s20
104 t21 = proj@$\_{1}$@ (proj@$\_{2}$@ h)
105 t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2)
106 t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre
107 (SemCond b) (SemComm cm') s20 ss2)
108 (proj@$\_{2}$@ (proj@$\_{2}$@ h)) 62 (proj@$\_{2}$@ (proj@$\_{2}$@ h))
109 t23 : SemCond (bInv /\ b) s20 63 t23 : SemCond (bInv @$\wedge$@ b) (proj@$\_{1}$@ h)
110 t23 = proj@$\_{2}$@ (respAnd bInv b s20) 64 t23 = proj@$\_{2}$@ (respAnd bInv b (proj@$\_{1}$@ h))
111 (hyp2 s20 t21 , proj@$\_{1}$@ t22) 65 (hyp2 (proj@$\_{1}$@ h) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) , proj@$\_{1}$@ t22)
112 in hyp s20 ss2 t23 (proj@$\_{2}$@ t22) 66 in hyp (proj@$\_{1}$@ h) ss2 t23 (proj@$\_{2}$@ t22)
113 t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2
114 t20 = lem1 n s2 t16 , proj@$\_{2}$@ (respNeg b s2) t17