Mercurial > hg > Members > ryokka > HoareLogic

changeset 57:990d1d892398

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Maybe All Proof. but Non-Terminating
author ryokka
date Sat, 21 Dec 2019 16:35:54 +0900
parents 34601fe34b71
children 7523d5cd670b
files whileTestGears.agda
diffstat 1 files changed, 3 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sat Dec 21 15:47:30 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 16:35:54 2019 +0900
@@ -183,12 +183,7 @@
     conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
     conv e record { pi1 = refl ; pi2 = refl } = +zero
 
+{-# TERMINATING #-}
 Proof : (c :  ℕ ) → whileTestPCallwP c
-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
+Proof zero = whileTestPwP {_} {_} zero (λ env s → refl)
+Proof (suc c) = Proof (suc c)