module whileTestProof where
--
-- Using imply relation to make soundness explicit
-- termination is shown by induction on varn
--

data _implies_  (A B : Set ) : Set (succ Zero) where
    proof : ( A @$\rightarrow$@ B ) @$\rightarrow$@ A implies B

implies2p : {A B : Set } @$\rightarrow$@ A implies B  @$\rightarrow$@ A @$\rightarrow$@ B
implies2p (proof x) = x

whileTestPSem :  (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestP c ( @$\lambda$@ env @$\rightarrow$@ ⊤ implies (whileTestStateP s1 env) )
whileTestPSem c = proof ( @$\lambda$@ _ @$\rightarrow$@ record { pi1 = refl ; pi2 = refl } )

SemGears : (f : {l : Level } {t : Set l } @$\rightarrow$@ (e0 : Envc ) @$\rightarrow$@ ((e : Envc) @$\rightarrow$@ t)  @$\rightarrow$@ t ) @$\rightarrow$@ Set (succ Zero)
SemGears f = Envc @$\rightarrow$@ Envc @$\rightarrow$@ Set

GearsUnitSound : (e0 e1 : Envc) {pre : Envc @$\rightarrow$@ Set} {post : Envc @$\rightarrow$@ Set}
   @$\rightarrow$@ (f : {l : Level } {t : Set l } @$\rightarrow$@ (e0 : Envc ) @$\rightarrow$@ (Envc @$\rightarrow$@ t)  @$\rightarrow$@ t )
   @$\rightarrow$@ (fsem : (e0 : Envc ) @$\rightarrow$@ f e0 ( @$\lambda$@ e1 @$\rightarrow$@ (pre e0) implies (post e1)))
   @$\rightarrow$@ f e0 (@$\lambda$@ e1 @$\rightarrow$@ pre e0 implies post e1)
GearsUnitSound e0 e1 f fsem = fsem e0

whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ ⊤ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c))
whileTestPSemSound c output refl = proof (@$\lambda$@ x @$\rightarrow$@ record { pi1 = refl ; pi2 = refl })
-- whileTestPSem c


whileConvPSemSound : {l : Level} @$\rightarrow$@ (input : Envc) @$\rightarrow$@ (whileTestStateP s1 input ) implies (whileTestStateP s2 input)
whileConvPSemSound input = proof @$\lambda$@ x @$\rightarrow$@ (conv input x) where
  conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env
  conv e record { pi1 = refl ; pi2 = refl } = +zero

loopPP : (n : @$\mathbb{N}$@) @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn input) @$\rightarrow$@ Envc
loopPP zero input refl = input
loopPP (suc n) input refl =
    loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl

whileLoopPSem : {l : Level} {t : Set l}   @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ whileTestStateP s2 input
  @$\rightarrow$@ (next : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  @$\rightarrow$@ t)
  @$\rightarrow$@ (exit : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output)  @$\rightarrow$@ t) @$\rightarrow$@ t
whileLoopPSem env s next exit with varn env | s
... | zero | _ = exit env (proof (@$\lambda$@ z @$\rightarrow$@ z))
... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof @$\lambda$@ x @$\rightarrow$@ +-suc varn (vari env) )

loopPPSem : (input output : Envc ) @$\rightarrow$@  output @$\equiv$@ loopPP (varn input)  input refl
  @$\rightarrow$@ (whileTestStateP s2 input ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output)
loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
  where
    lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env)
    lem n env = +-suc (n) (vari env)
    loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@  (loopeq : output @$\equiv$@ loopPP n current eq)
      @$\rightarrow$@ (whileTestStateP s2 current ) @$\rightarrow$@ (whileTestStateP s2 current ) implies (whileTestStateP sf output)
    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl)
    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
        whileLoopPSem current refl
            (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
            (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)

whileLoopPSemSound : {l : Level} @$\rightarrow$@ (input output : Envc )
   @$\rightarrow$@ whileTestStateP s2 input
   @$\rightarrow$@  output @$\equiv$@ loopPP (varn input) input refl
   @$\rightarrow$@ (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre