------------------------------------------------------------------------
-- Semantic equivalence
------------------------------------------------------------------------

module Equivalence where

open import Syntax
open import Semantics.BigStep

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Function
open import Data.Product

infix 3 _⊑⇓_ _⊑⇑_ _⊑_ _≈_

-- x ⊑ y iff every possible result for x is also a possible result
-- for y.

_⊑⇓_ :  {t}  Expr t  Expr t  Set
x ⊑⇓ y =  {i v}  x ⇓[ i ] v  y ⇓[ i ] v

_⊑⇑_ :  {t}  Expr t  Expr t  Set
x ⊑⇑ y =  {i}  x ⇑[ i ]  y ⇑[ i ]

record _⊑_ {t : Totality} (x y : Expr t) : Set where
  field
     : x ⊑⇓ y
     : x ⊑⇑ y

_⋢_ :  {t} (x y : Expr t)  Set
x  y = ¬ (x  y)

-- Semantic equivalence.
--
-- Is this a good notion of equivalence? Maybe one should also ensure
-- that the number of raised interrupts is the same on both sides.
-- (This would most likely make fewer things equivalent.)

record _≈_ {t : Totality} (x y : Expr t) : Set where
  field
     : y  x
     : x  y

  open _⊑_  public renaming (⇓ to ⊒⇓; ⇑ to ⊒⇑)
  open _⊑_  public renaming (⇓ to ⊑⇓; ⇑ to ⊑⇑)

is-≈ :  {t} {x y : Expr t} 
       x ⊑⇓ y  y ⊑⇓ x  x ⊑⇑ y  y ⊑⇑ x  x  y
is-≈ x⊑⇓y y⊑⇓x x⊑⇑y y⊑⇑x = record
  {  = record {  = x⊑⇓y;  = x⊑⇑y }
  ;  = record {  = y⊑⇓x;  = y⊑⇑x }
  }

-- _⊑_ is a preorder.

⊑-preorder : Totality  Preorder
⊑-preorder t = record
  { carrier    = Expr t
  ; _≈_        = _≡_
  ; _∼_        = _⊑_
  ; isPreorder = record
    { isEquivalence = ≡-isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    ; ≈-resp-∼      = ≡-resp _⊑_
    }
  }
  where
  reflexive : _≡_  _⊑_
  reflexive ≡-refl = record {  = id;  = id }

  trans : Transitive _⊑_
  trans x⊑y y⊑z = record {  =  y⊑z   x⊑y
                         ;  =  y⊑z   x⊑y }
    where open _⊑_

-- _≈_ is an equivalence relation.

≈-setoid : Totality  Setoid
≈-setoid t = record
  { carrier       = Expr t
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = record {  = P.refl;  = P.refl }
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  module P = Preorder (⊑-preorder t)

  sym : Symmetric _≈_
  sym x≈y = record {  =  ;  =  }
    where open _≈_ x≈y

  trans : Transitive _≈_
  trans x≈y y≈z = record {  = P.trans ( x≈y) ( y≈z)
                         ;  = P.trans ( y≈z) ( x≈y) }
    where open _≈_