# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1545641602 -32400
# Node ID fe7d6c90e435bea129ef5288e35a5500c8675c90
# Parent  5001cda86c3df5b9b488326ad84f52f5cc9bdfbb
Hoare and Relop done

diff -r 5001cda86c3d -r fe7d6c90e435 Hoare.agda
--- a/Hoare.agda	Mon Dec 24 14:56:01 2018 +0900
+++ b/Hoare.agda	Mon Dec 24 17:53:22 2018 +0900
@@ -4,39 +4,51 @@
 open import Data.Nat
 open import Data.Product
 open import Data.Bool
+open import Data.Empty
 open import Relation.Binary 
 open import Relation.Nullary
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
-
-
 open import whileTestPrim
 
---open import SET
-
 module Hoare where
 
---    (Cond : Set)
---    (PrimComm : Set)
---    (neg : Cond -> Cond)
---    (_/\_ : Cond -> Cond -> Cond)
---    (Tautology : Cond -> Cond -> Set)
---    (State : Set)
---    (Pred : State → Set)
-
 State : Set
 State = Env
 
-open import RelOp
+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
 
-_/\_ : Cond -> Cond -> Cond
-b1 /\ b2 = b1 and b2
-
 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
@@ -47,21 +59,44 @@
 
 respNeg : (b : Cond) -> (s : State) ->
                Iff (SemCond (neg b) s) (¬ SemCond b s)
-respNeg 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 = {!!}
+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 =  {!!}
-
+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  = {!!}
+                  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
@@ -71,17 +106,6 @@
 when f g (inj₁ x) = f x
 when f g (inj₂ y) = g y
 
-_\/_ : Cond -> Cond -> Cond
-b1 \/ b2 = neg (neg b1 /\ neg b2)
-
-_==>_ : Cond -> Cond -> Cond
-b1 ==> b2 = neg (b1 \/ b2)
-
--- Hoare Triple
--- data HT : Set where
---   ht : Cond -> Comm -> Cond -> HT
-
-
 -- semantics of commands
 SemComm : Comm -> Rel State (Level.zero)
 SemComm Skip = RelOpState.deltaGlob
@@ -114,7 +138,7 @@
 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
   = axiomValid bPre cm bPost pr s1 s2 q1 q2
 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
-  = substId1 {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
+  = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
           s1 s2 q1 q2
@@ -208,7 +232,7 @@
       lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 ->
              SemCond bInv ss2
       lem1 ℕ.zero ss2 h
-        = substId1 (proj₂ h) (SemCond bInv) q1
+        = substId1 State (proj₂ h) (SemCond bInv) q1
       lem1 (ℕ.suc n) ss2 h
         = let hyp2 : (z : State) -> Rel1 n s1 z ->
                      SemCond bInv z