Mercurial > hg > Members > ryokka > HoareLogic

changeset 55:1be7bb658cf0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proof whileLoopPwP tri= case, conv
author ryokka
date Fri, 20 Dec 2019 17:45:56 +0900
parents 3adf50622101
children 34601fe34b71
files whileTestGears.agda
diffstat 1 files changed, 11 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Fri Dec 20 16:13:52 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 20 17:45:56 2019 +0900
@@ -147,7 +147,11 @@
     → (next : (env : Envc ) → whileTestStateP s2 env  → t)
     → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
 whileLoopPwP env s next exit with <-cmp 0 (varn env)
-whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env {!!}
+whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
+  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 }) {!!}
 
@@ -158,10 +162,14 @@
 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 = {!!}
+    conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+Proof : (c :  ℕ ) → whileTestPCallwP c
+Proof c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → {!!} ) ) 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
 
 
 
 
 
-