Mercurial > hg > Members > ryokka > HoareLogic

changeset 33:7679b9dc4b40

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
env fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 Dec 2019 10:34:35 +0900
parents bf7c7bd69e35
children 9caff4e4a402
files whileTestGears.agda
diffstat 1 files changed, 42 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Tue Dec 10 09:51:12 2019 +0900
+++ b/whileTestGears.agda	Tue Dec 10 10:34:35 2019 +0900
@@ -16,11 +16,11 @@
     vari : ℕ
 open Env
 
-whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t
+whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
 whileTest c10 next = next (record {varn = c10 ; vari = 0} )
 
 {-# TERMINATING #-}
-whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
 whileLoop env next with lt 0 (varn env)
 whileLoop env next | false = next env
 whileLoop env next | true =
@@ -34,7 +34,7 @@
 proof1 = refl
 
 --                                                                              ↓PostCondition
-whileTest' : {l : Level} {t : Set l}  -> {c10 :  ℕ } → (Code : (env : Env)  -> ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t
+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
@@ -47,7 +47,7 @@
 
 
 {-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
-whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) -> (Code : Env -> t) -> t
+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 {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
@@ -74,8 +74,8 @@
           ∎
 
 -- Condition to Invaliant
-conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
-               -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t
+conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+               → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
 conversion1 env {c10} p1 next = next env proof4
    where
       proof4 : varn env + vari env ≡ c10
@@ -94,55 +94,62 @@
 proofGears : {c10 :  ℕ } → Set
 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
-data whileTestState (c10 : ℕ ) : Set where
-  error : whileTestState c10
-  state1 : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10
-  state2 : (env : Env) → (varn env + vari env ≡ c10) → whileTestState c10
-  finstate : (env : Env)  → ((vari env) ≡ c10 ) → whileTestState c10
+data whileTestState (c10 : ℕ ) (env : Env ) : Set where
+  error : whileTestState c10 env
+  state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env
+  state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
+  finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
 
 record Context : Set where
    field 
      c10 : ℕ
      whileDG : Env
-     whileCond : whileTestState c10
+     whileCond : whileTestState c10 whileDG
 
 open Context
 
-whileTestContext : {l : Level} {t : Set l} -> Context → (Code : Context -> t) -> t
-whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0}} )
+whileTestContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
+whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0} ; whileCond = {!!} } )
 
 {-# TERMINATING #-}
-whileLoopContext : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
+whileLoopContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
 whileLoopContext cxt next with lt 0 (varn (whileDG cxt) )
 whileLoopContext cxt next | false = next cxt
 whileLoopContext cxt next | true =
-    whileLoopContext (record cxt { whileDG = record {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} } )  next
+    whileLoopContext (record cxt { whileDG = record {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = {!!} } )  next
+
+open import Relation.Nullary
+open import Relation.Binary
+
 
 {-# TERMINATING #-}
-whileLoopStep : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) (Code : Env -> t) -> t
-whileLoopStep env next exit with lt 0 (varn env)
-whileLoopStep env next exit | false = exit env
-whileLoopStep env next exit | true =
-    next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) 
+whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 0 < varn e → t) (Code : (e : Env) → 0 ≡ varn e  → t) → t
+whileLoopStep env next exit with <-cmp 0 (varn env)
+whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
+whileLoopStep env next exit | tri< gt _ _  =
+    next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) {!!}
+whileLoopStep env next exit | tri> _ _ _  = {!!} -- can't happen
 
-whileTestProof : {l : Level} {t : Set l} -> Context → (Code : Context -> t) -> t
+whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
     out : Env 
     out =  whileTest (c10 cxt) ( λ e → e ) 
-    init : whileTestState (c10 cxt)
-    init = state1 out record { pi1 = refl ; pi2 = refl }
+    init : whileTestState (c10 cxt) out
+    init = state1 record { pi1 = refl ; pi2 = refl }
 
 {-# TERMINATING #-}
-whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t
+whileLoopProof : {l : Level} {t : Set l} → Context → (Code : Context → t) (Code : Context → t) → t
 whileLoopProof cxt next exit = whileLoopStep (whileDG cxt)
-    ( λ env → next record cxt { whileDG = env } ) 
-    ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } )   where
-        exitCond : Env → whileTestState (c10 cxt)
-        exitCond nenv with whileCond cxt
-        ... | state2 e inv = finstate (whileDG cxt) {!!}
-        ... | _ = error
+    ( λ env lt → next record cxt { whileDG = env ; whileCond = {!!} } ) 
+    ( λ env eq → exit record cxt { whileDG = env ; whileCond = exitCond env eq } )   where
+        proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
+        proof5 e inv = {!!}
+        exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
+        exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
+        ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
+        ... | _ | _ = error
 
-whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
+whileConvProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
 whileConvProof cxt next = next record cxt { whileCond = postCond } where
     proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
     proof4 env p1 = let open ≡-Reasoning  in
@@ -155,13 +162,13 @@
           ≡⟨ +-sym {c10 cxt} {0} ⟩
             c10 cxt 
           ∎
-    postCond : whileTestState (c10 cxt)
+    postCond : whileTestState (c10 cxt) (whileDG cxt)
     postCond with whileCond cxt
-    ... | state1 e inv = state2 e (proof4 e inv)
+    ... | state1 cond = state2 (proof4 (whileDG cxt) cond )
     ... | _ = error
 
 {-# TERMINATING #-}
-loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t
+loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t
 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
 
 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })