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