# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1544926853 -32400
# Node ID 8d546766a9a886227751ca4cfd1e4c5e218ac178
# Parent  a622d1700a1b5129b2f294f8b100a869f49ef2fd
Prim variable version done

diff -r a622d1700a1b -r 8d546766a9a8 utilities.agda
--- a/utilities.agda	Sun Dec 16 08:19:47 2018 +0900
+++ b/utilities.agda	Sun Dec 16 11:20:53 2018 +0900
@@ -152,3 +152,9 @@
 Equal+1 {x} {.x} | yes refl = refl
 Equal+1 {x} {y} | no ¬p = refl
 
+open import Data.Empty 
+
+≡→Equal : { x y : ℕ } → x ≡ y →  Equal x y ≡ true 
+≡→Equal {x} {.x} refl with x ≟ x
+≡→Equal {x} {.x} refl | yes refl = refl
+≡→Equal {x} {.x} refl | no ¬p = ⊥-elim ( ¬p refl )
diff -r a622d1700a1b -r 8d546766a9a8 whileTestPrim.agda
--- a/whileTestPrim.agda	Sun Dec 16 08:19:47 2018 +0900
+++ b/whileTestPrim.agda	Sun Dec 16 11:20:53 2018 +0900
@@ -117,6 +117,12 @@
 stmt1Cond : {c10 : ℕ} → Cond
 stmt1Cond {c10} env = Equal (varn env) c10
 
+init-case : {c10 :  ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true 
+init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
+
+init-type : {c10 :  ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10})
+init-type {c10} env = init-case env
+
 stmt2Cond : {c10 : ℕ} → Cond
 stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
 
@@ -129,15 +135,20 @@
 termCond : {c10 : ℕ} → Cond
 termCond {c10} env = Equal (vari env) c10
 
+lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+  begin
+    (Equal (varn env) c10 ) ∧ true
+  ≡⟨ ∧true ⟩
+    Equal (varn env) c10 
+  ≡⟨ cond ⟩
+    true
+  ∎ )
+
 proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
 proofs c10 =
-      SeqRule {initCond} ( PrimRule {!!} )
-    $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma {c10})
-  where
-     lemma : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
-     lemma env with (stmt1Cond {c10}) env
-     lemma env | false = {!!}
-     lemma env | true = {!!}
+      SeqRule {initCond} ( PrimRule (init-case {c10} ))
+    $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10})
 
 open import Data.Empty
 
@@ -145,17 +156,13 @@
 
 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
 proof1 c10 =
-      SeqRule {λ e → true} ( PrimRule {!!} )
+      SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
     $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
     $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
             WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
             $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
                      $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
   where
-     lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
-     lemma1 {c10} env with (stmt1Cond {c10}) env
-     lemma1 {c10} env | false = {!!}
-     lemma1 {c10} env | true = {!!}
      lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
      lemma21 eq = Equal→≡ (∧-pi1 eq)
      lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
@@ -166,7 +173,7 @@
             varn env + vari env
           ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
             c10 + vari env
-          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} {!!}  ) ⟩
+          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
             c10 + 0
           ≡⟨ +-sym {c10} {0} ⟩
             0 + c10 
@@ -182,7 +189,7 @@
             (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
           ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
             (stmt2Cond env)  ⇒ (Equal c10 c10)
-          ≡⟨ {!!} ⟩
+          ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl )  ⟩
             (stmt2Cond {c10} env)  ⇒  true
           ≡⟨ ⇒t ⟩
             true
@@ -230,7 +237,7 @@
             Equal (varn env + vari env) (suc c10)
           ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
             Equal (suc c10) (suc c10)
-          ≡⟨ {!!} ⟩
+          ≡⟨ ≡→Equal refl ⟩
             true
           ∎
      lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv