------------------------------------------------------------------------
-- The Agda standard library
--
-- Propertiers of any for containers
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Container.Relation.Unary.Any.Properties where

open import Algebra.Bundles using (CommutativeSemiring)
open import Data.Product.Base using (∃; _×_; ∃₂; _,_; proj₂)
open import Data.Product.Properties using (Σ-≡,≡→≡)
open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Function.Base using (_∘_; _∘′_; id; flip; _$_)
open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
open import Function.Properties.Inverse using (↔-refl)
open import Function.Properties.Inverse.HalfAdjointEquivalence using (_≃_; ↔⇒≃)
open import Function.Related.Propositional as Related using (Related; SK-sym)
open import Function.Related.TypeIsomorphisms
  using (×-⊎-commutativeSemiring; ∃∃↔∃∃; Σ-assoc; ×-comm)
open import Level using (Level; _⊔_)
open import Relation.Unary using (Pred ; _∪_ ; _∩_)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.PropositionalEquality.Core as ≡
  using (_≡_; _≗_; refl)
open import Relation.Binary.PropositionalEquality.Properties as ≡

private
  module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ)


open import Data.Container.Core
import Data.Container.Combinator as C
open import Data.Container.Combinator.Properties
open import Data.Container.Related
open import Data.Container.Relation.Unary.Any as Any using (◇; any)
open import Data.Container.Membership

module _ {s p} (C : Container s p) {x} {X : Set x} {ℓ} {P : Pred X ℓ} where

-- ◇ can be unwrapped to reveal the Σ type

  ↔Σ : ∀ {xs : ⟦ C ⟧ X} → ◇ C P xs ↔ ∃ λ p → P (proj₂ xs p)
  ↔Σ {xs} = mk↔ₛ′ ◇.proof any (λ _ → refl) (λ _ → refl)

-- ◇ can be expressed using _∈_.

  ↔∈ : ∀ {xs : ⟦ C ⟧ X} → ◇ C P xs ↔ (∃ λ x → x ∈ xs × P x)
  ↔∈ {xs} = mk↔ₛ′ to from to∘from (λ _ → refl) where

    to : ◇ C P xs → ∃ λ x → x ∈ xs × P x
    to (any (p , Px)) = (proj₂ xs p , (any (p , refl)) , Px)

    from : (∃ λ x → x ∈ xs × P x) → ◇ C P xs
    from (.(proj₂ xs p) , (any (p , refl)) , Px) = any (p , Px)

    to∘from : to ∘ from ≗ id
    to∘from (.(proj₂ xs p) , any (p , refl) , Px) = refl

module _ {s p} {C : Container s p} {x} {X : Set x}
         {ℓ₁ ℓ₂} {P₁ : Pred X ℓ₁} {P₂ : Pred X ℓ₂} where
