--- a/Hoare.agda	Mon Dec 24 10:08:46 2018 +0900
+++ b/Hoare.agda	Mon Dec 24 14:56:01 2018 +0900
@@ -7,6 +7,8 @@
 open import Relation.Binary 
 open import Relation.Nullary
 open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality
+
 
 open import whileTestPrim
 
@@ -22,49 +24,39 @@
 --    (State : Set)
 --    (Pred : State → Set)
 
+State : Set
 State = Env
 
-Pred : {!!}
-Pred = {!!}
+open import RelOp
+module RelOpState = RelOp State
 
-SemCond :  Cond -> Pred State
-SemCond = {!!}
-
--- open import RelOp
--- module RelOpState_= Rel State
 
-data RELA ( S : Set ) ( l : Level ) :  Set l where
-   RelOpState_deltaGlob :  RELA S l 
-   RelOpState_delta : (Cond -> {!!}) → RELA S l 
-   RelOpState_emptyRel : RELA S l 
-   RelOpState_comp : {!!} → {!!} → RELA S l 
-   RelOpState_union :  RELA S l   → RELA S l → RELA S l 
-   RelOpState_unionInf :  ( ℕ → RELA S l  ) → RELA S l
-   RelOpState_repeat :  ℕ → RELA S l → (Comm -> RELA S l ) →  RELA S l 
-   RelOpState_deltaRestPre :  RELA S l 
-   RelOpState_deltaRestPost : RELA S l 
+SemCond : Cond -> State -> Set
+SemCond c p = c p ≡ true
 
-Iff :  {!!}
-Iff = {!!}
-
-_/\_ : {!!}
-_/\_ = {!!}
+_/\_ : Cond -> Cond -> Cond
+b1 /\ b2 = b1 and b2
 
 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
                  (s : State) -> SemCond b1 s -> SemCond b2 s
-tautValid = {!!}
+tautValid b1 b2 taut s cond with b1 s | b2 s | taut s
+tautValid b1 b2 taut s () | false | false | refl
+tautValid b1 b2 taut s _ | false | true | refl = refl
+tautValid b1 b2 taut s _ | true | false | ()
+tautValid b1 b2 taut s _ | true | true | refl = refl
 
 respNeg : (b : Cond) -> (s : State) ->
                Iff (SemCond (neg b) s) (¬ SemCond b s)
-respNeg = {!!}
+respNeg b s = {!!}
 
 respAnd : (b1 b2 : Cond) -> (s : State) ->
                Iff (SemCond (b1 /\ b2) s)
                    ((SemCond b1 s) × (SemCond b2 s))
 respAnd = {!!}
 
