changeset 82:33a6fd61c3e6

writing Soundness conect
author ryokka
date Thu, 02 Jan 2020 20:22:24 +0900
parents 0122f980427c
children cf5e6afbeb7c
files whileTestGears.agda
diffstat 1 files changed, 27 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Thu Jan 02 15:33:49 2020 +0900
+++ b/whileTestGears.agda	Thu Jan 02 20:22:24 2020 +0900
@@ -18,7 +18,7 @@
   field
     varn : ℕ
     vari : ℕ
-open Env 
+open Env
 
 whileTest : {l : Level} {t : Set l}  → (c10 : ℕ) → (Code : Env → t) → t
 whileTest c10 next = next (record {varn = c10 ; vari = 0 } )
@@ -30,7 +30,7 @@
 whileLoop env next | true =
     whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 
-test1 : Env 
+test1 : Env
 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
 
 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
@@ -42,7 +42,7 @@
 whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
 whileTest' {_} {_}  {c10} next = next env proof2
   where
-    env : Env 
+    env : Env
     env = record {vari = 0 ; varn = c10 }
     proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
     proof2 = record {pi1 = refl ; pi2 = refl}
@@ -54,7 +54,7 @@
 {-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
 whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env  → t) → t
 whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
-whileLoop' env proof next | no p = next env 
+whileLoop' env proof next | no p = next env
 whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
     where
       env1 = record env {varn = (varn  env) - 1 ; vari = (vari env) + 1}
@@ -65,13 +65,13 @@
       proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
       proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
           begin
-             n' + (vari env + 1) 
+             n' + (vari env + 1)
           ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-             n' + (1 + vari env ) 
+             n' + (1 + vari env )
           ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1) + vari env 
+             (n' + 1) + vari env
           ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-             (suc n' ) + vari env 
+             (suc n' ) + vari env
           ≡⟨⟩
              varn env + vari env
           ≡⟨ proof  ⟩
@@ -97,7 +97,7 @@
 
 -- all proofs are connected
 proofGears : {c10 :  ℕ } → Set
-proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
 
 -- but we cannot prove the soundness of the last condition
 --
@@ -147,10 +147,10 @@
   s2 : whileTestState
   sf : whileTestState
 
-whileTestStateP : whileTestState → Envc →  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) 
+whileTestStateP : whileTestState → Envc →  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)
 
 whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
@@ -192,7 +192,7 @@
 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
 
 --  all codtions are correctly connected and required condtion is proved in the continuation
---      use required condition as t in (env → t) → t 
+--      use required condition as t in (env → t) → t
 whileTestPCallwP : (c :  ℕ ) → Set
 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c )  ) where
    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
@@ -224,17 +224,23 @@
 whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
 whileTestPSemSound c output refl = whileTestPSem c
 
+
+whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input)
+whileConvPSemSound input = proof λ x → (conv input x) where
+  conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+  conv e record { pi1 = refl ; pi2 = refl } = +zero
+
 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
 loopPP zero input refl = input
 loopPP (suc n) input refl =
-    loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl 
+    loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl
 
 whileLoopPSem : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
   → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
   → (exit : (output : Envc ) → (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) ) 
+... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) )
 
 loopPPSem : (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
   → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
@@ -244,7 +250,7 @@
     lem n env = +-suc (n) (vari env)
     loopPPSemInduct : (n : ℕ) → (current : Envc) → (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 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)
@@ -256,3 +262,7 @@
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
 
+
+
+whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ →  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 (whileTestP c (λ e → e)) refl) top))