------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to ◇
------------------------------------------------------------------------

module Data.Container.Any where

open import Algebra
open import Data.Container as C
open import Data.Container.Combinator
  using (module Composition) renaming (_∘_ to _⟨∘⟩_)
open import Data.Product as Prod hiding (swap)
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Related as Related using (Related)
open import Function.Related.TypeIsomorphisms
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_; refl)
import Relation.Binary.Sigma.Pointwise as Σ

open Related.EquationalReasoning
private
  module ×⊎ {k } = CommutativeSemiring (×⊎-CommutativeSemiring k )

-- ◇ can be expressed using _∈_.

↔∈ :  {c} (C : Container c) {X : Set c}
       {P : X  Set c} {xs :  C  X} 
      P xs  ( λ x  x  xs × P x)
↔∈ _ {P = P} {xs} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = λ _  refl
    ; right-inverse-of = to∘from
    }
  }
  where
  to :  P xs   λ x  x  xs × P x
  to (p , Px) = (proj₂ xs p , (p , refl) , Px)

  from : ( λ x  x  xs × P x)   P xs
  from (.(proj₂ xs p) , (p , refl) , Px) = (p , Px)

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

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

cong :  {k c} {C : Container c}
         {X : Set c} {P₁ P₂ : X  Set c} {xs₁ xs₂ :  C  X} 
       (∀ x  Related k (P₁ x) (P₂ x))  xs₁ ∼[ k ] xs₂ 
       Related k ( P₁ xs₁) ( P₂ xs₂)
cong {C = C} {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
   P₁ xs₁                  ↔⟨ ↔∈ C 
  ( λ x  x  xs₁ × P₁ x)  ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) 
  ( λ x  x  xs₂ × P₂ x)  ↔⟨ sym (↔∈ C) 
   P₂ xs₂                  

-- Nested occurrences of ◇ can sometimes be swapped.

swap :  {c} {C₁ C₂ : Container c} {X Y : Set c} {P : X  Y  Set c}
         {xs :  C₁  X} {ys :  C₂  Y} 
       let  :  {C : Container c} {X}   C  X  (X  Set c)  Set c= flip  in
        xs ( ys  P)   ys ( xs  flip P)
swap {c} {C₁} {C₂} {P = P} {xs} {ys} =
    x   (P x) ys) xs                    ↔⟨ ↔∈ C₁ 
  ( λ x  x  xs ×  (P x) ys)              ↔⟨ Σ.cong Inv.id  {x}  Inv.id  ×⊎.*-cong {= c}  ↔∈ C₂ {P = P x}) 
  ( λ x  x  xs ×  λ y  y  ys × P x y)  ↔⟨ Σ.cong Inv.id  {x}  ∃∃↔∃∃ {A = x  xs}  _ 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 Inv.id  {y}  Σ.cong Inv.id  {x} 
    (x  xs × y  ys × P x y)                     ↔⟨ sym $ ×⊎.*-assoc _ _ _ 
    ((x  xs × y  ys) × P x y)                   ↔⟨ ×⊎.*-comm _ _  ×⊎.*-cong {= c}  Inv.id 
    ((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 Inv.id  {y}  ∃∃↔∃∃ {B = y  ys}  x _  x  xs × P x y)) 
  ( λ y  y  ys ×  λ x  x  xs × P x y)  ↔⟨ Σ.cong Inv.id  {y}  Inv.id  ×⊎.*-cong {= c}  sym (↔∈ C₁ {P = flip P y})) 
  ( λ y  y  ys ×  (flip P y) xs)         ↔⟨ sym (↔∈ C₂) 
    y   (flip P y) xs) ys               

-- Nested occurrences of ◇ can sometimes be flattened.

flatten :  {c} {C₁ C₂ : Container c} {X}
          P (xss :  C₁  ( C₂  X)) 
           ( P) xss 
           P (Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss)
flatten {C₁ = C₁} {C₂} {X} P xss = record
  { to         = P.→-to-⟶ t
  ; from       = P.→-to-⟶ f
  ; inverse-of = record
    { left-inverse-of  = λ _  refl
    ; right-inverse-of = λ _  refl
    }
  }
  where
  open Inverse

  t :  ( P) xss   P (from (Composition.correct C₁ C₂) ⟨$⟩ xss)
  t (p₁ , p₂ , p) = ((p₁ , p₂) , p)

  f :  P (from (Composition.correct C₁ C₂) ⟨$⟩ xss)   ( P) xss
  f ((p₁ , p₂) , p) = (p₁ , p₂ , p)

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

◇⊎↔⊎◇ :  {c} {C : Container c} {X : Set c} {xs :  C  X}
          {P Q : X  Set c} 
          x  P x  Q x) xs  ( P xs   Q xs)
◇⊎↔⊎◇ {xs = xs} {P} {Q} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = [  _  refl) ,  _  refl) ]
    }
  }
  where
  to :   x  P x  Q x) xs   P xs   Q xs
  to (pos , inj₁ p) = inj₁ (pos , p)
  to (pos , inj₂ q) = inj₂ (pos , q)

  from :  P xs   Q xs    x  P x  Q x) xs
  from = [ Prod.map id inj₁ , Prod.map id inj₂ ]

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

