--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/whileTestProof.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,65 @@
+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