Mercurial > hg > Members > ryokka > HoareLogic

changeset 75:d45e98211d7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author ryokka
date Thu, 26 Dec 2019 18:34:27 +0900
parents 6f26de2fb7fe
children cf00bc7af369
files whileTestGears.agda
diffstat 1 files changed, 7 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Thu Dec 26 18:16:35 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 18:34:27 2019 +0900
@@ -226,15 +226,14 @@
 
 loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
   → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
-loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input refl s2p (proof (λ x → {!!}))
+loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
   where
-    -- lem1 :  (ncurrent : Envc) → suc (varn ncurrent) + vari ncurrent ≡ c10 ncurrent → varn ncurrent + suc (vari ncurrent) ≡ c10 ncurrent
-    -- lem1 current eq = {!!}
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n → (whileTestStateP s2 current ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
-    loopPPSemInduct zero current refl refl imp with loopPP (varn current) current refl -- = proof λ x → {!!}
-    loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl refl imp | record { c10 = c10 ; varn = varn ; vari = vari } = proof {!!}
-    loopPPSemInduct (suc n) current refl s2p imp with <-cmp 0 (suc n) | whileLoopPSem current s2p (λ output x → proof {!!}) λ output x → proof λ x₁ → {!!}
-    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl s2p imp | tri< a ¬b ¬c | proof x = {!!}
+    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n →  output ≡ loopPP n  current {!!}
+      → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+    loopPPSemInduct zero current refl eq refl with loopPP (varn current) current refl -- = proof λ x → {!!}
+    loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl eq refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof (λ x → {!!})
+    loopPPSemInduct (suc n) current refl eq s2p with <-cmp 0 (suc n) | whileLoopPSem current s2p (λ output x → proof {!!}) λ output x → proof λ x₁ → {!!}
+    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | proof x = {!!}