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