{-# OPTIONS --universe-polymorphism #-}

open import Level
open import Data.Nat
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 utilities 

module HoareSoundness
    (Cond : Set)
    (PrimComm : Set)
    (neg : Cond -> Cond)
    (_/\_ : Cond -> Cond -> Cond)
    (Tautology : Cond -> Cond -> Set)
    (State : Set)
    (SemCond : Cond -> State -> Set)
    (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
                 (s : State) -> SemCond b1 s -> SemCond b2 s)
    (respNeg : (b : Cond) -> (s : State) ->
               Iff (SemCond (neg b) s) (¬ SemCond b s))
    (respAnd : (b1 b2 : Cond) -> (s : State) ->
               Iff (SemCond (b1 /\ b2) s)
                   ((SemCond b1 s) × (SemCond b2 s)))
    (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l)
    (Axiom : Cond -> PrimComm -> Cond -> Set)
    (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) where

open import Hoare PrimComm Cond Axiom Tautology _/\_ neg

open import RelOp 
module RelOpState = RelOp State

NotP : {S : Set} -> Pred S -> Pred S
NotP X s = ¬ X s

_\/_ : Cond -> Cond -> Cond
b1 \/ b2 = neg (neg b1 /\ neg b2)

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

-- semantics of commands
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 (If b c1 c2)
  = RelOpState.union
      (RelOpState.comp (RelOpState.delta (SemCond b))
                       (SemComm c1))
      (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
                       (SemComm c2))
SemComm (While b c)
  = RelOpState.unionInf
      (λ (n : ℕ) ->
        RelOpState.comp (RelOpState.repeat
                           n
                           (RelOpState.comp
                             (RelOpState.delta (SemCond b))
                             (SemComm c)))
                         (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

Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
            HTProof bPre cm bPost -> Satisfies bPre cm bPost
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 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
  = let hyp : Satisfies bPre' cm bPost'
        hyp = Soundness pr
        r1 : SemCond bPre' s1
        r1 = tautValid bPre bPre' tautPre s1 q1
        r2 : SemCond bPost' s2
        r2 = hyp s1 s2 r1 q2
    in tautValid bPost' bPost tautPost s2 r2
Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
           s1 s2 q1 q2
  = let hyp1 : Satisfies bPre cm1 bMid
        hyp1 = Soundness pr1
        hyp2 : Satisfies bMid cm2 bPost
        hyp2 = Soundness pr2
        sMid : State
        sMid = proj₁ q2
        r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2
        r1 = proj₂ q2
        r2 : SemComm cm1 s1 sMid
        r2 = proj₁ r1
        r3 : SemComm cm2 sMid s2
        r3 = proj₂ r1
        r4 : SemCond bMid sMid
        r4 = hyp1 s1 sMid q1 r2
    in hyp2 sMid s2 r4 r3
Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
          s1 s2 q1 q2
  = let hypThen : Satisfies (bPre /\ b) cmThen bPost
        hypThen = Soundness pThen
        hypElse : Satisfies (bPre /\ neg b) cmElse bPost
        hypElse = Soundness pElse
        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
                                     (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)))
                  (SemComm cmElse) s1 s2 ->
                SemCond bPost s2
        rElse = λ h ->
                  let t10 : (NotP (SemCond b) s1) ×
                            (SemComm cmElse s1 s2)
                      t10 = proj₂ (RelOpState.deltaRestPre
                                    (NotP (SemCond b)) (SemComm cmElse) s1 s2)
                            h
                      t6 : SemCond (neg b) s1
                      t6 = proj₂ (respNeg b s1) (proj₁ t10)
                      t7 : SemComm cmElse s1 s2
                      t7 = proj₂ t10
                      t8 : SemCond (bPre /\ neg b) s1
                      t8 = proj₂ (respAnd bPre (neg b) s1)
                           (q1 , t6)
                  in hypElse s1 s2 t8 t7
    in when rThen rElse q2
Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
  = proj₂ (respAnd bInv (neg b) s2) t20
    where
      hyp : Satisfies (bInv /\ b) cm' bInv
      hyp = Soundness pr
      n : ℕ
      n = proj₁ q2
      Rel1 : ℕ -> Rel State (Level.zero)
      Rel1 = λ m ->
               RelOpState.repeat
                 m
                 (RelOpState.comp (RelOpState.delta (SemCond b))
                                  (SemComm cm'))
      t1 : RelOpState.comp
             (Rel1 n)
             (RelOpState.delta (NotP (SemCond b))) s1 s2
      t1 = proj₂ q2
      t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
      t15 = proj₂ (RelOpState.deltaRestPost
                    (NotP (SemCond b)) (Rel1 n) s1 s2)
              t1
      t16 : Rel1 n s1 s2
      t16 = proj₁ t15
      t17 : NotP (SemCond b) s2
      t17 = proj₂ t15
      lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 ->
             SemCond bInv ss2
      lem1 ℕ.zero ss2 h
        = substId1 State (proj₂ h) (SemCond bInv) q1
      lem1 (ℕ.suc n) ss2 h
        = let hyp2 : (z : State) -> Rel1 n s1 z ->
                     SemCond bInv z
              hyp2 = lem1 n
              s20 : State
              s20 = proj₁ h
              t21 : Rel1 n s1 s20
              t21 = proj₁ (proj₂ h)
              t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
              t22 = proj₂ (RelOpState.deltaRestPre
                            (SemCond b) (SemComm cm') s20 ss2)
                    (proj₂ (proj₂ h))
              t23 : SemCond (bInv /\ b) s20
              t23 = proj₂ (respAnd bInv b s20)
                    (hyp2 s20 t21 , proj₁ t22)
          in hyp s20 ss2 t23 (proj₂ t22)
      t20 : SemCond bInv s2 × SemCond (neg b) s2
      t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17