{-# OPTIONS --safe --no-import-sorts #-}
{-# OPTIONS -v allTactics:100 #-}
 
open import abstract-set-theory.Prelude hiding (map)
open import Axiom.Set using (Theory)
 
module Axiom.Set.Rel (th : Theory) where
 
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
import Function.Related.Propositional as R
 
open Theory th
open import Axiom.Set.Properties th
 
import Data.Product as ×
open import Data.List.Ext.Properties using (_⊎-cong_)
open import Data.Maybe.Base using () renaming (map to map?)
open import Data.Product.Properties using (,-injectiveˡ; ×-≡,≡→≡; ×-≡,≡←≡)
open import Data.Product.Properties.Ext using (∃-cong′; ∃-distrib-⊎)
open import Relation.Unary using (Decidable)
open import Relation.Binary using (_Preserves_⟶_)
 
open import Tactic.AnyOf
open import Tactic.Defaults
 
open Equivalence
 
-- Because of missing macro hygiene, we have to copy&paste this.
-- c.f. https://github.com/agda/agda/issues/3819
private macro
  ∈⇒P = anyOfⁿᵗ
    (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ [])
  P⇒∈ = anyOfⁿᵗ
    (quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ [])
  ∈⇔P = anyOfⁿᵗ
    ( quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻
    ∷ quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ [])
 
Rel : Type → Type → Type
Rel A B = Set (A × B)
 
private variable A A' B B' C : Type
                 R R' : Rel A B
                 X : Set A
 
relatedˡ : Rel A B → Set A
relatedˡ = map proj₁
 
∅ʳ : Rel A B
∅ʳ = ∅
 
dom : Rel A B → Set A
dom = map proj₁
 
range : Rel A B → Set B
range = map proj₂
 
disjoint-dom⇒disjoint : disjoint (dom R) (dom R') → disjoint R R'
disjoint-dom⇒disjoint disj = ∈-map⁺'' -⟨ disj ⟩- ∈-map⁺''
 
_∣'_ : {P : A → Type} → Rel A B → specProperty P → Rel A B
m ∣' P? = filter (sp-∘ P? proj₁) m
 
_∣^'_ : {P : B → Type} → Rel A B → specProperty P → Rel A B
m ∣^' P? = filter (sp-∘ P? proj₂) m
 
impl⇒res⊆ : ∀ {X : Rel A B} {P P'} (sp-P : specProperty P) (sp-P' : specProperty P')
          → (∀ {a} → P a → P' a) → X ∣' sp-P ⊆ X ∣' sp-P'
impl⇒res⊆ sp-P sp-P' P⇒P' a∈X∣'P = ∈⇔P (×.map₁ P⇒P' (∈⇔P a∈X∣'P))
 
impl⇒cores⊆ : ∀ {X : Rel A B} {P P'} (sp-P : specProperty P) (sp-P' : specProperty P')
            → (∀ {b} → P b → P' b) → X ∣^' sp-P ⊆ X ∣^' sp-P'
impl⇒cores⊆ sp-P sp-P' P⇒P' a∈X∣^'P = ∈⇔P (×.map₁ P⇒P' (∈⇔P a∈X∣^'P))
 
mapˡ : (A → A') → Rel A B → Rel A' B
mapˡ f R = map (×.map₁ f) R
 
mapʳ : (B → B') → Rel A B → Rel A B'
mapʳ f R = map (×.map₂ f) R
 
dom∈ : ∀ {a} → (∃[ b ] (a , b) ∈ R) ⇔ a ∈ dom R
dom∈ {R = R} {a} =
  (∃[ b ] (a , b) ∈ R)            ∼⟨ R.SK-sym (mk⇔ (λ { ((_ , y) , refl , ay∈R) → y , ay∈R })
                                              (λ (x , ax∈R) → (a , x) , refl , ax∈R)) ⟩
  (∃[ a₁ ] a ≡ proj₁ a₁ × a₁ ∈ R) ∼⟨ ∈-map ⟩
 
  a ∈ dom R                       ∎
  where open R.EquationalReasoning
 
module _ {x : A} {y : B} where
  module _ {a : A} where
    ∈-dom-singleton-pair : a ≡ x ⇔ a ∈ dom ❴ x , y ❵
    ∈-dom-singleton-pair = mk⇔ (λ a≡x → to dom∈ (y , to ∈-singleton (×-≡,≡→≡ (a≡x , refl))))
                               (,-injectiveˡ ∘ from ∈-singleton ∘ proj₂ ∘ from dom∈)
 
    dom-single→single : a ∈ dom ❴ x , y ❵ → a ∈ ❴ x ❵
    dom-single→single = to ∈-singleton ∘ from ∈-dom-singleton-pair
 
    single→dom-single : a ∈ ❴ x ❵ → a ∈ dom ❴ x , y ❵
    single→dom-single = to ∈-dom-singleton-pair ∘ from ∈-singleton
 
  dom-single≡single : dom ❴ x , y ❵ ≡ᵉ ❴ x ❵
  dom-single≡single = dom-single→single , single→dom-single
 
∈-dom : {a : A × B} → a ∈ R → proj₁ a ∈ dom R
∈-dom {a = a} a∈ = to ∈-map (a , (refl , a∈))
 
∉-dom∅ : {a : A} → a ∉ dom{A}{B} ∅
∉-dom∅ {a} a∈dom∅ = ⊥-elim $ ∉-∅ $ proj₂ $ (from dom∈) a∈dom∅
 
dom∅ : dom{A}{B} ∅ ≡ᵉ ∅
dom∅ = ⊥-elim ∘ ∉-dom∅ , ∅-minimum (dom ∅)
 
dom∪ : dom (R ∪ R') ≡ᵉ dom R ∪ dom R'
dom∪ {R = R} {R'} = from ≡ᵉ⇔≡ᵉ' λ a →
  a ∈ dom (R ∪ R')                           ∼⟨ R.SK-sym dom∈ ⟩
  (∃[ b ] (a , b) ∈ R ∪ R')                  ∼⟨ ∃-cong′ (R.SK-sym ∈-∪) ⟩
  (∃[ b ] ((a , b) ∈ R ⊎ (a , b) ∈ R'))      ↔⟨ ∃-distrib-⊎ ⟩
  (∃[ b ] (a , b) ∈ R ⊎ ∃[ b ] (a , b) ∈ R') ∼⟨ dom∈ ⊎-cong dom∈ ⟩
  (a ∈ dom R ⊎ a ∈ dom R')                   ∼⟨ ∈-∪ ⟩
  a ∈ dom R ∪ dom R'                         ∎
  where open R.EquationalReasoning
 
dom⊆ : dom{A}{B} Preserves _⊆_ ⟶ _⊆_
dom⊆ R⊆R' a∈ = to dom∈ $ proj₁ (from dom∈ a∈) , R⊆R' (proj₂ (from dom∈ a∈))
 
dom-cong : R ≡ᵉ R' → dom R ≡ᵉ dom R'
dom-cong RR' = (dom⊆ (proj₁ RR')) , (dom⊆ (proj₂ RR'))
 
dom-⊆mapʳ : {f : B → B'} → dom R ⊆ dom (mapʳ f R)
dom-⊆mapʳ {f = f} {a} a∈domR with from dom∈ a∈domR
... | b , ab∈R = to dom∈ (f b , to ∈-map ((a , b) , refl , ab∈R))
 
dom-mapʳ⊆ : {f : B → B'} → dom (mapʳ f R) ⊆ dom R
dom-mapʳ⊆ a∈dmR with from dom∈ a∈dmR
... | _ , p∈map with from ∈-map p∈map
... | (_ , b) , refl , ab∈R = to dom∈ (b , ab∈R)
 
mapʳ-dom : {f : B → B'} → dom R ≡ᵉ dom (mapʳ f R)
mapʳ-dom = dom-⊆mapʳ , dom-mapʳ⊆
 
dom-mapˡ≡map-dom : {f : A → A'} → dom (mapˡ f R) ≡ᵉ map f (dom R)
dom-mapˡ≡map-dom .proj₁ a'∈dom with from ∈-map (proj₂ (from dom∈ a'∈dom))
... | (a , b) , a'b≡fab , ab∈R = to ∈-map (a , proj₁ (×-≡,≡←≡ a'b≡fab) , to dom∈ (b , ab∈R))
dom-mapˡ≡map-dom .proj₂ a'∈map with from ∈-map a'∈map
... | a , a'≡fa , a∈domR with from dom∈ a∈domR
... | b , ab∈R = to dom∈ (b , to ∈-map ((a , b) , ×-≡,≡→≡ (a'≡fa , refl) , ab∈R))
 
dom-∅ : dom R ⊆ ∅ → R ≡ᵉ ∅
dom-∅ dom⊆∅ = ∅-least (λ {x} x∈R → ⊥-elim $ ∉-∅ $ dom⊆∅ $ to dom∈ (-, x∈R))
 
mapPartialLiftKey : (A → B → Maybe B') → A × B → Maybe (A × B')
mapPartialLiftKey f (k , v) = map? (k ,_) (f k v)
 
mapPartialLiftKey-map : ∀ {a : A} {b' : B'} {f : A → B → Maybe B'} {r : Rel A B}
  → just (a , b') ∈ map (mapPartialLiftKey f) r
  → ∃[ b ] just b' ≡ f a b × (a , b) ∈ r
mapPartialLiftKey-map {f = f} ab∈m
  with from ∈-map ab∈m
... | (a' , b') , ≡ , a'b'∈r
  with f a' b' in eq
mapPartialLiftKey-map {f = f} ab∈m | (a' , b') , refl , a'b'∈r | just x
  = b' , sym eq , a'b'∈r
 
mapMaybeWithKey : (A → B → Maybe B') → Rel A B → Rel A B'
mapMaybeWithKey f r = mapPartial (mapPartialLiftKey f) r
 
∈-mapMaybeWithKey : ∀ {a : A} {b' : B'} {f : A → B → Maybe B'} {r : Rel A B}
  → (a , b') ∈ mapMaybeWithKey f r
  → ∃[ b ] (just b' ≡ f a b × (a , b) ∈ r)
∈-mapMaybeWithKey {a = a} {b'} {f} ab'∈
  = mapPartialLiftKey-map {f = f}
  $ ⊆-mapPartial
  $ to (∈-map {f = just}) ((a , b') , refl , ab'∈)
 
module Restriction (sp-∈ : spec-∈ A) where
 
  _∣_ : Rel A B → Set A → Rel A B
  m ∣ X = m ∣' sp-∈ {X}
 
  _∣_ᶜ : Rel A B → Set A → Rel A B
  m ∣ X ᶜ = m ∣' sp-¬ (sp-∈ {X})
 
  _⟪$⟫_ : Rel A B → Set A → Set B
  m ⟪$⟫ X = range (m ∣ X)
 
  res-cong : (R ∣_) Preserves _≡ᵉ_ ⟶ _≡ᵉ_
  res-cong (X⊆Y , Y⊆X) = (λ ∈R∣X → ∈⇔P (×.map₁ X⊆Y (∈⇔P ∈R∣X)))
                       , (λ ∈R∣Y → ∈⇔P (×.map₁ Y⊆X (∈⇔P ∈R∣Y)))
 
  res-dom : dom (R ∣ X) ⊆ X
  res-dom a∈dom with ∈⇔P a∈dom
  ... | _ , refl , h = proj₁ $ ∈⇔P h
 
  res-domᵐ : dom (R ∣ X) ⊆ dom R
  res-domᵐ a∈dom with ∈⇔P a∈dom
  ... | _ , refl , h = ∈-map⁺'' $ proj₂ (∈⇔P h)
 
  res-comp-cong : (R ∣_ᶜ) Preserves _≡ᵉ_ ⟶ _≡ᵉ_
  res-comp-cong (X⊆Y , Y⊆X) = (λ ∈R∣X → ∈⇔P (×.map₁ (_∘ Y⊆X) (∈⇔P ∈R∣X)))
                            , (λ ∈R∣Y → ∈⇔P (×.map₁ (_∘ X⊆Y) (∈⇔P ∈R∣Y)))
 
  res-comp-dom : ∀ {a} → a ∈ dom (R ∣ X ᶜ) → a ∉ X
  res-comp-dom a∈dom with ∈⇔P a∈dom
  ... | _ , refl , h = proj₁ $ ∈⇔P h
 
  res-comp-domᵐ : dom (R ∣ X ᶜ) ⊆ dom R
  res-comp-domᵐ a∈dom with ∈⇔P a∈dom
  ... | _ , refl , h = ∈-map⁺'' (proj₂ (∈⇔P h))
 
  res-⊆ : (R ∣ X) ⊆ R
  res-⊆ = proj₂ ∘′ ∈⇔P
 
  ex-⊆ : (R ∣ X ᶜ) ⊆ R
  ex-⊆ = proj₂ ∘′ ∈⇔P
 
  res-∅ : R ∣ ∅ ≡ᵉ ∅
  res-∅ = dom-∅ res-dom
 
  res-∅ᶜ : R ∣ ∅ ᶜ ≡ᵉ R
  res-∅ᶜ = ex-⊆ , λ a∈R → ∈⇔P (∉-∅ , a∈R)
 
  ∈-resᶜ-dom⁻ : ∀ {a} → a ∈ dom (R ∣ X ᶜ) → a ∉ X × ∃[ b ] (a , b) ∈ R
  ∈-resᶜ-dom⁻ a∈ = res-comp-dom a∈ , from dom∈ (dom⊆ ex-⊆ a∈)
 
  ∈-resᶜ-dom⁺ : ∀ {a} → a ∉ X × ∃[ b ] (a , b) ∈ R → a ∈ dom (R ∣ X ᶜ)
  ∈-resᶜ-dom⁺ (a∉X , (b , ab∈R)) = to dom∈ (b , (∈⇔P (a∉X , ab∈R)))
 
  ∈-resᶜ-dom : ∀ {a} → a ∈ dom (R ∣ X ᶜ) ⇔ (a ∉ X × ∃[ b ] (a , b) ∈ R)
  ∈-resᶜ-dom = mk⇔ ∈-resᶜ-dom⁻ ∈-resᶜ-dom⁺
 
  res-ex-∪ : Decidable (_∈ X) → (R ∣ X) ∪ (R ∣ X ᶜ) ≡ᵉ R
  res-ex-∪ ∈X? = ∪-⊆ res-⊆ ex-⊆ , λ {a} h → case ∈X? (proj₁ a) of λ where
    (yes p) → ∈⇔P (inj₁ (∈⇔P (p , h)))
    (no ¬p) → ∈⇔P (inj₂ (∈⇔P (¬p , h)))
 
  res-ex-disjoint : disjoint (dom (R ∣ X)) (dom (R ∣ X ᶜ))
  res-ex-disjoint h h' = res-comp-dom h' (res-dom h)
 
  res-ex-disj-∪ : Decidable (_∈ X) → R ≡ (R ∣ X) ⨿ (R ∣ X ᶜ)
  res-ex-disj-∪ ∈X? = IsEquivalence.sym ≡ᵉ-isEquivalence (res-ex-∪ ∈X?)
                    , disjoint-dom⇒disjoint res-ex-disjoint
    where open import Relation.Binary using (IsEquivalence)
 
  curryʳ : Rel (A × B) C → A → Rel B C
  curryʳ R a = mapˡ proj₂ (R ∣' (sp-∘ (sp-∈ {X = ❴ a ❵}) proj₁))
 
  ∈-curryʳ : ∀ {a} {b : B} {c : C} → (b , c) ∈ curryʳ R a → ((a , b) , c) ∈ R
  ∈-curryʳ h = case ∈⇔P h of λ where
    (((a , b) , c) , refl , h'') → case ∈⇔P h'' of λ where
      (p , p') → case from ∈-singleton p of λ where refl → p'
 
  open Intersection sp-∈
  open Intersectionᵖ sp-∈
 
  res-dom-comm⊆∩ : {m : Rel A B} {m' : Rel A C} → dom (m ∣ dom m') ⊆ dom m ∩ dom m'
  res-dom-comm⊆∩ x = to ∈-∩ (res-domᵐ x , res-dom x)
 
  res-dom-comm∩⊆ : {m : Rel A B} {m' : Rel A C} → dom m ∩ dom m' ⊆ dom (m ∣ dom m')
  res-dom-comm∩⊆ {m = m} {m' = m'} x with from ∈-∩ x
  ... | a∈dm , a∈dm' with from dom∈ a∈dm | from dom∈ a∈dm'
  ... | b , ab∈m | c , ac∈m = to dom∈ (b , to ∈-filter (a∈dm' , ab∈m))
 
  res-dom-comm' : {m : Rel A B} {m' : Rel A C} → dom (m ∣ dom m') ≡ᵉ dom m ∩ dom m'
  res-dom-comm' = res-dom-comm⊆∩ , res-dom-comm∩⊆
 
  res-dom-comm : {m : Rel A B} {m' : Rel A C} → dom (m ∣ dom m') ≡ᵉ dom (m' ∣ dom m)
  res-dom-comm {m = m} {m'} = begin
    dom (m ∣ dom m') ≈⟨ res-dom-comm' ⟩
    dom m ∩ dom m'   ≈˘⟨ ∩-sym ⟩
    dom m' ∩ dom m   ≈˘⟨ res-dom-comm' ⟩
    dom (m' ∣ dom m) ∎
    where open SetoidReasoning ≡ᵉ-Setoid
 
module Corestriction (sp-∈ : spec-∈ B) where
 
  _∣^_ : Rel A B → Set B → Rel A B
  m ∣^ X = m ∣^' sp-∈ {X}
 
  _∣^_ᶜ : Rel A B → Set B → Rel A B
  m ∣^ X ᶜ = m ∣^' sp-¬ (sp-∈ {X})
 
  cores-⊆ : (R ∣^ X) ⊆ R
  cores-⊆ = proj₂ ∘′ ∈⇔P
 
  coex-⊆ : (R ∣^ X ᶜ) ⊆ R
  coex-⊆ = proj₂ ∘′ ∈⇔P