Mercurial > hg > Papers > 2020 > soto-midterm

diff src/whileTestPrimProof.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/whileTestPrimProof.agda.replaced	Tue Sep 08 18:38:08 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