Mercurial > hg > Members > ryokka > HoareLogic

changeset 29:816b44e5e674

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fincase
author ryokka
date Mon, 09 Dec 2019 19:17:01 +0900
parents 835b2d53815e
children dd66b94bf365
files whileTestGears.agda
diffstat 1 files changed, 7 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Mon Dec 09 19:08:08 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 09 19:17:01 2019 +0900
@@ -101,23 +101,25 @@
   
   state1 : whileTestState
   state2 : whileTestState
-
+  finstate : whileTestState
 
 record whileTestCondition  (c10 : ℕ)  (t : whileTestState)  : Set where
   coinductive
   field
+    fincase : (env : Env) → (t ≡ finstate)  → (vari env ≡ c10)
     case1 : (env : Env)  → (t ≡ state1) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestCondition c10 state2
     case2 : (env : Env) → (t ≡ state2)  → (varn env + vari env ≡ c10) → whileTestCondition c10 state2
 
 open whileTestCondition
 
 test2 : (c10 : ℕ) → whileTestCondition c10 state1 → whileTestCondition c10 state2 
-test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → proof3 env env1 cond1 ))
+test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → {!!}))
   where    
     whileLoopCond : (e env1 : Env) → varn env1 + vari env1 ≡ c10 → varn e + vari e ≡ c10 → whileTestCondition c10 state2
     whileLoopCond = {!!}
-    proof3 : (env env1 : Env) → whileTestCondition c10 state1 → whileTestCondition c10 state2
-    case1 (proof3 env env1 cond1) e ()
-    case2 (proof3 env env1 cond1) e refl cond2 = {!!}
+    proof3 : (env env1 : Env) → whileTestCondition c10 finstate
+    fincase (proof3 env env1) = {!!}
+    case1 (proof3 env env1 ) e ()
+    case2 (proof3 env env1 ) e ()
 
 -- conversion1 e {c10} (case2  (case1 cond1 ? ? ?)) {!!}