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