Mercurial > hg > Members > ryokka > HoareLogic
annotate HoareSoundness.agda @ 50:2edb44c5bf52
add s1~3, proofs
| author | ryokka |
|---|---|
| date | Wed, 18 Dec 2019 20:08:58 +0900 |
| parents | e668962ac31a |
| children | 222dd3869ab0 |
| rev | line source |
|---|---|
| 18 | 1 {-# OPTIONS --universe-polymorphism #-} |
| 2 | |
| 3 open import Level | |
| 4 open import Data.Nat | |
| 5 open import Data.Product | |
| 6 open import Data.Bool | |
| 20 | 7 open import Data.Empty |
| 21 | 8 open import Data.Sum |
| 18 | 9 open import Relation.Binary |
| 10 open import Relation.Nullary | |
| 11 open import Relation.Binary.Core | |
| 19 | 12 open import Relation.Binary.PropositionalEquality |
| 21 | 13 open import RelOp |
|
22
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
14 open import utilities |
| 18 | 15 |
| 24 | 16 module HoareSoundness |
|
22
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
17 (Cond : Set) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
18 (PrimComm : Set) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
19 (neg : Cond -> Cond) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
20 (_/\_ : Cond -> Cond -> Cond) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
21 (Tautology : Cond -> Cond -> Set) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
22 (State : Set) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
23 (SemCond : Cond -> State -> Set) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
24 (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
25 (s : State) -> SemCond b1 s -> SemCond b2 s) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
26 (respNeg : (b : Cond) -> (s : State) -> |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
27 Iff (SemCond (neg b) s) (¬ SemCond b s)) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
28 (respAnd : (b1 b2 : Cond) -> (s : State) -> |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
29 Iff (SemCond (b1 /\ b2) s) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
30 ((SemCond b1 s) × (SemCond b2 s))) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
31 (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
32 (Axiom : Cond -> PrimComm -> Cond -> Set) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
33 (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
34 (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
35 SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where |
| 18 | 36 |
| 24 | 37 open import Hoare PrimComm Cond Axiom Tautology _/\_ neg |
|
22
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
38 |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
39 open import RelOp |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
40 module RelOpState = RelOp State |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
41 |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
42 NotP : {S : Set} -> Pred S -> Pred S |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
43 NotP X s = ¬ X s |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
44 |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
45 _\/_ : Cond -> Cond -> Cond |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
46 b1 \/ b2 = neg (neg b1 /\ neg b2) |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
47 |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
48 _==>_ : Cond -> Cond -> Cond |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
49 b1 ==> b2 = neg (b1 \/ b2) |
| 18 | 50 |
| 19 | 51 when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> |
| 52 X ⊎ Y -> Z | |
| 53 when f g (inj₁ x) = f x | |
| 54 when f g (inj₂ y) = g y | |
| 18 | 55 |
| 56 -- semantics of commands | |
| 19 | 57 SemComm : Comm -> Rel State (Level.zero) |
| 58 SemComm Skip = RelOpState.deltaGlob | |
| 59 SemComm Abort = RelOpState.emptyRel | |
| 18 | 60 SemComm (PComm pc) = PrimSemComm pc |
| 19 | 61 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) |
| 18 | 62 SemComm (If b c1 c2) |
| 19 | 63 = RelOpState.union |
| 64 (RelOpState.comp (RelOpState.delta (SemCond b)) | |
| 18 | 65 (SemComm c1)) |
| 19 | 66 (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) |
| 18 | 67 (SemComm c2)) |
| 68 SemComm (While b c) | |
| 19 | 69 = RelOpState.unionInf |
| 18 | 70 (λ (n : ℕ) -> |
| 19 | 71 RelOpState.comp (RelOpState.repeat |
| 18 | 72 n |
| 19 | 73 (RelOpState.comp |
| 74 (RelOpState.delta (SemCond b)) | |
| 18 | 75 (SemComm c))) |
| 19 | 76 (RelOpState.delta (NotP (SemCond b)))) |
| 18 | 77 |
| 78 Satisfies : Cond -> Comm -> Cond -> Set | |
| 79 Satisfies bPre cm bPost | |
| 80 = (s1 : State) -> (s2 : State) -> | |
| 19 | 81 SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2 |
| 18 | 82 |
| 83 Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> | |
| 84 HTProof bPre cm bPost -> Satisfies bPre cm bPost | |
| 85 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 | |
| 86 = axiomValid bPre cm bPost pr s1 s2 q1 q2 | |
| 87 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2 | |
| 20 | 88 = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1 |
| 18 | 89 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () |
| 90 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) | |
| 91 s1 s2 q1 q2 | |
| 92 = let hyp : Satisfies bPre' cm bPost' | |
| 93 hyp = Soundness pr | |
| 94 r1 : SemCond bPre' s1 | |
| 95 r1 = tautValid bPre bPre' tautPre s1 q1 | |
| 96 r2 : SemCond bPost' s2 | |
| 97 r2 = hyp s1 s2 r1 q2 | |
| 98 in tautValid bPost' bPost tautPost s2 r2 | |
| 99 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) | |
| 100 s1 s2 q1 q2 | |
| 101 = let hyp1 : Satisfies bPre cm1 bMid | |
| 102 hyp1 = Soundness pr1 | |
| 103 hyp2 : Satisfies bMid cm2 bPost | |
| 104 hyp2 = Soundness pr2 | |
| 105 sMid : State | |
| 106 sMid = proj₁ q2 | |
| 107 r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2 | |
| 108 r1 = proj₂ q2 | |
| 109 r2 : SemComm cm1 s1 sMid | |
| 110 r2 = proj₁ r1 | |
| 111 r3 : SemComm cm2 sMid s2 | |
| 112 r3 = proj₂ r1 | |
| 113 r4 : SemCond bMid sMid | |
| 114 r4 = hyp1 s1 sMid q1 r2 | |
| 115 in hyp2 sMid s2 r4 r3 | |
| 116 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) | |
| 117 s1 s2 q1 q2 | |
| 118 = let hypThen : Satisfies (bPre /\ b) cmThen bPost | |
| 119 hypThen = Soundness pThen | |
| 120 hypElse : Satisfies (bPre /\ neg b) cmElse bPost | |
| 121 hypElse = Soundness pElse | |
| 19 | 122 rThen : RelOpState.comp |
| 123 (RelOpState.delta (SemCond b)) | |
| 18 | 124 (SemComm cmThen) s1 s2 -> |
| 125 SemCond bPost s2 | |
| 126 rThen = λ h -> | |
| 127 let t1 : SemCond b s1 × SemComm cmThen s1 s2 | |
| 19 | 128 t1 = (proj₂ (RelOpState.deltaRestPre |
| 18 | 129 (SemCond b) |
| 130 (SemComm cmThen) s1 s2)) h | |
| 131 t2 : SemCond (bPre /\ b) s1 | |
| 132 t2 = (proj₂ (respAnd bPre b s1)) | |
| 133 (q1 , proj₁ t1) | |
| 134 in hypThen s1 s2 t2 (proj₂ t1) | |
| 19 | 135 rElse : RelOpState.comp |
| 136 (RelOpState.delta (NotP (SemCond b))) | |
| 18 | 137 (SemComm cmElse) s1 s2 -> |
| 138 SemCond bPost s2 | |
| 139 rElse = λ h -> | |
| 140 let t10 : (NotP (SemCond b) s1) × | |
| 141 (SemComm cmElse s1 s2) | |
| 19 | 142 t10 = proj₂ (RelOpState.deltaRestPre |
| 18 | 143 (NotP (SemCond b)) (SemComm cmElse) s1 s2) |
| 144 h | |
| 145 t6 : SemCond (neg b) s1 | |
| 146 t6 = proj₂ (respNeg b s1) (proj₁ t10) | |
| 147 t7 : SemComm cmElse s1 s2 | |
| 148 t7 = proj₂ t10 | |
| 149 t8 : SemCond (bPre /\ neg b) s1 | |
| 150 t8 = proj₂ (respAnd bPre (neg b) s1) | |
| 151 (q1 , t6) | |
| 152 in hypElse s1 s2 t8 t7 | |
| 153 in when rThen rElse q2 | |
| 154 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 | |
| 155 = proj₂ (respAnd bInv (neg b) s2) t20 | |
| 156 where | |
| 157 hyp : Satisfies (bInv /\ b) cm' bInv | |
| 158 hyp = Soundness pr | |
| 159 n : ℕ | |
| 160 n = proj₁ q2 | |
| 161 Rel1 : ℕ -> Rel State (Level.zero) | |
| 162 Rel1 = λ m -> | |
| 19 | 163 RelOpState.repeat |
| 18 | 164 m |
| 19 | 165 (RelOpState.comp (RelOpState.delta (SemCond b)) |
| 18 | 166 (SemComm cm')) |
| 19 | 167 t1 : RelOpState.comp |
| 18 | 168 (Rel1 n) |
| 19 | 169 (RelOpState.delta (NotP (SemCond b))) s1 s2 |
| 18 | 170 t1 = proj₂ q2 |
| 171 t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2) | |
| 19 | 172 t15 = proj₂ (RelOpState.deltaRestPost |
| 18 | 173 (NotP (SemCond b)) (Rel1 n) s1 s2) |
| 174 t1 | |
| 175 t16 : Rel1 n s1 s2 | |
| 176 t16 = proj₁ t15 | |
| 177 t17 : NotP (SemCond b) s2 | |
| 178 t17 = proj₂ t15 | |
| 179 lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 -> | |
| 180 SemCond bInv ss2 | |
| 181 lem1 ℕ.zero ss2 h | |
| 20 | 182 = substId1 State (proj₂ h) (SemCond bInv) q1 |
| 18 | 183 lem1 (ℕ.suc n) ss2 h |
| 184 = let hyp2 : (z : State) -> Rel1 n s1 z -> | |
| 185 SemCond bInv z | |
| 186 hyp2 = lem1 n | |
| 187 s20 : State | |
| 188 s20 = proj₁ h | |
| 189 t21 : Rel1 n s1 s20 | |
| 190 t21 = proj₁ (proj₂ h) | |
| 191 t22 : (SemCond b s20) × (SemComm cm' s20 ss2) | |
| 19 | 192 t22 = proj₂ (RelOpState.deltaRestPre |
| 18 | 193 (SemCond b) (SemComm cm') s20 ss2) |
| 194 (proj₂ (proj₂ h)) | |
| 195 t23 : SemCond (bInv /\ b) s20 | |
| 196 t23 = proj₂ (respAnd bInv b s20) | |
| 197 (hyp2 s20 t21 , proj₁ t22) | |
| 198 in hyp s20 ss2 t23 (proj₂ t22) | |
| 199 t20 : SemCond bInv s2 × SemCond (neg b) s2 | |
| 200 t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17 |