Mercurial > hg > Members > ryokka > HoareLogic

changeset 81:0122f980427c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Jan 2020 15:33:49 +0900
parents 148feaa1e346
children 33a6fd61c3e6
files whileTestGears.agda
diffstat 1 files changed, 45 insertions(+), 111 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Wed Jan 01 21:50:38 2020 +0900
+++ b/whileTestGears.agda	Thu Jan 02 15:33:49 2020 +0900
@@ -12,6 +12,8 @@
 open import utilities
 open  _/\_
 
+-- original codeGear (with non terminatinng )
+
 record Env : Set (succ Zero) where
   field
     varn : ℕ
@@ -31,10 +33,11 @@
 test1 : Env 
 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
 
-
 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
+-- codeGear with pre-condtion and post-condition
+--
 --                                                                              ↓PostCondition
 whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
 whileTest' {_} {_}  {c10} next = next env proof2
@@ -92,18 +95,19 @@
             c10
           ∎
 
-
+-- 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 )))) 
 
+-- but we cannot prove the soundness of the last condition
+--
 -- proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
 -- proofGearsMeta {c10} = {!!} -- net yet done
 
 --
---      openended Env c  <=>  Context
+-- codeGear with loop step and closed environment
 --
 
-open import Relation.Nullary hiding (proof)
 open import Relation.Binary
 
 record Envc : Set (succ Zero) where
@@ -122,11 +126,12 @@
 whileLoopP env next exit | tri< a ¬b ¬c =
      next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
 
+-- equivalent of whileLoopP but it looks like an induction on varn
 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
 whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env
 whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari })
 
-
+-- normal loop without termination
 {-# TERMINATING #-}
 loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
@@ -134,6 +139,9 @@
 whileTestPCall : (c10 :  ℕ ) → Envc
 whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  env))
 
+--
+-- codeGears with states of condition
+--
 data whileTestState  : Set where
   s1 : whileTestState
   s2 : whileTestState
@@ -157,7 +165,6 @@
   where
     lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
     lem p1 p2 rewrite p1 = p2
-
 whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
   where
     1<0 : 1 ≤ zero → ⊥
@@ -180,6 +187,22 @@
          c10 env
       ∎
 
+{-# TERMINATING #-}
+loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
+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 
+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
+   conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+--
+-- 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 → B ) → A implies B
 
@@ -201,124 +224,35 @@
 whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
 whileTestPSemSound c output refl = whileTestPSem c
 
+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 
+
 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 <-cmp 0 (varn env)
-whileLoopPSem env s next exit | tri≈ ¬a b ¬c rewrite (sym b) = exit env (proof (λ z → z))
-whileLoopPSem env s next exit | tri< a ¬b ¬c  = next env (proof (λ z → z))
-
-
-
-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@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z))
-whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next exit =
-  next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari)
-
-
-{--
- (((⊤ implies varn ≡ 0 ∧ vari ≡ c10 ) implies (varn + vari ≡ c10)) implies vari ≡ c10)
-
+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) ) 
 
---}
-loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
-loopPP zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
-loopPP (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP input (λ x → loopPP n (record x { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl) λ x → x -- ?
-
-loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
-
-loopPP' zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
-loopPP' (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = loopPP' n (record { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl -- ?
-
-loopPPSem : (input output : Envc ) →  output ≡ loopPP' (varn input)  input refl
+loopPPSem : (input output : Envc ) →  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 : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡  Envc.c10 output
-    -- lem output eq with <-cmp 0 (Envc.varn input)
-    -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!}
-    -- lem output refl | tri≈ ¬a refl ¬c = s2p
     lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
     lem n env = +-suc (n) (vari env)
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP' n current eq)
+    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) -- loopeq には output ≡ loopPP zero current (zero = varn current)
-
-    -- n を減らして loop を回しつつ証明したい
-    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)
-
--- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq 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)
+            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
 
 whileLoopPSemSound : {l : Level} → (input output : Envc )
    → whileTestStateP s2 input
-   →  output ≡ loopPP' (varn input) input refl
+   →  output ≡ loopPP (varn input) input refl
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
 
-
--- induction にする
-{-# TERMINATING #-}
-loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
-loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
-
---  wP を Env のRel にする  Env → Env → Set にしちゃう
-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
-   conv e record { pi1 = refl ; pi2 = refl } = +zero
-
-
-conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-conv1 e record { pi1 = refl ; pi2 = refl } = +zero
-
--- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
-
-
--- data GComm : Set (succ Zero) where
---   Skip  : GComm
---   Abort : GComm
---   PComm : Set → GComm
---   -- Seq   : GComm → GComm → GComm
---   -- If   : whileTestState → GComm → GComm → GComm
---   while : whileTestState → GComm → GComm
-
--- gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
--- gearsSem pre post = {!!}
-
--- unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
--- unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
-
--- comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
--- comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
-
--- -- repeat : ℕ -> rel set zero -> rel set zero
--- -- repeat ℕ.zero r = λ x x₁ → ⊤
--- -- repeat (ℕ.suc m) r = comp (repeat m r) r
-
--- GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
--- GSemComm Skip = λ x x₁ → ⊤
--- GSemComm Abort = λ x x₁ → ⊥
--- GSemComm (PComm x) = λ x₁ x₂ → x
--- -- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
--- -- GSemComm (If x con con₁) = {!!}
--- GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) →  {!!}) {!!} {!!}
-
-ProofConnect : {l : Level} {t : Set l}
-  → (pr1 : Envc → Set → Set)
-  → (Envc → Set → (Envc → Set → t))
-  → (Envc → Set → Set)
-ProofConnect prev f env post =  {!!} -- with f env ({!!}) {!!} 
-
-Proof2 : (env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env
-Proof2 _ refl = refl 
-
-
--- Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → ((env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env) → vari env ≡ c10 env
-Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → loopPwP env s ( λ env s → vari env ≡ c10 env ) 
-Proof1 env s = {!!} 
-
-Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof c = {!!}