# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1545659425 -32400
# Node ID 5e4abc1919b40f3ca7d42a0c6716235c0e4f85c6
# Parent  fe7d6c90e435bea129ef5288e35a5500c8675c90
fix module relation

diff -r fe7d6c90e435 -r 5e4abc1919b4 Hoare.agda
--- a/Hoare.agda	Mon Dec 24 17:53:22 2018 +0900
+++ b/Hoare.agda	Mon Dec 24 22:50:25 2018 +0900
@@ -5,101 +5,16 @@
 open import Data.Product
 open import Data.Bool
 open import Data.Empty
+open import Data.Sum
 open import Relation.Binary 
 open import Relation.Nullary
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
+open import RelOp 
 open import whileTestPrim
 
 module Hoare where
 
-State : Set
-State = Env
-
-open import RelOp hiding ( Iff ; NotP ; Imply ; Pred )
-module RelOpState = RelOp State
-
--- PrimComm : Set
--- PrimComm = Env → Env
-
--- Cond : Set
--- Cond = (Env → Bool) 
-
-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
-
-_/\_ : Cond -> Cond -> Cond
-b1 /\ b2 = b1 and b2
-
-_\/_ : Cond -> Cond -> Cond
-b1 \/ b2 = neg (neg b1 /\ neg b2)
-
-_==>_ : Cond -> Cond -> Cond
-b1 ==> b2 = neg (b1 \/ b2)
-
-SemCond : Cond -> State -> Set
-SemCond c p = c p ≡ true
-
-tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
-                 (s : State) -> SemCond b1 s -> SemCond b2 s
-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 b s = ( left , right ) where
-    left : not (b s) ≡ true → (b s) ≡ true → ⊥
-    left ne with b s
-    left refl | false = λ ()
-    left () | true
-    right : ((b s) ≡ true → ⊥) → not (b s) ≡ true
-    right ne with b s
-    right ne | false = refl
-    right ne | true = ⊥-elim ( ne refl )
-
-respAnd : (b1 b2 : Cond) -> (s : State) ->
-               Iff (SemCond (b1 /\ b2) s)
-                   ((SemCond b1 s) × (SemCond b2 s))
-respAnd b1 b2 s = ( left , right ) where
-     left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true)  ×  (b2 s ≡ true)
-     left and with b1 s | b2 s
-     left () | false | false 
-     left () | false | true 
-     left () | true | false 
-     left refl | true | true = ( refl , refl )
-     right :  (b1 s ≡ true)  ×  (b2 s ≡ true) →  b1 s ∧ b2 s ≡ true
-     right ( x1 , x2 ) with b1 s | b2 s
-     right (() , ()) | false | false 
-     right (() , _) | false | true 
-     right (_ , ()) | true | false 
-     right (refl , refl) | true | true = refl
-
-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 
-axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
-axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
-axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
-axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
-axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
-
-
-open import Data.Sum
 
 when : {X  Y  Z : Set} -> (X -> Z) -> (Y -> Z) ->
        X ⊎ Y -> Z
diff -r fe7d6c90e435 -r 5e4abc1919b4 RelOp.agda
--- a/RelOp.agda	Mon Dec 24 17:53:22 2018 +0900
+++ b/RelOp.agda	Mon Dec 24 22:50:25 2018 +0900
@@ -9,22 +9,10 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 open import Relation.Nullary
-
+open import utilities
 
 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
 
diff -r fe7d6c90e435 -r 5e4abc1919b4 utilities.agda
--- a/utilities.agda	Mon Dec 24 17:53:22 2018 +0900
+++ b/utilities.agda	Mon Dec 24 22:50:25 2018 +0900
@@ -2,11 +2,20 @@
 
 open import Function
 open import Data.Nat
+open import Data.Product
 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
 
+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
 
 record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where
   field
diff -r fe7d6c90e435 -r 5e4abc1919b4 whileTestPrim.agda
--- a/whileTestPrim.agda	Mon Dec 24 17:53:22 2018 +0900
+++ b/whileTestPrim.agda	Mon Dec 24 22:50:25 2018 +0900
@@ -7,7 +7,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
 
-open import utilities
+open import utilities hiding ( _/\_ )
 
 record Env : Set where
   field
@@ -299,5 +299,78 @@
           ∎
         )
 
+--- necessary definitions for Hoare.agda ( Soundness )
 
+State : Set
+State = Env
 
+open import RelOp 
+module RelOpState = RelOp State
+
+open import Data.Product
+open import Relation.Binary
+
+NotP : {S : Set} -> Pred S -> Pred S
+NotP X s = ¬ X s
+
+_/\_ : Cond -> Cond -> Cond
+b1 /\ b2 = b1 and b2
+
+_\/_ : Cond -> Cond -> Cond
+b1 \/ b2 = neg (neg b1 /\ neg b2)
+
+_==>_ : Cond -> Cond -> Cond
+b1 ==> b2 = neg (b1 \/ b2)
+
+SemCond : Cond -> State -> Set
+SemCond c p = c p ≡ true
+
+tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
+                 (s : State) -> SemCond b1 s -> SemCond b2 s
+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 b s = ( left , right ) where
+    left : not (b s) ≡ true → (b s) ≡ true → ⊥
+    left ne with b s
+    left refl | false = λ ()
+    left () | true
+    right : ((b s) ≡ true → ⊥) → not (b s) ≡ true
+    right ne with b s
+    right ne | false = refl
+    right ne | true = ⊥-elim ( ne refl )
+
+respAnd : (b1 b2 : Cond) -> (s : State) ->
+               Iff (SemCond (b1 /\ b2) s)
+                   ((SemCond b1 s) × (SemCond b2 s))
+respAnd b1 b2 s = ( left , right ) where
+     left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true)  ×  (b2 s ≡ true)
+     left and with b1 s | b2 s
+     left () | false | false 
+     left () | false | true 
+     left () | true | false 
+     left refl | true | true = ( refl , refl )
+     right :  (b1 s ≡ true)  ×  (b2 s ≡ true) →  b1 s ∧ b2 s ≡ true
+     right ( x1 , x2 ) with b1 s | b2 s
+     right (() , ()) | false | false 
+     right (() , _) | false | true 
+     right (_ , ()) | true | false 
+     right (refl , refl) | true | true = refl
+
+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 
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
+