------------------------------------------------------------------------
-- Properties of homogeneous binary relations
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

-- This file contains some core definitions which are reexported by
-- Relation.Binary or Relation.Binary.PropositionalEquality.

module Relation.Binary.Core where

open import Data.Product
open import Data.Sum
open import Data.Function
open import Level
open import Relation.Nullary.Core

------------------------------------------------------------------------
-- Homogeneous binary relations

REL : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
REL A ℓ = A → A → Set ℓ

Rel : ∀ {a} → Set a → Set (suc zero ⊔ a)
Rel A = REL A zero

------------------------------------------------------------------------
-- Simple properties of binary relations

infixr  _⇒_ _=[_]⇒_

-- Implication/containment. Could also be written ⊆.

_⇒_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → REL A ℓ₁ → REL A ℓ₂ → Set _
P ⇒ Q = ∀ {i j} → P i j → Q i j

-- Generalised implication. If P ≡ Q it can be read as "f preserves
-- P".

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
          REL A ℓ₁ → (A → B) → REL B ℓ₂ → Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)

-- A synonym, along with a binary variant.

_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
                (A → B) → REL A ℓ₁ → REL B ℓ₂ → Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q

_Preserves₂_⟶_⟶_ :
  ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
  (A → B → C) → REL A ℓ₁ → REL B ℓ₂ → REL C ℓ₃ → Set _
_+_ Preserves₂ P ⟶ Q ⟶ R =
  ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

-- Reflexivity of _∼_ can be expressed as _≈_ ⇒ _∼_, for some
-- underlying equality _≈_. However, the following variant is often
-- easier to use.

Reflexive : ∀ {a ℓ} {A : Set a} → REL A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x

-- Irreflexivity is defined using an underlying equality.

Irreflexive : ∀ {a ℓ₁ ℓ₂} {A : Set a} → REL A ℓ₁ → REL A ℓ₂ → Set _
Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)

-- Generalised symmetry.

Sym : ∀ {a ℓ₁ ℓ₂} {A : Set a} → REL A ℓ₁ → REL A ℓ₂ → Set _
Sym P Q = P ⇒ flip Q

Symmetric : ∀ {a ℓ} {A : Set a} → REL A ℓ → Set _
Symmetric _∼_ = Sym _∼_ _∼_

-- Generalised transitivity.

Trans : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} →
        REL A ℓ₁ → REL A ℓ₂ → REL A ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

Transitive : ∀ {a ℓ} {A : Set a} → REL A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_

Antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} → REL A ℓ₁ → REL A ℓ₂ → Set _
Antisymmetric _≈_ _≤_ = ∀ {x y} → x ≤ y → y ≤ x → x ≈ y

Asymmetric : ∀ {a ℓ} {A : Set a} → REL A ℓ → Set _
Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

_Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → REL A ℓ₂ → Set _
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y

_Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → REL A ℓ₁ → REL A ℓ₂ → Set _
P Respects₂ _∼_ =
  (∀ {x} → P x      Respects _∼_) ×
  (∀ {y} → flip P y Respects _∼_)

Substitutive : ∀ {a ℓ₁} {A : Set a} → REL A ℓ₁ → (ℓ₂ : Level) → Set _
Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_

Decidable : ∀ {a ℓ} {A : Set a} → REL A ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

Total : ∀ {a ℓ} {A : Set a} → REL A ℓ → Set _
Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x)

data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
         Set (a ⊔ b ⊔ c) where
  tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≈ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C

Trichotomous : ∀ {a ℓ₁ ℓ₂} {A : Set a} → REL A ℓ₁ → REL A ℓ₂ → Set _
Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
  where _>_ = flip _<_

record NonEmpty {i ℓ} {I : Set i} (T : REL I ℓ) : Set (i ⊔ ℓ) where
  constructor nonEmpty
  field
    {i₁ i₂} : I
    proof   : T i₁ i₂

------------------------------------------------------------------------
-- Propositional equality

-- This dummy module is used to avoid shadowing of the field named
-- refl defined in IsEquivalence below. The module is opened publicly
-- at the end of this file.

private
 module Dummy where

  infix  _≡_ _≢_

  data _≡_ {a} {A : Set a} (x : A) : A → Set where
    refl : x ≡ x

  {-# BUILTIN EQUALITY _≡_ #-}
  {-# BUILTIN REFL refl #-}

  -- Nonequality.

  _≢_ : ∀ {a} {A : Set a} → A → A → Set
  x ≢ y = ¬ x ≡ y

------------------------------------------------------------------------
-- Equivalence relations

-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.

record IsEquivalence {a ℓ} {A : Set a}
                     (_≈_ : REL A ℓ) : Set (a ⊔ ℓ) where
  field
    refl  : Reflexive _≈_
    sym   : Symmetric _≈_
    trans : Transitive _≈_

  reflexive : Dummy._≡_ ⇒ _≈_
  reflexive Dummy.refl = refl

open Dummy public