------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to maybes
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Maybe.Relation.Binary.Pointwise where
 
open import Level
open import Data.Product.Base using (∃; _×_; -,_; _,_)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.Any using (Any; just)
open import Function.Bundles using (_⇔_; mk⇔)
open import Relation.Binary.Core using (REL; Rel; _⇒_)
open import Relation.Binary.Bundles using (Setoid; DecSetoid)
open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable)
open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Nullary
open import Relation.Unary using (_⊆_)
import Relation.Nullary.Decidable as Dec
 
------------------------------------------------------------------------
-- Definition
 
data Pointwise
       {a b ℓ} {A : Set a} {B : Set b}
       (R : REL A B ℓ) : REL (Maybe A) (Maybe B) (a ⊔ b ⊔ ℓ) where
  just    : ∀ {x y} → R x y → Pointwise R (just x) (just y)
  nothing : Pointwise R nothing nothing
 
------------------------------------------------------------------------
-- Properties
 
module _ {a b ℓ} {A : Set a} {B : Set b} {R : REL A B ℓ} where
 
  drop-just : ∀ {x y} → Pointwise R (just x) (just y) → R x y
  drop-just (just p) = p
 
  just-equivalence : ∀ {x y} → R x y ⇔ Pointwise R (just x) (just y)
  just-equivalence = mk⇔ just drop-just
 
  nothing-inv : ∀ {x} → Pointwise R nothing x → x ≡ nothing
  nothing-inv nothing = ≡.refl
 
  just-inv : ∀ {x y} → Pointwise R (just x) y → ∃ λ z → y ≡ just z × R x z
  just-inv (just r) = -, ≡.refl , r
 
------------------------------------------------------------------------
-- Relational properties
 
module _ {a r} {A : Set a} {R : Rel A r} where
 
  refl : Reflexive R → Reflexive (Pointwise R)
  refl R-refl {just _}  = just R-refl
  refl R-refl {nothing} = nothing
 
  reflexive : _≡_ ⇒ R → _≡_ ⇒ Pointwise R
  reflexive reflexive ≡.refl = refl (reflexive ≡.refl)
 
module _ {a b r₁ r₂} {A : Set a} {B : Set b}
         {R : REL A B r₁} {S : REL B A r₂} where
 
  sym : Sym R S → Sym (Pointwise R) (Pointwise S)
  sym R-sym (just p) = just (R-sym p)
  sym R-sym nothing  = nothing
 
module _ {a b c r₁ r₂ r₃} {A : Set a} {B : Set b} {C : Set c}
         {R : REL A B r₁} {S : REL B C r₂} {T : REL A C r₃} where
 
  trans : Trans R S T → Trans (Pointwise R) (Pointwise S) (Pointwise T)
  trans R-trans (just p) (just q) = just (R-trans p q)
  trans R-trans nothing  nothing  = nothing
 
module _ {a r} {A : Set a} {R : Rel A r} where
 
  dec : Decidable R → Decidable (Pointwise R)
  dec R-dec (just x) (just y) = Dec.map just-equivalence (R-dec x y)
  dec R-dec (just x) nothing  = no (λ ())
  dec R-dec nothing  (just y) = no (λ ())
  dec R-dec nothing  nothing  = yes nothing
 
  isEquivalence : IsEquivalence R → IsEquivalence (Pointwise R)
  isEquivalence R-isEquivalence = record
    { refl  = refl R.refl
    ; sym   = sym R.sym
    ; trans = trans R.trans
    } where module R = IsEquivalence R-isEquivalence
 
  isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
  isDecEquivalence R-isDecEquivalence = record
    { isEquivalence = isEquivalence R.isEquivalence
    ; _≟_           = dec R._≟_
    } where module R = IsDecEquivalence R-isDecEquivalence
 
  pointwise⊆any : ∀ {x} → Pointwise R (just x) ⊆ Any (R x)
  pointwise⊆any (just Rxy) = just Rxy
 
module _ {c ℓ} where
 
  setoid : Setoid c ℓ → Setoid c (c ⊔ ℓ)
  setoid S = record
    { isEquivalence = isEquivalence S.isEquivalence
    } where module S = Setoid S
 
  decSetoid : DecSetoid c ℓ → DecSetoid c (c ⊔ ℓ)
  decSetoid S = record
    { isDecEquivalence = isDecEquivalence S.isDecEquivalence
    } where module S = DecSetoid S