-- Products "commute" with ◇.

×◇↔◇◇× :  {c} {C₁ C₂ : Container c}
           {X Y} {P : X  Set c} {Q : Y  Set c}
           {xs :  C₁  X} {ys :  C₂  Y} 
           x    y  P x × Q y) ys) xs  ( P xs ×  Q ys)
×◇↔◇◇× {C₁ = C₁} {C₂} {P = P} {Q} {xs} {ys} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = λ _  refl
    ; right-inverse-of = λ _  refl
    }
  }
  where
  to :   x    y  P x × Q y) ys) xs   P xs ×  Q ys
  to (p₁ , p₂ , p , q) = ((p₁ , p) , (p₂ , q))

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

-- map can be absorbed by the predicate.

map↔∘ :  {c} (C : Container c) {X Y : Set c}
        (P : Y  Set c) {xs :  C  X} (f : X  Y) 
         P (C.map f xs)   (P  f) xs
map↔∘ _ _ _ = Inv.id

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

∈map↔∈×≡ :  {c} (C : Container c) {X Y : Set c} {f : X  Y}
             {xs :  C  X} {y} 
           y  C.map f xs  ( λ x  x  xs × y  f x)
∈map↔∈×≡ {c} C {f = f} {xs} {y} =
  y  C.map f xs              ↔⟨ map↔∘ C (_≡_ y) f 
    x  y  f x) xs        ↔⟨ ↔∈ C 
  ( λ x  x  xs × y  f x)  

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

map-cong :  {k c} {C : Container c} {X Y : Set c}
             {f₁ f₂ : X  Y} {xs₁ xs₂ :  C  X} 
           f₁  f₂  xs₁ ∼[ k ] xs₂ 
           C.map f₁ xs₁ ∼[ k ] C.map f₂ xs₂
map-cong {c = c} {C} {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
  x  C.map f₁ xs₁        ↔⟨ map↔∘ C (_≡_ x) f₁ 
    y  x  f₁ y) xs₁  ∼⟨ cong {xs₁ = xs₁} {xs₂ = xs₂} (Related.↔⇒  helper) xs₁≈xs₂ 
    y  x  f₂ y) xs₂  ↔⟨ sym (map↔∘ C (_≡_ x) f₂) 
  x  C.map f₂ xs₂        
  where
  helper :  y  (x  f₁ y)  (x  f₂ y)
  helper y = record
    { to         = P.→-to-⟶  x≡f₁y  P.trans x≡f₁y (        f₁≗f₂ y))
    ; from       = P.→-to-⟶  x≡f₂y  P.trans x≡f₂y (P.sym $ f₁≗f₂ y))
    ; inverse-of = record
      { left-inverse-of  = λ _  P.proof-irrelevance _ _
      ; right-inverse-of = λ _  P.proof-irrelevance _ _
      }
    }

-- Uses of linear morphisms can be removed.

remove-linear :
   {c} {C₁ C₂ : Container c} {X} {xs :  C₁  X}
  (P : X  Set c) (m : C₁  C₂) 
   P ( m ⟫⊸ xs)   P xs
remove-linear {xs = xs} P m = record
  { to         = P.→-to-⟶ t
  ; from       = P.→-to-⟶ f
  ; inverse-of = record
    { left-inverse-of  = f∘t
    ; right-inverse-of = t∘f
    }
  }
  where
  open Inverse

  t :  P ( m ⟫⊸ xs)   P xs
  t = Prod.map (_⟨$⟩_ (to (position⊸ m))) id

  f :  P xs   P ( m ⟫⊸ xs)
  f = Prod.map (_⟨$⟩_ (from (position⊸ m)))
               (P.subst (P  proj₂ xs)
                        (P.sym $ right-inverse-of (position⊸ m) _))

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

  t∘f : t  f  id
  t∘f (p₁ , p) = H.≅-to-≡ $
    H.cong₂ _,_ (H.≡-to-≅ $ right-inverse-of (position⊸ m) p₁)
                (H.≡-subst-removable
                  (P  proj₂ xs)
                  (P.sym (right-inverse-of (position⊸ m) p₁))
                  p)

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

linear-identity :
   {c} {C : Container c} {X} {xs :  C  X} (m : C  C) 
   m ⟫⊸ xs ∼[ bag ] xs
linear-identity {xs = xs} m {x} =
  x   m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m 
  x         xs  

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

join↔◇ :  {c} {C₁ C₂ C₃ : Container c} {X}
         P (join′ : (C₁ ⟨∘⟩ C₂)  C₃) (xss :  C₁  ( C₂  X)) 
         let join :  {X}   C₁  ( C₂  X)   C₃  X
             join =  join′ ⟫⊸ 
                    _⟨$⟩_ (Inverse.from (Composition.correct C₁ C₂)) in
          P (join xss)   ( P) xss
join↔◇ {C₁ = C₁} {C₂} P join xss =
   P ( join ⟫⊸ xss′)  ↔⟨ remove-linear P join 
   P            xss′   ↔⟨ sym $ flatten P xss 
   ( P) xss           
  where xss′ = Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss