module hoare-while where

open import Data.Nat
open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary

record Envc : Set (succ Zero) where
  field
    c10 : !$\mathbb{N}$!
    varn : !$\mathbb{N}$!
    vari : !$\mathbb{N}$!
open Envc

whileTestP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! (next : Envc !$\rightarrow$! t) !$\rightarrow$! t
whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )

whileLoopP : {l : Level} {t : Set l} !$\rightarrow$! Envc !$\rightarrow$! (next : Envc !$\rightarrow$! t) !$\rightarrow$! (exit : Envc !$\rightarrow$! t) !$\rightarrow$! t
whileLoopP env next exit with (varn env)
... | zero = exit env
... | suc n = exit (record env { varn = n ; vari = (suc n) })


{-# TERMINATING #-}
loopP : {l : Level} {t : Set l} !$\rightarrow$! Envc !$\rightarrow$! (exit : Envc !$\rightarrow$! t) !$\rightarrow$! t
loopP env exit = whileLoopP env (!$\lambda$! env !$\rightarrow$! loopP env exit ) exit

whileTestPCall : (c10 :  !$\mathbb{N}$! ) !$\rightarrow$! Envc
whileTestPCall c10 = whileTestP {_} {_} c10 (!$\lambda$! env !$\rightarrow$! loopP env (!$\lambda$! env !$\rightarrow$!  env))

---
open import Data.Empty
--open import Relation.Nullary using (!$\neg$!_; Dec; yes; no)

--open import Agda.Builtin.Unit
open import utilities

open import Relation.Binary.PropositionalEquality

open _/\_

data whileTestState  : Set where
  s1 : whileTestState
  s2 : whileTestState
  sf : whileTestState

whileTestStateP : whileTestState !$\rightarrow$! Envc !$\rightarrow$!  Set
whileTestStateP s1 env = (vari env !$\equiv$! 0) /\ (varn env !$\equiv$! c10 env)
whileTestStateP s2 env = (varn env + vari env !$\equiv$! c10 env)
whileTestStateP sf env = (vari env !$\equiv$! c10 env)

whileTestPwP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
   env : Envc
   env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )

whileLoopPwP : {l : Level} {t : Set l}   !$\rightarrow$! (env : Envc ) !$\rightarrow$! whileTestStateP s2 env
    !$\rightarrow$! (next : (env : Envc ) !$\rightarrow$! whileTestStateP s2 env  !$\rightarrow$! t)
    !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env  !$\rightarrow$! t) !$\rightarrow$! t
whileLoopPwP env s next exit with <-cmp 0 (varn env)
whileLoopPwP env s next exit | tri≈ !$\neg$!a b !$\neg$!c = exit env (lem (sym b) s)
  where
    lem : (varn env !$\equiv$! 0) !$\rightarrow$! (varn env + vari env !$\equiv$! c10 env) !$\rightarrow$! vari env !$\equiv$! c10 env
    lem refl refl = refl
whileLoopPwP env s next exit | tri< a !$\neg$!b !$\neg$!c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
  where
    1<0 : 1 !$\leq$! zero !$\rightarrow$! !$\bot$!
    1<0 ()
    proof5 : (suc zero  !$\leq$! (varn  env))  !$\rightarrow$! ((varn env ) - 1) + (vari env + 1) !$\equiv$! c10 env
    proof5 (s!$\leq$!s lt) with varn  env
    proof5 (s!$\leq$!s z!$\leq$!n) | zero = !$\bot$!-elim (1<0 a)
    proof5 (s!$\leq$!s (z!$\leq$!n {n!$\prime$!}) ) | suc n = let open !$\equiv$!-Reasoning in
      begin
        n!$\prime$! + (vari env + 1)
      !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n!$\prime$! + z ) ( +-sym  {vari env} {1} )  !$\rangle$!
        n!$\prime$! + (1 + vari env )
      !$\equiv$!!$\langle$! sym ( +-assoc (n!$\prime$!)  1 (vari env) ) !$\rangle$!
        (n!$\prime$! + 1) + vari env
      !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env )  +1!$\equiv$!suc  !$\rangle$!
        (suc n!$\prime$! ) + vari env
      !$\equiv$!!$\langle$!!$\rangle$!
        varn env + vari env
      !$\equiv$!!$\langle$! s  !$\rangle$!
         c10 env
      !$\blacksquare$!


whileLoopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env
  !$\rightarrow$! (next : (env : Envc ) !$\rightarrow$! (pred n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env  !$\rightarrow$! t)
  !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env  !$\rightarrow$! t) !$\rightarrow$! t
whileLoopPwP!$\prime$! zero env refl refl next exit = exit env refl
whileLoopPwP!$\prime$! (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))



whileTestPSemSound : (c : !$\mathbb{N}$! ) (output : Envc ) !$\rightarrow$! output !$\equiv$! whileTestP c (!$\lambda$! e !$\rightarrow$! e) !$\rightarrow$! !$\top$! implies ((vari output !$\equiv$! 0) /\ (varn output !$\equiv$! c))
whileTestPSemSound c output refl = whileTestPSem c