# HG changeset patch
# User ryokka
# Date 1576142799 -32400
# Node ID 9caff4e4a402e704ecf533bce337588edd8c6a76
# Parent  7679b9dc4b40cf997c15111e20ad3ac9798e7421
add some proofs

diff -r 7679b9dc4b40 -r 9caff4e4a402 whileTestGears.agda
--- 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 )