------------------------------------------------------------------------
-- 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 _≈_