--- a/WhileTest.agda	Thu Feb 11 17:30:33 2021 +0900
+++ b/WhileTest.agda	Thu Feb 11 19:33:35 2021 +0900
@@ -9,12 +9,28 @@
 open import Function
 open import logic
 
---open import Data.Bool hiding ( _≟_ ) -- ; _≤?_ ; _≤_ ; _<_)
---open import Relation.Binary.PropositionalEquality
+open import Data.Bool hiding ( _∧_ ;  _≟_ ) -- ; _∧_ ; _≤_ ; _<_)
+open import Data.Product
 open import Agda.Builtin.Unit
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+open import Data.Empty
+open import Data.Nat.Properties
+
+-- logicへ
++zero : { y : ℕ } → y + zero  ≡ y
++zero {zero} = refl
++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+
+-- utilへ
+_-_ : ℕ → ℕ → ℕ
+x - zero  = x
+zero - _  = zero
+(suc x) - (suc y)  = x - y
 
 record Env : Set (Suc Zero) where
   field
+    c10 : ℕ
     varn : ℕ
     vari : ℕ
 open Env
@@ -22,23 +38,24 @@
 data _implies_  (A B : Set ) : Set (Suc Zero) where
     proof : ( A → B ) → A implies B
 
+implies2p : {A B : Set } → A implies B  → A → B
+implies2p (proof x) = x
+
 data whileTestState  : Set where
   s1 : whileTestState
   s2 : whileTestState
   sf : whileTestState
 
-whileTestStateP : whileTestState → Env → ℕ → Set
-whileTestStateP s1 env c10 = (vari env ≡ 0) ∧ (varn env ≡ c10)
-whileTestStateP s2 env c10 = (varn env + vari env ≡ c10 )
-whileTestStateP sf env c10 = (vari env ≡ c10)
+whileTestStateP : whileTestState → Env → Set
+whileTestStateP s1 env = (vari env ≡ 0) ∧ (varn env ≡ c10 env)
+whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
+whileTestStateP sf env = (vari env ≡ c10 env)
 
 record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
   field
     env : Env
   whileInit :  {m : Level }  {t : Set m } → (c10 : ℕ) → (Env → t) → t
-  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
-  whileInit-impl : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env c10) )
-  whileInit-impl c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } )
+  whileInit c10 next = next (record {c10 = c10 ; varn = c10 ; vari = 0 } )
   whileLoop : Env → (Code : Env → t) → t
   whileLoop env next = whileLoop1 (varn env) env where
       whileLoop1 : ℕ → Env → t
@@ -47,10 +64,58 @@
   whileTest : (c10 : ℕ) → (Env → t) → t
   whileTest c10 next = whileInit c10 $ λ env → whileLoop env next
 
+  loopPP : (n : ℕ) → (input : Env ) → (n ≡ varn input) → Env
+  loopPP zero input refl = input
+  loopPP (suc n) input refl = loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl
+
+  -- init
+  whileInit-impl : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env) )
+  whileInit-impl c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } )
+  whileTestPSemSound : (c : ℕ ) (output : Env ) → output ≡ whileInit c (λ e → e) → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c))
+  whileTestPSemSound c output refl = whileInit-impl c
+  -- init → loop
+  whileConvPSemSound : {l : Level} → (input : Env) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input)
+  whileConvPSemSound input = proof λ x → (conv input x) where
+    conv : (env : Env ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env ) → varn env + vari env ≡ c10 env
+    conv e record { proj1 = refl ; proj2 = refl } = +zero
+  -- loop → loop
+  whileLoopPSem : {l : Level} {t : Set l}  → (input : Env )  → whileTestStateP s2 input
+   → (next : (output : Env ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
+   → (exit : (output : Env ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
+  whileLoopPSem env s next exit with varn env | s
+  ... | zero | _ = exit env (proof (λ z → z))
+  ... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) )
+  -- loop → fin
+
+  loopPPSem : (input output : Env ) →  output ≡ loopPP (varn input)  input refl
+    → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
+  loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
+    where
+      lem : (n : ℕ) → (env : Env) → n + suc (vari env) ≡ suc (n + vari env)
+      lem n env = +-suc (n) (vari env)
+      loopPPSemInduct : (n : ℕ) → (current : Env) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP n current eq)
+        → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+      loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
+      loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
+          whileLoopPSem current refl
+              (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
+              (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
+
+
+  whileLoopPSemSound : {l : Level} → (input output : Env )
+    → whileTestStateP s2 input
+    →  output ≡ loopPP (varn input) input refl
+    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
+  whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
+
+  whileTestSound : {l : Level} (c : ℕ) → (output : Env) → ⊤ →  whileTestStateP sf output
+  whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top =
+    implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileInit c (λ e → e)) refl) top))
+
 open WhileTest
 
 createWhileTest : {m : Level} {t : Set m }  → WhileTest {m} {t}
-createWhileTest  = record { env = record { varn = 0; vari = 0 } }
+createWhileTest  = record { env = record { c10 = 0; varn = 0; vari = 0 } }
 
 test2 : ℕ
 test2 = whileTest createWhileTest 10 $ λ e → vari e