-PrimSemComm : {!!} -- ∀ {l} {S : Set } -> PrimComm -> (x y : State ) → RELA S l x y
-PrimSemComm = {!!}
+PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
+PrimSemComm prim =  {!!}
+
 
 axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
                   (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
@@ -72,15 +64,12 @@
 axiomValid  = {!!}
 
 
-NotP : (Cond -> {!!} ) → (Cond -> {!!} ) 
-NotP = {!!}
+open import Data.Sum
 
-substId1 : {!!}
-substId1 = {!!}
-
-when : {!!}
-when = {!!}
-
+when : {X  Y  Z : Set} -> (X -> Z) -> (Y -> Z) ->
+       X ⊎ Y -> Z
+when f g (inj₁ x) = f x
+when f g (inj₂ y) = g y
 
 _\/_ : Cond -> Cond -> Cond
 b1 \/ b2 = neg (neg b1 /\ neg b2)
@@ -94,31 +83,31 @@
 
 
 -- semantics of commands
-SemComm : Comm -> RELA State (Level.zero)
-SemComm Skip = RelOpState_deltaGlob
-SemComm Abort = RelOpState_emptyRel
+SemComm : Comm -> Rel State (Level.zero)
+SemComm Skip = RelOpState.deltaGlob
+SemComm Abort = RelOpState.emptyRel
 SemComm (PComm pc) = PrimSemComm pc
-SemComm (Seq c1 c2) = RelOpState_comp (SemComm c1) (SemComm c2)
+SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
 SemComm (If b c1 c2)
-  = RelOpState_union
-      (RelOpState_comp (RelOpState_delta (SemCond b))
+  = RelOpState.union
+      (RelOpState.comp (RelOpState.delta (SemCond b))
                        (SemComm c1))
-      (RelOpState_comp (RelOpState_delta (NotP (SemCond b)))
+      (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
                        (SemComm c2))
 SemComm (While b c)
-  = RelOpState_unionInf
+  = RelOpState.unionInf
       (λ (n : ℕ) ->
-        RelOpState_comp (RelOpState_repeat
+        RelOpState.comp (RelOpState.repeat
                            n
-                           (RelOpState_comp
-                             (RelOpState_delta (SemCond b))
+                           (RelOpState.comp
+                             (RelOpState.delta (SemCond b))
                              (SemComm c)))
-                         (RelOpState_delta (NotP (SemCond b))))
+                         (RelOpState.delta (NotP (SemCond b))))
 
 Satisfies : Cond -> Comm -> Cond -> Set
 Satisfies bPre cm bPost
   = (s1 : State) -> (s2 : State) ->
-      SemCond bPre s1 -> {!!} -- SemComm cm s1 s2 -> SemCond bPost s2
+      SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
 
 Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
             HTProof bPre cm bPost -> Satisfies bPre cm bPost
@@ -159,27 +148,27 @@
         hypThen = Soundness pThen
         hypElse : Satisfies (bPre /\ neg b) cmElse bPost
         hypElse = Soundness pElse
-        rThen : RelOpState_comp
-                  (RelOpState_delta (SemCond b))
+        rThen : RelOpState.comp
+                  (RelOpState.delta (SemCond b))
                   (SemComm cmThen) s1 s2 ->
                 SemCond bPost s2
         rThen = λ h ->
                   let t1 : SemCond b s1 × SemComm cmThen s1 s2
-                      t1 = (proj₂ (RelOpState_deltaRestPre
+                      t1 = (proj₂ (RelOpState.deltaRestPre
                                      (SemCond b)
                                      (SemComm cmThen) s1 s2)) h
                       t2 : SemCond (bPre /\ b) s1
                       t2 = (proj₂ (respAnd bPre b s1))
                            (q1 , proj₁ t1)
                   in hypThen s1 s2 t2 (proj₂ t1)
-        rElse : RelOpState_comp
-                  (RelOpState_delta (NotP (SemCond b)))
+        rElse : RelOpState.comp
+                  (RelOpState.delta (NotP (SemCond b)))
                   (SemComm cmElse) s1 s2 ->
                 SemCond bPost s2
         rElse = λ h ->
                   let t10 : (NotP (SemCond b) s1) ×
                             (SemComm cmElse s1 s2)
-                      t10 = proj₂ (RelOpState_deltaRestPre
+                      t10 = proj₂ (RelOpState.deltaRestPre
                                     (NotP (SemCond b)) (SemComm cmElse) s1 s2)
                             h
                       t6 : SemCond (neg b) s1
@@ -200,16 +189,16 @@
       n = proj₁ q2
       Rel1 : ℕ -> Rel State (Level.zero)
       Rel1 = λ m ->
-               RelOpState_repeat
+               RelOpState.repeat
                  m
-                 (RelOpState_comp (RelOpState_delta (SemCond b))
+                 (RelOpState.comp (RelOpState.delta (SemCond b))
                                   (SemComm cm'))
-      t1 : RelOpState_comp
+      t1 : RelOpState.comp
              (Rel1 n)
-             (RelOpState_delta (NotP (SemCond b))) s1 s2
+             (RelOpState.delta (NotP (SemCond b))) s1 s2
       t1 = proj₂ q2
       t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
-      t15 = proj₂ (RelOpState_deltaRestPost
+      t15 = proj₂ (RelOpState.deltaRestPost
                     (NotP (SemCond b)) (Rel1 n) s1 s2)
               t1
       t16 : Rel1 n s1 s2
@@ -229,7 +218,7 @@
               t21 : Rel1 n s1 s20
               t21 = proj₁ (proj₂ h)
               t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
-              t22 = proj₂ (RelOpState_deltaRestPre
+              t22 = proj₂ (RelOpState.deltaRestPre
                             (SemCond b) (SemComm cm') s20 ss2)
                     (proj₂ (proj₂ h))
               t23 : SemCond (bInv /\ b) s20

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/RelOp.agda	Mon Dec 24 14:56:01 2018 +0900
@@ -0,0 +1,94 @@
+{-# OPTIONS --universe-polymorphism #-}
+
+open import Level
+open import Data.Empty
+open import Data.Product
+open import Data.Nat
+open import Data.Sum
+open import Data.Unit
+open import Relation.Binary
+open import Relation.Binary.Core
+open import Relation.Nullary
+
+
+module RelOp (S : Set) where
+
+Pred : Set -> Set₁
+Pred X = X -> Set
+
+Imply : Set -> Set -> Set
+Imply X Y = X -> Y
+
+Iff : Set -> Set -> Set
+Iff X Y = Imply X Y × Imply Y X
+
+NotP : {S : Set} -> Pred S -> Pred S
+NotP X s = ¬ X s
+
+data Id {l} {X : Set} : Rel X l where
+  ref : {x : X} -> Id x x
+
+-- substId1 | x == y & P(x) => P(y)
+substId1 :  ∀ {l} -> {X : Set} -> {x y : X} ->
+           Id {l} x y -> (P : Pred X) -> P x -> P y
+substId1 ref P q = q
+
+-- substId2 | x == y & P(y) => P(x)
+substId2 :  ∀ {l} -> {X : Set} -> {x y : X} ->
+           Id {l} x  y -> (P : Pred X) -> P y -> P x
+substId2 ref P q = q
+
+-- for X ⊆ S (formally, X : Pred S)
+-- delta X = { (a, a) | a ∈ X }
+delta : ∀ {l} -> Pred S -> Rel S l
+delta X a b = X a × Id a b 
+
+-- deltaGlob = delta S
+deltaGlob : ∀ {l} -> Rel S l
+deltaGlob = delta (λ (s : S) → ⊤)
+
+-- emptyRel = \varnothing
+emptyRel : Rel S Level.zero
+emptyRel a b = ⊥
+
+-- comp R1 R2 = R2 ∘ R1 (= R1; R2)
+comp : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
+comp R1 R2 a b = ∃ (λ (a' : S) → R1 a a' × R2 a' b)
+
+-- union R1 R2 = R1 ∪ R2
+union : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
+union R1 R2 a b = R1 a b ⊎ R2 a b
+
+-- repeat n R = R^n
+repeat : ∀ {l} -> ℕ -> Rel S l -> Rel S l
+repeat ℕ.zero R = deltaGlob
+repeat (ℕ.suc m) R = comp (repeat m R) R
+
+-- unionInf f = ⋃_{n ∈ ω} f(n)
+unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l
+unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
+
+-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
+restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l
+restPre X R a b = X a × R a b
+
+-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X }
+restPost : ∀ {l} -> Pred S -> Rel S l -> Rel S l
+restPost X R a b = R a b × X b
+
+deltaRestPre : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
+               Iff (restPre X R a b) (comp (delta X) R a b)
+deltaRestPre X R a b
+  = (λ (h : restPre X R a b) → a , (proj₁ h , ref) , proj₂ h) ,
+     λ (h : comp (delta X) R a b) → proj₁ (proj₁ (proj₂ h)) ,
+       substId2
+         (proj₂ (proj₁ (proj₂ h)))
+         (λ z → R z b) (proj₂ (proj₂ h))
+
+deltaRestPost : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
+                Iff (restPost X R a b) (comp R (delta X) a b)
+deltaRestPost X R a b
+  = (λ (h : restPost X R a b) → b , proj₁ h , proj₂ h , ref) ,
+     λ (h : comp R (delta X) a b) →
+       substId1 (proj₂ (proj₂ (proj₂ h))) (R a) (proj₁ (proj₂ h)) ,
+       substId1 (proj₂ (proj₂ (proj₂ h))) X (proj₁ (proj₂ (proj₂ h)))