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 _⊑⇓_ _⊑⇑_ _⊑_ _≈_
_⊑⇓_ : ∀ {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)
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 }
}
⊑-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 _⊑_
≈-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 _≈_