module Equivalence where

open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)

record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
    field
        ≈-refl : {a : A} → a ≈ a
        ≈-sym : {a b : A} → a ≈ b → b ≈ a
        ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c

module IsEquivalenceInstances where
    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where

        infix 4 _≈_

        _≈_ : A × B → A × B → Set a
        (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)

        ProdEquivalence : IsEquivalence (A × B) _≈_
        ProdEquivalence = record
            { ≈-refl = λ {p} →
                ( IsEquivalence.≈-refl eA
                , IsEquivalence.≈-refl eB
                )
            ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) →
                ( IsEquivalence.≈-sym eA a₁≈a₂
                , IsEquivalence.≈-sym eB b₁≈b₂
                )
            ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
                ( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃
                , IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃
                )
            }

    module ForMap {a b} (A : Set a) (B : Set b)
        (≡-dec-A : Decidable (_≡_ {a} {A}))
        (_≈₂_ : B → B → Set b)
        (eB : IsEquivalence B _≈₂_) where

        open import Lattice.Map A B ≡-dec-A using (Map; lift; subset)
        open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map

        open IsEquivalence eB renaming
            ( ≈-refl to ≈₂-refl
            ; ≈-sym to ≈₂-sym
            ; ≈-trans to ≈₂-trans
            )

        _≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
        _≈_ = lift _≈₂_

        _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
        _⊆_ = subset _≈₂_

        private
            ⊆-refl : (m : Map) →  m ⊆ m
            ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))

            ⊆-trans : (m₁ m₂ m₃ : Map) →  m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃
            ⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
                let
                    (v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
                    (v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
                in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))

        LiftEquivalence : IsEquivalence Map _≈_
        LiftEquivalence = record
            { ≈-refl = λ {m} → (⊆-refl m , ⊆-refl m)
            ; ≈-sym = λ {m₁} {m₂} (m₁⊆m₂ , m₂⊆m₁) → (m₂⊆m₁ , m₁⊆m₂)
            ; ≈-trans = λ {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) →
                ( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃
                , ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁
                )
            }