Mercurial > hg > Papers > 2021 > soto-thesis
comparison prepaper/src/whileTestPrimProof.agda.replaced @ 0:3dba680da508
init-test
| author | soto |
|---|---|
| date | Tue, 08 Dec 2020 19:06:49 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:3dba680da508 |
|---|---|
| 1 module whileTestPrimProof where | |
| 2 | |
| 3 open import Function | |
| 4 open import Data.Nat | |
| 5 open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ ) | |
| 6 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 7 open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) | |
| 8 open import Relation.Binary.PropositionalEquality | |
| 9 | |
| 10 open import utilities hiding ( _@$\wedge$@_ ) | |
| 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 : @$\mathbb{N}$@} @$\rightarrow$@ Cond | |
| 21 stmt1Cond {c10} env = Equal (varn env) c10 | |
| 22 | |
| 23 init-case : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (( @$\lambda$@ e @$\rightarrow$@ true @$\Rightarrow$@ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) @$\equiv$@ true | |
| 24 init-case {c10} _ = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ @$\equiv$@@$\rightarrow$@Equal refl ) | |
| 25 | |
| 26 init-type : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (@$\lambda$@ env @$\rightarrow$@ true) (@$\lambda$@ env @$\rightarrow$@ record { varn = c10 ; vari = vari env }) (stmt1Cond {c10}) | |
| 27 init-type {c10} env = init-case env | |
| 28 | |
| 29 stmt2Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond | |
| 30 stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0) | |
| 31 | |
| 32 lemma1 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) | |
| 33 lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in | |
| 34 begin | |
| 35 (Equal (varn env) c10 ) @$\wedge$@ true | |
| 36 @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ | |
| 37 Equal (varn env) c10 | |
| 38 @$\equiv$@@$\langle$@ cond @$\rangle$@ | |
| 39 true | |
| 40 @$\blacksquare$@ ) | |
| 41 | |
| 42 -- simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm | |
| 43 -- simple c10 = | |
| 44 -- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) | |
| 45 -- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}) | |
| 46 | |
| 47 proofs : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ 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 : @$\mathbb{N}$@} @$\rightarrow$@ Cond | |
| 57 whileInv {c10} env = Equal ((varn env) + (vari env)) c10 | |
| 58 | |
| 59 whileInv' : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond | |
| 60 whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) @$\wedge$@ lt zero (varn env) | |
| 61 | |
| 62 termCond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond | |
| 63 termCond {c10} env = Equal (vari env) c10 | |
| 64 | |
| 65 | |
| 66 -- program : @$\mathbb{N}$@ @$\rightarrow$@ Comm | |
| 67 -- program c10 = | |
| 68 -- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) | |
| 69 -- $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})) | |
| 70 -- $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) ) | |
| 71 -- (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} )) | |
| 72 -- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} )) | |
| 73 | |
| 74 | |
| 75 proof1 : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (program c10 ) (termCond {c10}) | |
| 76 proof1 c10 = | |
| 77 SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule (init-case {c10} )) | |
| 78 $ SeqRule {@$\lambda$@ e @$\rightarrow$@ Equal (varn e) c10} ( PrimRule lemma1 ) | |
| 79 $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) c10) @$\wedge$@ (Equal (vari e) 0)} lemma2 ( | |
| 80 WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) c10} | |
| 81 $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e) } lemma3 ) | |
| 82 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 | |
| 83 where | |
| 84 lemma21 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env @$\equiv$@ c10 | |
| 85 lemma21 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 eq) | |
| 86 lemma22 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond {c10} env @$\equiv$@ true @$\rightarrow$@ vari env @$\equiv$@ 0 | |
| 87 lemma22 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi2 eq) | |
| 88 lemma23 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 | |
| 89 lemma23 {env} {c10} eq = let open @$\equiv$@-Reasoning in | |
| 90 begin | |
| 91 varn env + vari env | |
| 92 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x + vari env ) (lemma21 eq ) @$\rangle$@ | |
| 93 c10 + vari env | |
| 94 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ c10 + x) (lemma22 {env} {c10} eq ) @$\rangle$@ | |
| 95 c10 + 0 | |
| 96 @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ | |
| 97 0 + c10 | |
| 98 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 99 c10 | |
| 100 @$\blacksquare$@ | |
| 101 lemma2 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology stmt2Cond whileInv | |
| 102 lemma2 {c10} env = bool-case (stmt2Cond env) ( | |
| 103 @$\lambda$@ eq @$\rightarrow$@ let open @$\equiv$@-Reasoning in | |
| 104 begin | |
| 105 (stmt2Cond env) @$\Rightarrow$@ (whileInv env) | |
| 106 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 107 (stmt2Cond env) @$\Rightarrow$@ ( Equal (varn env + vari env) c10 ) | |
| 108 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ ( Equal x c10 ) ) ( lemma23 {env} eq ) @$\rangle$@ | |
| 109 (stmt2Cond env) @$\Rightarrow$@ (Equal c10 c10) | |
| 110 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ x ) (@$\equiv$@@$\rightarrow$@Equal refl ) @$\rangle$@ | |
| 111 (stmt2Cond {c10} env) @$\Rightarrow$@ true | |
| 112 @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@ | |
| 113 true | |
| 114 @$\blacksquare$@ | |
| 115 ) ( | |
| 116 @$\lambda$@ ne @$\rightarrow$@ let open @$\equiv$@-Reasoning in | |
| 117 begin | |
| 118 (stmt2Cond env) @$\Rightarrow$@ (whileInv env) | |
| 119 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x @$\Rightarrow$@ (whileInv env) ) ne @$\rangle$@ | |
| 120 false @$\Rightarrow$@ (whileInv {c10} env) | |
| 121 @$\equiv$@@$\langle$@ f@$\Rightarrow$@ {whileInv {c10} env} @$\rangle$@ | |
| 122 true | |
| 123 @$\blacksquare$@ | |
| 124 ) | |
| 125 lemma3 : Axiom (@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e)) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = vari env + 1 }) whileInv' | |
| 126 lemma3 env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in | |
| 127 begin | |
| 128 whileInv' (record { varn = varn env ; vari = vari env + 1 }) | |
| 129 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 130 Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ (lt 0 (varn env) ) | |
| 131 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ z ) (@$\wedge$@-pi2 cond ) @$\rangle$@ | |
| 132 Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ true | |
| 133 @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ | |
| 134 Equal (varn env + (vari env + 1)) (suc c10) | |
| 135 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) @$\rangle$@ | |
| 136 Equal ((varn env + vari env) + 1) (suc c10) | |
| 137 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) +1@$\equiv$@suc @$\rangle$@ | |
| 138 Equal (suc (varn env + vari env)) (suc c10) | |
| 139 @$\equiv$@@$\langle$@ sym Equal+1 @$\rangle$@ | |
| 140 Equal ((varn env + vari env) ) c10 | |
| 141 @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@ | |
| 142 true | |
| 143 @$\blacksquare$@ ) | |
| 144 lemma41 : (env : Env ) @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ (varn env + vari env) @$\equiv$@ (suc c10) @$\rightarrow$@ lt 0 (varn env) @$\equiv$@ true @$\rightarrow$@ Equal ((varn env - 1) + vari env) c10 @$\equiv$@ true | |
| 145 lemma41 env {c10} c1 c2 = let open @$\equiv$@-Reasoning in | |
| 146 begin | |
| 147 Equal ((varn env - 1) + vari env) c10 | |
| 148 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-pred@$\mathbb{N}$@=n c2) ) @$\rangle$@ | |
| 149 Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 ) - 1) + vari env) c10 | |
| 150 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 151 Equal ((pred@$\mathbb{N}$@ {varn env} c2 ) + vari env) c10 | |
| 152 @$\equiv$@@$\langle$@ Equal+1 @$\rangle$@ | |
| 153 Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 )) + vari env) (suc c10) | |
| 154 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env ) (suc c10) ) (suc-pred@$\mathbb{N}$@=n c2 ) @$\rangle$@ | |
| 155 Equal (varn env + vari env) (suc c10) | |
| 156 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ (Equal z (suc c10) )) c1 @$\rangle$@ | |
| 157 Equal (suc c10) (suc c10) | |
| 158 @$\equiv$@@$\langle$@ @$\equiv$@@$\rightarrow$@Equal refl @$\rangle$@ | |
| 159 true | |
| 160 @$\blacksquare$@ | |
| 161 lemma4 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom whileInv' (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env - 1 ; vari = vari env }) whileInv | |
| 162 lemma4 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in | |
| 163 begin | |
| 164 whileInv (record { varn = varn env - 1 ; vari = vari env }) | |
| 165 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 166 Equal ((varn env - 1) + vari env) c10 | |
| 167 @$\equiv$@@$\langle$@ lemma41 env (Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 cond)) (@$\wedge$@-pi2 cond) @$\rangle$@ | |
| 168 true | |
| 169 @$\blacksquare$@ | |
| 170 ) | |
| 171 lemma51 : (z : Env ) @$\rightarrow$@ neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)) z @$\equiv$@ true @$\rightarrow$@ varn z @$\equiv$@ zero | |
| 172 lemma51 z cond with varn z | |
| 173 lemma51 z refl | zero = refl | |
| 174 lemma51 z () | suc x | |
| 175 lemma5 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology ((@$\lambda$@ e @$\rightarrow$@ Equal (varn e + vari e) c10) and (neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)))) termCond | |
| 176 lemma5 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in | |
| 177 begin | |
| 178 termCond env | |
| 179 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 180 Equal (vari env) c10 | |
| 181 @$\equiv$@@$\langle$@@$\rangle$@ | |
| 182 Equal (zero + vari env) c10 | |
| 183 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env) c10 ) (sym ( lemma51 env ( @$\wedge$@-pi2 cond ) )) @$\rangle$@ | |
| 184 Equal (varn env + vari env) c10 | |
| 185 @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@ | |
| 186 true | |
| 187 @$\blacksquare$@ | |
| 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} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S | |
| 202 NotP X s = @$\neg$@ X s | |
| 203 | |
| 204 _@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond | |
| 205 b1 @$\wedge$@ b2 = b1 and b2 | |
| 206 | |
| 207 _\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond | |
| 208 b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2) | |
| 209 | |
| 210 SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set | |
| 211 SemCond c p = c p @$\equiv$@ true | |
| 212 | |
| 213 tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@ | |
| 214 (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ 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) @$\rightarrow$@ (s : State) @$\rightarrow$@ | |
| 222 Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s) | |
| 223 respNeg b s = ( left , right ) where | |
| 224 left : not (b s) @$\equiv$@ true @$\rightarrow$@ (b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@ | |
| 225 left ne with b s | |
| 226 left refl | false = @$\lambda$@ () | |
| 227 left () | true | |
| 228 right : ((b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@) @$\rightarrow$@ not (b s) @$\equiv$@ true | |
| 229 right ne with b s | |
| 230 right ne | false = refl | |
| 231 right ne | true = @$\bot$@-elim ( ne refl ) | |
| 232 | |
| 233 respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ | |
| 234 Iff (SemCond (b1 @$\wedge$@ b2) s) | |
| 235 ((SemCond b1 s) @$\times$@ (SemCond b2 s)) | |
| 236 respAnd b1 b2 s = ( left , right ) where | |
| 237 left : b1 s @$\wedge$@ b2 s @$\equiv$@ true @$\rightarrow$@ (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ 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 @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true) @$\rightarrow$@ b1 s @$\wedge$@ b2 s @$\equiv$@ 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 : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l | |
| 251 PrimSemComm prim s1 s2 = Id State (prim s1) s2 | |
| 252 | |
| 253 | |
| 254 | |
| 255 axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@ | |
| 256 (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@ | |
| 257 SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ 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} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ | |
| 280 HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost | |
| 281 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht | |
| 282 | |
| 283 | |
| 284 proofOfProgram : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (input output : Env ) | |
| 285 @$\rightarrow$@ initCond input @$\equiv$@ true | |
| 286 @$\rightarrow$@ (SemComm (program c10) input output) | |
| 287 @$\rightarrow$@ termCond {c10} output @$\equiv$@ true | |
| 288 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem |