### changeset 34:9caff4e4a402

author ryokka Thu, 12 Dec 2019 18:26:39 +0900 7679b9dc4b40 7c739972cd26 whileTestGears.agda 1 files changed, 10 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
```--- a/whileTestGears.agda	Tue Dec 10 10:34:35 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 12 18:26:39 2019 +0900
@@ -2,7 +2,7 @@

open import Function
open import Data.Nat
-open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_)
+open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_)
open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality
@@ -127,8 +127,14 @@
whileLoopStep env next exit with <-cmp 0 (varn env)
whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
whileLoopStep env next exit | tri< gt _ _  =
-    next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) {!!}
-whileLoopStep env next exit | tri> _ _ _  = {!!} -- can't happen
+    next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) (lem env gt)
+      where
+        lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1)
+        lem record { varn = (suc na) ; vari = vari } (s≤s gt) with na ≟ 0
+        lem record { varn = (suc na) ; vari = vari } (s≤s gt) | does₁ because proof₁ = {!!}
+        -- n が 0 の時正しくない
+
+whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen

whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
@@ -143,7 +149,7 @@
( λ env lt → next record cxt { whileDG = env ; whileCond = {!!} } )
( λ env eq → exit record cxt { whileDG = env ; whileCond = exitCond env eq } )   where
proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
-        proof5 e inv = {!!}
+        proof5 record { varn = .0 ; vari = vari } refl refl = refl
exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )```