# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1577062134 -32400
# Node ID 9071e5a77a132d1228a1eb573918c75a62134a2a
# Parent  bef5d4281ac81cf45f2a69fb12ab684404079066
implies

diff -r bef5d4281ac8 -r 9071e5a77a13 whileTestGears.agda
--- a/whileTestGears.agda	Sun Dec 22 15:41:41 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 23 09:48:54 2019 +0900
@@ -176,14 +176,26 @@
          c10 env
       ∎
 
-whileTestPwPSound :  (c : ℕ) → whileTestPwP c ( λ env s → whileTestStateP s1 env )
-whileTestPwPSound c = record { pi1 = refl ; pi2 = refl }
+data _implies_  (A B : Set ) : Set (succ Zero) where
+    proof : ( A → B ) → A implies B
+
+implies2p : {A B : Set } → A implies B  → A → B
+implies2p (proof x) = x
+
+whileTestPwPSound :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
+whileTestPwPSound c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
 
-GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t )  → post (f env ( λ env s → env ))
-GearsIdSound env {post} f = ?
+GearsIdSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set}
+   (f : {l : Level } {t : Set l } → (e0 : Envc ) → pre e0 → ((e : Envc) → post e → t)  → t )
+   → (p : pre e0)
+   → e1 ≡ ( f e0 p ( λ e1 s → e1 ))
+   → (pre e0) implies (post e1)
+GearsIdSound e0 _ {pre} {post} f p refl = proof (λ p → (f e0 p (λ e1 s → {!!} ))) where
+    lemma : post (f e0 p (λ e1 s → e1))
+    lemma = subst (λ k → post k ) {!!} {!!}
 
--- hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → (vari e ≡ 0) /\ (varn e ≡ c))
--- hoge c env = GearsIdSound env (λ e → whileTestPwP c )
+hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → ⊤ implies ((vari e ≡ 0) /\ (varn e ≡ c)))
+hoge c env = {!!} -- GearsIdSound env (λ e → whileTestPwP c )
 
 -- induction にする
 {-# TERMINATING #-}
diff -r bef5d4281ac8 -r 9071e5a77a13 whileTestPrimProof.agda
--- a/whileTestPrimProof.agda	Sun Dec 22 15:41:41 2019 +0900
+++ b/whileTestPrimProof.agda	Mon Dec 23 09:48:54 2019 +0900
@@ -250,6 +250,8 @@
 PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
 PrimSemComm prim s1 s2 =  Id State (prim s1) s2
 
+
+
 axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
                   (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
                   SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2