module whilespecimple where

open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Relation.Binary
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Empty
open import Agda.Builtin.Sigma
open import Data.Product
open import Data.Nat


open import utilities hiding ( _/\_ )
open import whiletest
open import Hoare PrimComm Cond Axiom Tautology _and_ neg
open import whilespec

State : Set
State = Env

open import RelOp 
module RelOpState = RelOp State


SemCond : Cond -> State -> Set
SemCond c p = c p ≡ true

PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
PrimSemComm prim s1 s2 =  Id State (prim s1) s2

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


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


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 )

_/\_ : Cond -> Cond -> Cond
b1 /\ b2 = b1 and b2

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

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


open import HoareSoundness
    Cond 
    PrimComm 
    neg 
    _and_ 
    Tautology 
    State 
    SemCond 
    tautValid 
    respNeg 
    respAnd 
    PrimSemComm 
    Axiom 
    axiomValid

PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
            HTProof bPre cm bPost -> Satisfies bPre cm bPost
PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht


proofOfProgram : (c10 : ℕ) → (input output : Env )
  → initCond input ≡ true
  → (SemComm (program c10) input output)
  → termCond {c10} output ≡ true
proofOfProgram c10 input output ic sem  = PrimSoundness (proof1 c10) input output ic sem