Mercurial > hg > Members > ryokka > HoareLogic

changeset 56:34601fe34b71

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Sat, 21 Dec 2019 15:47:30 +0900
parents 1be7bb658cf0
children 990d1d892398
files whileTestGears.agda
diffstat 1 files changed, 28 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Fri Dec 20 17:45:56 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 15:47:30 2019 +0900
@@ -143,7 +143,7 @@
    env : Envc
    env = whileTestP c10 ( λ env → env )
 
-whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env 
+whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
     → (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)
@@ -152,8 +152,27 @@
     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 }) {!!}
+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 → ⊥
+    1<0 ()
+    proof5 : (suc zero  ≤ (varn  env))  → (varn env - 1) + (vari env + 1) ≡ c10 env
+    proof5 (s≤s lt) with varn  env
+    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
+    proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
+      begin
+        n' + (vari env + 1)
+      ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+        n' + (1 + vari env )
+      ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+        (n' + 1) + vari env
+      ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+        (suc n' ) + vari env
+      ≡⟨⟩
+        varn env + vari env
+      ≡⟨ s  ⟩
+         c10 env
+      ∎
 
 {-# TERMINATING #-}
 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
@@ -165,11 +184,11 @@
     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
+Proof zero = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → refl))
+  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
-
-
-
-
-
+Proof (suc c) = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → {!!})) -- Proof c したいが with <-cmp 0 c とか with 0 ≤ c とかするとAgda の check が終わらない
+  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