Mercurial > hg > Members > ryokka > HoareLogic

changeset 60:ad83c2d5e869

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
agda2 can't stop case
author ryokka
date Sat, 21 Dec 2019 18:28:46 +0900
parents 5c2cdcee9971
children 62dcb0ae2c94
files whileTestGears.agda
diffstat 1 files changed, 20 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sat Dec 21 17:49:15 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 18:28:46 2019 +0900
@@ -189,7 +189,26 @@
 
 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
 
-{-# TERMINATING #-}
+ProofConnect : {l : Level} {t : Set l} → (prev : Envc → Set → Set) → (Envc → Set → (Envc → Set → t)) → (Envc → Set → Set)
+ProofConnect prev f env post with f env ({!!}) {!!} 
+... | tt = {!!}
+
+Proof2 : (env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env
+Proof2 _ refl = refl 
+
+
+{--
+  Proof1 env s with Proof2 ? ?
+  ... | tt = ?
+のとき agda2 が停まらなくなる
+--}
+
+Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → loopPwP env s ( λ env s → vari env ≡ c10 env ) 
+Proof1 env s = {!!} -- with Proof2 ? ? <- agda2 don't stop
+  where
+    lemm : whileLoopPwP env s (λ env s → {!!} ) (λ env s → {!!} )
+    lemm = {!!} -- with Proof2 ? ?
+
 Proof : (c :  ℕ ) → whileTestPCallwP c
 Proof zero = whileTestPwP {_} {_} zero ( λ env s → loopPwP env (conv env s) ( λ env s → refl)  )
   where