-- ◇ is a congruence for bag and set equality and related preorders.

  cong : ∀ {k} {xs₁ xs₂ : ⟦ C ⟧ X} →
         (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ≲[ k ] xs₂ →
         Related k (◇ C P₁ xs₁) (◇ C P₂ xs₂)
  cong {k} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
    ◇ C P₁ xs₁               ↔⟨ ↔∈ C ⟩
    (∃ λ x → x ∈ xs₁ × P₁ x) ∼⟨ Σ.cong ↔-refl (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
    (∃ λ x → x ∈ xs₂ × P₂ x) ↔⟨ SK-sym (↔∈ C) ⟩
    ◇ C P₂ xs₂               ∎
    where open Related.EquationalReasoning

-- Nested occurrences of ◇ can sometimes be swapped.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x y} {X : Set x} {Y : Set y} {r} {P : REL X Y r} where

  swap : {xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
         let ◈ : ∀ {s p} {C : Container s p} {x} {X : Set x} {ℓ} → ⟦ C ⟧ X → Pred X ℓ → Set (p ⊔ ℓ)
             ◈ = λ {_} {_} → flip (◇ _) in
         ◈ xs (◈ ys ∘ P) ↔ ◈ ys (◈ xs ∘ flip P)
  swap {xs} {ys} =
    ◇ _ (λ x → ◇ _ (P x) ys) xs                ↔⟨ ↔∈ C₁ ⟩
    (∃ λ x → x ∈ xs × ◇ _ (P x) ys)            ↔⟨ Σ.cong ↔-refl $ Σ.cong ↔-refl $ ↔∈ C₂ ⟩
    (∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y)  ↔⟨ Σ.cong ↔-refl (λ {x} → ∃∃↔∃∃ (λ _ y → y ∈ ys × P x y)) ⟩
    (∃₂ λ x y → x ∈ xs × y ∈ ys × P x y)       ↔⟨ ∃∃↔∃∃ (λ x y → x ∈ xs × y ∈ ys × P x y) ⟩
    (∃₂ λ y x → x ∈ xs × y ∈ ys × P x y)       ↔⟨ Σ.cong ↔-refl (λ {y} → Σ.cong ↔-refl (λ {x} →
      (x ∈ xs × y ∈ ys × P x y)                     ↔⟨ SK-sym Σ-assoc ⟩
      ((x ∈ xs × y ∈ ys) × P x y)                   ↔⟨ Σ.cong (×-comm _ _) ↔-refl ⟩
      ((y ∈ ys × x ∈ xs) × P x y)                   ↔⟨ Σ-assoc ⟩
      (y ∈ ys × x ∈ xs × P x y)                     ∎)) ⟩
    (∃₂ λ y x → y ∈ ys × x ∈ xs × P x y)       ↔⟨ Σ.cong ↔-refl (λ {y} → ∃∃↔∃∃ {B = y ∈ ys} (λ x _ → x ∈ xs × P x y)) ⟩
    (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong ↔-refl (Σ.cong ↔-refl (SK-sym (↔∈ C₁))) ⟩
    (∃ λ y → y ∈ ys × ◇ _ (flip P y) xs)       ↔⟨ SK-sym (↔∈ C₂) ⟩
    ◇ _ (λ y → ◇ _ (flip P y) xs) ys           ∎
    where open Related.EquationalReasoning

-- Nested occurrences of ◇ can sometimes be flattened.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x} {X : Set x} {ℓ} (P : Pred X ℓ) where

  flatten : ∀ (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
            ◇ C₁ (◇ C₂ P) xss ↔
            ◇ (C₁ C.∘ C₂) P (Inverse.from (Composition.correct C₁ C₂) xss)
  flatten xss = mk↔ₛ′ t f (λ _ → refl) (λ _ → refl) where

    ◇₁ = ◇ C₁; ◇₂ = ◇ C₂; ◇₁₂ = ◇ (C₁ C.∘ C₂)
    open Inverse

    t : ◇₁ (◇₂ P) xss → ◇₁₂ P (from (Composition.correct C₁ C₂) xss)
    t (any (p₁ , (any (p₂ , p)))) = any (any (p₁ , p₂) , p)

    f : ◇₁₂ P (from (Composition.correct C₁ C₂) xss) → ◇₁ (◇₂ P) xss
    f (any (any (p₁ , p₂) , p)) = any (p₁ , any (p₂ , p))

-- Sums commute with ◇ (for a fixed instance of a given container).

module _ {s p} {C : Container s p} {x} {X : Set x}
         {ℓ ℓ′} {P : Pred X ℓ} {Q : Pred X ℓ′} where

  ◇⊎↔⊎◇ : ∀ {xs : ⟦ C ⟧ X} → ◇ C (P ∪ Q) xs ↔ (◇ C P xs ⊎ ◇ C Q xs)
  ◇⊎↔⊎◇ {xs} = mk↔ₛ′ to from to∘from from∘to
    where
    to : ◇ C (λ x → P x ⊎ Q x) xs → ◇ C P xs ⊎ ◇ C Q xs
    to (any (pos , inj₁ p)) = inj₁ (any (pos , p))
    to (any (pos , inj₂ q)) = inj₂ (any (pos , q))

    from : ◇ C P xs ⊎ ◇ C Q xs → ◇ C (λ x → P x ⊎ Q x) xs
    from = [ Any.map₂ inj₁ , Any.map₂ inj₂ ]

    from∘to : from ∘ to ≗ id
    from∘to (any (pos , inj₁ p)) = refl
    from∘to (any (pos , inj₂ q)) = refl

    to∘from : to ∘ from ≗ id
    to∘from = [ (λ _ → refl) , (λ _ → refl) ]

-- Products "commute" with ◇.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x y} {X : Set x} {Y : Set y} {ℓ ℓ′} {P : Pred X ℓ} {Q : Pred Y ℓ′} where

  ×◇↔◇◇× : ∀ {xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
           ◇ C₁ (λ x → ◇ C₂ (λ y → P x × Q y) ys) xs ↔ (◇ C₁ P xs × ◇ C₂ Q ys)
  ×◇↔◇◇× {xs} {ys} = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
    where
    ◇₁ = ◇ C₁; ◇₂ = ◇ C₂

    to : ◇₁ (λ x → ◇₂ (λ y → P x × Q y) ys) xs → ◇₁ P xs × ◇₂ Q ys
    to (any (p₁ , any (p₂ , p , q))) = (any (p₁ , p) , any (p₂ , q))

    from : ◇₁ P xs × ◇₂ Q ys → ◇₁ (λ x → ◇₂ (λ y → P x × Q y) ys) xs
    from (any (p₁ , p) , any (p₂ , q)) = any (p₁ , any (p₂ , p , q))

-- map can be absorbed by the predicate.

module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
         {ℓ} (P : Pred Y ℓ) where

  map↔∘ : ∀ {xs : ⟦ C ⟧ X} (f : X → Y) → ◇ C P (map f xs) ↔ ◇ C (P ∘′ f) xs
  map↔∘ {xs} f =
   ◇ C P (map f xs)          ↔⟨ ↔Σ C ⟩
   ∃ (P ∘′ proj₂ (map f xs)) ≡⟨⟩
   ∃ (P ∘′ f ∘′ proj₂ xs)    ↔⟨ SK-sym (↔Σ C) ⟩
   ◇ C (P ∘′ f) xs           ∎
   where open Related.EquationalReasoning

-- Membership in a mapped container can be expressed without reference
-- to map.

module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
         {ℓ} (P : Pred Y ℓ) where

  ∈map↔∈×≡ : ∀ {f : X → Y} {xs : ⟦ C ⟧ X} {y} →
             y ∈ map f xs ↔ (∃ λ x → x ∈ xs × y ≡ f x)
  ∈map↔∈×≡ {f = f} {xs} {y} =
    y ∈ map f xs               ↔⟨ map↔∘ C (y ≡_) f ⟩
    ◇ C (λ x → y ≡ f x) xs     ↔⟨ ↔∈ C ⟩
    ∃ (λ x → x ∈ xs × y ≡ f x) ∎
    where open Related.EquationalReasoning

-- map is a congruence for bag and set equality and related preorders.

module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
         {ℓ} (P : Pred Y ℓ) where

  map-cong : ∀ {k} {f₁ f₂ : X → Y} {xs₁ xs₂ : ⟦ C ⟧ X} →
             f₁ ≗ f₂ → xs₁ ≲[ k ] xs₂ →
             map f₁ xs₁ ≲[ k ] map f₂ xs₂
  map-cong {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
    x ∈ map f₁ xs₁           ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
    ◇ C (λ y → x ≡ f₁ y) xs₁ ∼⟨ cong (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
    ◇ C (λ y → x ≡ f₂ y) xs₂ ↔⟨ SK-sym (map↔∘ C (_≡_ x) f₂) ⟩
    x ∈ map f₂ xs₂           ∎
    where
    open Related.EquationalReasoning
    helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y)
    helper y rewrite f₁≗f₂ y = ↔-refl

-- Uses of linear morphisms can be removed.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x} {X : Set x} {ℓ} (P : Pred X ℓ) where

  remove-linear : ∀ {xs : ⟦ C₁ ⟧ X} (m : C₁ ⊸ C₂) → ◇ C₂ P (⟪ m ⟫⊸ xs) ↔ ◇ C₁ P xs
  remove-linear {xs} m = mk↔ₛ′ t f t∘f f∘t
    where
    open _≃_
    open ≡.≡-Reasoning

    position⊸m : ∀ {s} → Position C₂ (shape⊸ m s) ≃ Position C₁ s
    position⊸m = ↔⇒≃ (position⊸ m)

    ◇₁ = ◇ C₁; ◇₂ = ◇ C₂

    t : ◇₂ P (⟪ m ⟫⊸ xs) → ◇₁ P xs
    t = Any.map₁ (_⊸_.morphism m)

    f : ◇₁ P xs → ◇₂ P (⟪ m ⟫⊸ xs)
    f (any (x , p)) =
      any $ from position⊸m x
          , ≡.subst (P ∘′ proj₂ xs) (≡.sym (right-inverse-of position⊸m _)) p

    f∘t : f ∘ t ≗ id
    f∘t (any (p₂ , p)) = ≡.cong any $ Σ-≡,≡→≡
      ( left-inverse-of position⊸m p₂
      , (≡.subst (P ∘ proj₂ xs ∘ to position⊸m)
           (left-inverse-of position⊸m p₂)
           (≡.subst (P ∘ proj₂ xs)
              (≡.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              p)                                                ≡⟨ ≡.subst-∘ (left-inverse-of position⊸m _) ⟩

         ≡.subst (P ∘ proj₂ xs)
           (≡.cong (to position⊸m)
              (left-inverse-of position⊸m p₂))
           (≡.subst (P ∘ proj₂ xs)
              (≡.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              p)                                                ≡⟨ ≡.cong (λ eq → ≡.subst (P ∘ proj₂ xs) eq
                                                                                    (≡.subst (P ∘ proj₂ xs)
                                                                                       (≡.sym (right-inverse-of position⊸m _)) _))
                                                                     (_≃_.left-right position⊸m _) ⟩
         ≡.subst (P ∘ proj₂ xs)
           (right-inverse-of position⊸m
              (to position⊸m p₂))
           (≡.subst (P ∘ proj₂ xs)
              (≡.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              p)                                                ≡⟨ ≡.subst-subst (≡.sym (right-inverse-of position⊸m _)) ⟩

         ≡.subst (P ∘ proj₂ xs)
           (≡.trans
              (≡.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              (right-inverse-of position⊸m
                 (to position⊸m p₂)))
           p                                                    ≡⟨ ≡.cong (λ eq → ≡.subst (P ∘ proj₂ xs) eq p)
                                                                     (≡.trans-symˡ (right-inverse-of position⊸m _)) ⟩

         ≡.subst (P ∘ proj₂ xs) ≡.refl p                        ≡⟨⟩

        p                                                       ∎)
      )

    t∘f : t ∘ f ≗ id
    t∘f (any (p₁ , p)) = ≡.cong any $ Σ-≡,≡→≡
      ( right-inverse-of position⊸m p₁
      , (≡.subst (P ∘ proj₂ xs)
           (right-inverse-of position⊸m p₁)
           (≡.subst (P ∘ proj₂ xs)
              (≡.sym (right-inverse-of position⊸m p₁))
              p)                                                ≡⟨ ≡.subst-subst (≡.sym (right-inverse-of position⊸m _)) ⟩

         ≡.subst (P ∘ proj₂ xs)
           (≡.trans
              (≡.sym (right-inverse-of position⊸m p₁))
              (right-inverse-of position⊸m p₁))
           p                                                    ≡⟨ ≡.cong (λ eq → ≡.subst (P ∘ proj₂ xs) eq p)
                                                                     (≡.trans-symˡ (right-inverse-of position⊸m _)) ⟩
         ≡.subst (P ∘ proj₂ xs) ≡.refl p                        ≡⟨⟩

        p                                                       ∎)
      )

-- Linear endomorphisms are identity functions if bag equality is used.

module _ {s p} {C : Container s p} {x} {X : Set x} where

  linear-identity : ∀ {xs : ⟦ C ⟧ X} (m : C ⊸ C) → ⟪ m ⟫⊸ xs ≲[ bag ] xs
  linear-identity {xs} m {x} =
    x ∈ ⟪ m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m ⟩
    x ∈        xs  ∎
    where open Related.EquationalReasoning

-- If join can be expressed using a linear morphism (in a certain
-- way), then it can be absorbed by the predicate.

module _ {s₁ s₂ s₃ p₁ p₂ p₃}
         {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃}
         {x} {X : Set x} {ℓ} (P : Pred X ℓ) where

  join↔◇ : (join′ : (C₁ C.∘ C₂) ⊸ C₃) (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
           let join : ∀ {X} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₃ ⟧ X
               join = λ {_} → ⟪ join′ ⟫⊸ ∘
                      (Inverse.from (Composition.correct C₁ C₂)) in
           ◇ C₃ P (join xss) ↔ ◇ C₁ (◇ C₂ P) xss
  join↔◇ join xss =
    ◇ C₃ P (⟪ join ⟫⊸ xss′) ↔⟨ remove-linear P join ⟩
    ◇ (C₁ C.∘ C₂) P xss′    ↔⟨ SK-sym $ flatten P xss ⟩
    ◇ C₁ (◇ C₂ P) xss       ∎
    where
    open Related.EquationalReasoning
    xss′ = Inverse.from (Composition.correct C₁ C₂) xss