Mercurial > hg > Papers > 2021 > soto-thesis
diff prepaper/src/whileTestPrimProof.agda.replaced @ 0:3dba680da508
init-test
| author | soto |
|---|---|
| date | Tue, 08 Dec 2020 19:06:49 +0900 |
| parents | |
| children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prepaper/src/whileTestPrimProof.agda.replaced Tue Dec 08 19:06:49 2020 +0900 @@ -0,0 +1,288 @@ +module whileTestPrimProof where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ ) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +open import utilities hiding ( _@$\wedge$@_ ) +open import whileTestPrim + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +open Env + +initCond : Cond +initCond env = true + +stmt1Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +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 +init-case {c10} _ = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ @$\equiv$@@$\rightarrow$@Equal refl ) + +init-type : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (@$\lambda$@ env @$\rightarrow$@ true) (@$\lambda$@ env @$\rightarrow$@ record { varn = c10 ; vari = vari env }) (stmt1Cond {c10}) +init-type {c10} env = init-case env + +stmt2Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0) + +lemma1 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + (Equal (varn env) c10 ) @$\wedge$@ true + @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ + Equal (varn env) c10 + @$\equiv$@@$\langle$@ cond @$\rangle$@ + true + @$\blacksquare$@ ) + +-- simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm +-- simple c10 = +-- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) +-- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}) + +proofs : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (simple c10) (stmt2Cond {c10}) +proofs c10 = + SeqRule {initCond} ( PrimRule (init-case {c10} )) + $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10}) + +open import Data.Empty + +open import Data.Nat.Properties + +whileInv : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) @$\wedge$@ lt zero (varn env) + +termCond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +termCond {c10} env = Equal (vari env) c10 + + +-- program : @$\mathbb{N}$@ @$\rightarrow$@ Comm +-- program c10 = +-- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) +-- $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})) +-- $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) ) +-- (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} )) +-- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} )) + + +proof1 : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (program c10 ) (termCond {c10}) +proof1 c10 = + SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule (init-case {c10} )) + $ SeqRule {@$\lambda$@ e @$\rightarrow$@ Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) c10) @$\wedge$@ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + where + lemma21 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env @$\equiv$@ c10 + lemma21 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 eq) + lemma22 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond {c10} env @$\equiv$@ true @$\rightarrow$@ vari env @$\equiv$@ 0 + lemma22 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi2 eq) + lemma23 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 + lemma23 {env} {c10} eq = let open @$\equiv$@-Reasoning in + begin + varn env + vari env + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x + vari env ) (lemma21 eq ) @$\rangle$@ + c10 + vari env + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ c10 + x) (lemma22 {env} {c10} eq ) @$\rangle$@ + c10 + 0 + @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ + 0 + c10 + @$\equiv$@@$\langle$@@$\rangle$@ + c10 + @$\blacksquare$@ + lemma2 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology stmt2Cond whileInv + lemma2 {c10} env = bool-case (stmt2Cond env) ( + @$\lambda$@ eq @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + (stmt2Cond env) @$\Rightarrow$@ (whileInv env) + @$\equiv$@@$\langle$@@$\rangle$@ + (stmt2Cond env) @$\Rightarrow$@ ( Equal (varn env + vari env) c10 ) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ ( Equal x c10 ) ) ( lemma23 {env} eq ) @$\rangle$@ + (stmt2Cond env) @$\Rightarrow$@ (Equal c10 c10) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ x ) (@$\equiv$@@$\rightarrow$@Equal refl ) @$\rangle$@ + (stmt2Cond {c10} env) @$\Rightarrow$@ true + @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@ + true + @$\blacksquare$@ + ) ( + @$\lambda$@ ne @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + (stmt2Cond env) @$\Rightarrow$@ (whileInv env) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x @$\Rightarrow$@ (whileInv env) ) ne @$\rangle$@ + false @$\Rightarrow$@ (whileInv {c10} env) + @$\equiv$@@$\langle$@ f@$\Rightarrow$@ {whileInv {c10} env} @$\rangle$@ + true + @$\blacksquare$@ + ) + lemma3 : Axiom (@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e)) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = vari env + 1 }) whileInv' + lemma3 env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + @$\equiv$@@$\langle$@@$\rangle$@ + Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ (lt 0 (varn env) ) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ z ) (@$\wedge$@-pi2 cond ) @$\rangle$@ + Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ true + @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ + Equal (varn env + (vari env + 1)) (suc c10) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) @$\rangle$@ + Equal ((varn env + vari env) + 1) (suc c10) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) +1@$\equiv$@suc @$\rangle$@ + Equal (suc (varn env + vari env)) (suc c10) + @$\equiv$@@$\langle$@ sym Equal+1 @$\rangle$@ + Equal ((varn env + vari env) ) c10 + @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@ + true + @$\blacksquare$@ ) + 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 + lemma41 env {c10} c1 c2 = let open @$\equiv$@-Reasoning in + begin + Equal ((varn env - 1) + vari env) c10 + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-pred@$\mathbb{N}$@=n c2) ) @$\rangle$@ + Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 ) - 1) + vari env) c10 + @$\equiv$@@$\langle$@@$\rangle$@ + Equal ((pred@$\mathbb{N}$@ {varn env} c2 ) + vari env) c10 + @$\equiv$@@$\langle$@ Equal+1 @$\rangle$@ + Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 )) + vari env) (suc c10) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env ) (suc c10) ) (suc-pred@$\mathbb{N}$@=n c2 ) @$\rangle$@ + Equal (varn env + vari env) (suc c10) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ (Equal z (suc c10) )) c1 @$\rangle$@ + Equal (suc c10) (suc c10) + @$\equiv$@@$\langle$@ @$\equiv$@@$\rightarrow$@Equal refl @$\rangle$@ + true + @$\blacksquare$@ + lemma4 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom whileInv' (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + whileInv (record { varn = varn env - 1 ; vari = vari env }) + @$\equiv$@@$\langle$@@$\rangle$@ + Equal ((varn env - 1) + vari env) c10 + @$\equiv$@@$\langle$@ lemma41 env (Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 cond)) (@$\wedge$@-pi2 cond) @$\rangle$@ + true + @$\blacksquare$@ + ) + lemma51 : (z : Env ) @$\rightarrow$@ neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)) z @$\equiv$@ true @$\rightarrow$@ varn z @$\equiv$@ zero + lemma51 z cond with varn z + lemma51 z refl | zero = refl + lemma51 z () | suc x + 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 + lemma5 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + termCond env + @$\equiv$@@$\langle$@@$\rangle$@ + Equal (vari env) c10 + @$\equiv$@@$\langle$@@$\rangle$@ + Equal (zero + vari env) c10 + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env) c10 ) (sym ( lemma51 env ( @$\wedge$@-pi2 cond ) )) @$\rangle$@ + Equal (varn env + vari env) c10 + @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@ + true + @$\blacksquare$@ + ) + +--- necessary definitions for Hoare.agda ( Soundness ) + +State : Set +State = Env + +open import RelOp +module RelOpState = RelOp State + +open import Data.Product +open import Relation.Binary + +NotP : {S : Set} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S +NotP X s = @$\neg$@ X s + +_@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +b1 @$\wedge$@ b2 = b1 and b2 + +_\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2) + +SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set +SemCond c p = c p @$\equiv$@ true + +tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@ + (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ SemCond b2 s +tautValid b1 b2 taut s cond with b1 s | b2 s | taut s +tautValid b1 b2 taut s () | false | false | refl +tautValid b1 b2 taut s _ | false | true | refl = refl +tautValid b1 b2 taut s _ | true | false | () +tautValid b1 b2 taut s _ | true | true | refl = refl + +respNeg : (b : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s) +respNeg b s = ( left , right ) where + left : not (b s) @$\equiv$@ true @$\rightarrow$@ (b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@ + left ne with b s + left refl | false = @$\lambda$@ () + left () | true + right : ((b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@) @$\rightarrow$@ not (b s) @$\equiv$@ true + right ne with b s + right ne | false = refl + right ne | true = @$\bot$@-elim ( ne refl ) + +respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (b1 @$\wedge$@ b2) s) + ((SemCond b1 s) @$\times$@ (SemCond b2 s)) +respAnd b1 b2 s = ( left , right ) where + left : b1 s @$\wedge$@ b2 s @$\equiv$@ true @$\rightarrow$@ (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true) + left and with b1 s | b2 s + left () | false | false + left () | false | true + left () | true | false + left refl | true | true = ( refl , refl ) + right : (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true) @$\rightarrow$@ b1 s @$\wedge$@ b2 s @$\equiv$@ true + right ( x1 , x2 ) with b1 s | b2 s + right (() , ()) | false | false + right (() , _) | false | true + right (_ , ()) | true | false + right (refl , refl) | true | true = refl + +PrimSemComm : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l +PrimSemComm prim s1 s2 = Id State (prim s1) s2 + + + +axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@ + (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@ + SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ SemCond bPost s2 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl + +open import HoareSoundness + Cond + PrimComm + neg + _and_ + Tautology + State + SemCond + tautValid + respNeg + respAnd + PrimSemComm + Axiom + axiomValid + +PrimSoundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht + + +proofOfProgram : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (input output : Env ) + @$\rightarrow$@ initCond input @$\equiv$@ true + @$\rightarrow$@ (SemComm (program c10) input output) + @$\rightarrow$@ termCond {c10} output @$\equiv$@ true +proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem