------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to bag and set equality
------------------------------------------------------------------------

-- Bag and set equality are defined in Data.List.Any.

module Data.List.Any.BagAndSetEquality where

open import Algebra
open import Algebra.FunctionProperties
open import Category.Monad
open import Data.List as List
import Data.List.Properties as LP
open import Data.List.Any as Any using (Any); open Any.Any
open import Data.List.Any.Properties
open import Data.List.Any.Membership.Propositional
open import Data.Product
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
import Function.Equivalence as FE
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Related as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→)
open import Function.Related.TypeIsomorphisms
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_)
open import Relation.Binary.Sum
open import Relation.Nullary

open import Data.List.Any.Membership.Propositional.Properties
private
  module Eq  {k a} {A : Set a} = Setoid ([ k ]-Equality A)
  module Ord {k a} {A : Set a} = Preorder ([ k ]-Order A)
  module ×⊎ {k } = CommutativeSemiring (×⊎-CommutativeSemiring k )
  open module ListMonad {} = RawMonad (List.monad { = })
  module ListMonoid {a} {A : Set a} = Monoid (List.monoid A)

------------------------------------------------------------------------
-- Congruence lemmas

-- _∷_ is a congruence.

∷-cong :  {a k} {A : Set a} {x₁ x₂ : A} {xs₁ xs₂} 
         x₁  x₂  xs₁ ∼[ k ] xs₂  x₁  xs₁ ∼[ k ] x₂  xs₂
∷-cong {x₂ = x} {xs₁} {xs₂} P.refl xs₁≈xs₂ {y} =
  y  x  xs₁        ↔⟨ sym $ ∷↔ (_≡_ y) 
  (y  x  y  xs₁)  ∼⟨ (y  x ) ⊎-cong xs₁≈xs₂ 
  (y  x  y  xs₂)  ↔⟨ ∷↔ (_≡_ y) 
  y  x  xs₂        
  where open Related.EquationalReasoning

-- List.map is a congruence.

map-cong :  { k} {A B : Set } {f₁ f₂ : A  B} {xs₁ xs₂} 
           f₁  f₂  xs₁ ∼[ k ] xs₂ 
           List.map f₁ xs₁ ∼[ k ] List.map f₂ xs₂
map-cong {} {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
  x  List.map f₁ xs₁       ↔⟨ sym $ map↔ {a = } {b = } {p = } 
  Any  y  x  f₁ y) xs₁  ∼⟨ Any-cong (↔⇒  helper) xs₁≈xs₂ 
  Any  y  x  f₂ y) xs₂  ↔⟨ map↔ {a = } {b = } {p = } 
  x  List.map f₂ xs₂       
  where
  open Related.EquationalReasoning

  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 _ _
      }
    }

-- _++_ is a congruence.

++-cong :  {a k} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} 
          xs₁ ∼[ k ] xs₂  ys₁ ∼[ k ] ys₂ 
          xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
++-cong {a} {xs₁ = xs₁} {xs₂} {ys₁} {ys₂} xs₁≈xs₂ ys₁≈ys₂ {x} =
  x  xs₁ ++ ys₁       ↔⟨ sym $ ++↔ {a = a} {p = a} 
  (x  xs₁  x  ys₁)  ∼⟨ xs₁≈xs₂ ⊎-cong ys₁≈ys₂ 
  (x  xs₂  x  ys₂)  ↔⟨ ++↔ {a = a} {p = a} 
  x  xs₂ ++ ys₂       
  where open Related.EquationalReasoning

-- concat is a congruence.

concat-cong :  {a k} {A : Set a} {xss₁ xss₂ : List (List A)} 
              xss₁ ∼[ k ] xss₂  concat xss₁ ∼[ k ] concat xss₂
concat-cong {a} {xss₁ = xss₁} {xss₂} xss₁≈xss₂ {x} =
  x  concat xss₁         ↔⟨ sym $ concat↔ {a = a} {p = a} 
  Any (Any (_≡_ x)) xss₁  ∼⟨ Any-cong  _  _ ) xss₁≈xss₂ 
  Any (Any (_≡_ x)) xss₂  ↔⟨ concat↔ {a = a} {p = a} 
  x  concat xss₂         
  where open Related.EquationalReasoning

-- The list monad's bind is a congruence.

>>=-cong :  { k} {A B : Set } {xs₁ xs₂} {f₁ f₂ : A  List B} 
           xs₁ ∼[ k ] xs₂  (∀ x  f₁ x ∼[ k ] f₂ x) 
           (xs₁ >>= f₁) ∼[ k ] (xs₂ >>= f₂)
>>=-cong {} {xs₁ = xs₁} {xs₂} {f₁} {f₂} xs₁≈xs₂ f₁≈f₂ {x} =
  x  (xs₁ >>= f₁)          ↔⟨ sym $ >>=↔ { = } {p = } 
  Any  y  x  f₁ y) xs₁  ∼⟨ Any-cong  x  f₁≈f₂ x) xs₁≈xs₂ 
  Any  y  x  f₂ y) xs₂  ↔⟨ >>=↔ { = } {p = } 
  x  (xs₂ >>= f₂)          
  where open Related.EquationalReasoning

-- _⊛_ is a congruence.

⊛-cong :  { k} {A B : Set } {fs₁ fs₂ : List (A  B)} {xs₁ xs₂} 
         fs₁ ∼[ k ] fs₂  xs₁ ∼[ k ] xs₂ 
         (fs₁  xs₁) ∼[ k ] (fs₂  xs₂)
⊛-cong fs₁≈fs₂ xs₁≈xs₂ =
  >>=-cong fs₁≈fs₂ λ f 
  >>=-cong xs₁≈xs₂ λ x 
  _ 
  where open Related.EquationalReasoning

-- _⊗_ is a congruence.

⊗-cong :  { k} {A B : Set } {xs₁ xs₂ : List A} {ys₁ ys₂ : List B} 
         xs₁ ∼[ k ] xs₂  ys₁ ∼[ k ] ys₂ 
         (xs₁  ys₁) ∼[ k ] (xs₂  ys₂)
⊗-cong {} xs₁≈xs₂ ys₁≈ys₂ =
  ⊛-cong (⊛-cong (Ord.refl {x = [ _,_ {a = } {b = } ]})
                 xs₁≈xs₂)
         ys₁≈ys₂

------------------------------------------------------------------------
-- Other properties

-- _++_ and [] form a commutative monoid, with either bag or set
-- equality as the underlying equality.

commutativeMonoid :  {a}  Symmetric-kind  Set a 
                    CommutativeMonoid _ _
commutativeMonoid {a} k A = record
  { Carrier             = List A
  ; _≈_                 = λ xs ys  xs ∼[  k  ] ys
  ; _∙_                 = _++_
  ; ε                   = []
  ; isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = Eq.isEquivalence
      ; assoc         = λ xs ys zs 
                          Eq.reflexive (ListMonoid.assoc xs ys zs)
      ; ∙-cong        = ++-cong
      }
    ; identityˡ = λ xs {x}  x  xs 
    ; comm      = λ xs ys {x} 
                    x  xs ++ ys  ↔⟨ ++↔++ {a = a} {p = a} xs ys 
                    x  ys ++ xs  
    }
  }
  where open Related.EquationalReasoning

-- The only list which is bag or set equal to the empty list (or a
-- subset or subbag of the list) is the empty list itself.

empty-unique :  {k a} {A : Set a} {xs : List A} 
               xs ∼[  k ⌋→ ] []  xs  []
empty-unique {xs = []}    _    = P.refl
empty-unique {xs = _  _} ∷∼[] with ⇒→ ∷∼[] (here P.refl)
... | ()

-- _++_ is idempotent (under set equality).

++-idempotent :  {a} {A : Set a} 
                Idempotent  (xs ys : List A)  xs ∼[ set ] ys) _++_
++-idempotent {a} xs {x} =
  x  xs ++ xs  ∼⟨ FE.equivalence ([ id , id ]′  _⟨$⟩_ (Inverse.from $ ++↔ {a = a} {p = a}))
                                  (_⟨$⟩_ (Inverse.to $ ++↔ {a = a} {p = a})  inj₁) 
  x  xs        
  where open Related.EquationalReasoning

-- The list monad's bind distributes from the left over _++_.

>>=-left-distributive :
   {} {A B : Set } (xs : List A) {f g : A  List B} 
  (xs >>= λ x  f x ++ g x) ∼[ bag ] (xs >>= f) ++ (xs >>= g)
>>=-left-distributive {} xs {f} {g} {y} =
  y  (xs >>= λ x  f x ++ g x)                      ↔⟨ sym $ >>=↔ { = } {p = } 
  Any  x  y  f x ++ g x) xs                      ↔⟨ sym (Any-cong  _  ++↔ {a = } {p = }) (_ )) 
  Any  x  y  f x  y  g x) xs                   ↔⟨ sym $ ⊎↔ {a = } {p = } {q = } 
  (Any  x  y  f x) xs  Any  x  y  g x) xs)  ↔⟨ >>=↔ { = } {p = }  ×⊎.+-cong { = }  >>=↔ { = } {p = } 
  (y  (xs >>= f)  y  (xs >>= g))                  ↔⟨ ++↔ {a = } {p = } 
  y  (xs >>= f) ++ (xs >>= g)                       
  where open Related.EquationalReasoning

-- The same applies to _⊛_.

⊛-left-distributive :
   {} {A B : Set } (fs : List (A  B)) xs₁ xs₂ 
  (fs  (xs₁ ++ xs₂)) ∼[ bag ] (fs  xs₁) ++ (fs  xs₂)
⊛-left-distributive {B = B} fs xs₁ xs₂ = begin
  fs  (xs₁ ++ xs₂)                         ≡⟨ P.refl 
  (fs >>= λ f  xs₁ ++ xs₂ >>= return  f)  ≡⟨ (LP.Monad.cong (P.refl {x = fs}) λ f 
                                                LP.Monad.right-distributive xs₁ xs₂ (return  f)) 
  (fs >>= λ f  (xs₁ >>= return  f) ++
                (xs₂ >>= return  f))       ≈⟨ >>=-left-distributive fs 

  (fs >>= λ f  xs₁ >>= return  f) ++
  (fs >>= λ f  xs₂ >>= return  f)         ≡⟨ P.refl 

  (fs  xs₁) ++ (fs  xs₂)                  
  where open EqR ([ bag ]-Equality B)

private

  -- If x ∷ xs is set equal to x ∷ ys, then xs and ys are not
  -- necessarily set equal.

  ¬-drop-cons :
     {a} {A : Set a} {x : A} 
    ¬ (∀ {xs ys}  x  xs ∼[ set ] x  ys  xs ∼[ set ] ys)
  ¬-drop-cons {x = x} drop-cons
    with FE.Equivalence.to x∼[] ⟨$⟩ here P.refl
    where
    x,x≈x :  (x  x  []) ∼[ set ] [ x ]
    x,x≈x = ++-idempotent [ x ]

    x∼[] : [ x ] ∼[ set ] []
    x∼[] = drop-cons x,x≈x
  ... | ()

-- However, the corresponding property does hold for bag equality.

drop-cons :  {a} {A : Set a} {x : A} {xs ys} 
            x  xs ∼[ bag ] x  ys  xs ∼[ bag ] ys
drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys {z} = record
  { to         = P.→-to-⟶ $ f           x∷xs≈x∷ys
  ; from       = P.→-to-⟶ $ f $ Inv.sym x∷xs≈x∷ys
  ; inverse-of = record
    { left-inverse-of  = f∘f           x∷xs≈x∷ys
    ; right-inverse-of = f∘f $ Inv.sym x∷xs≈x∷ys
    }
  }
  where
  open Inverse
  open P.≡-Reasoning

  f :  {xs ys z}  (z  x  xs)  (z  x  ys)  z  xs  z  ys
  f inv z∈xs with to inv ⟨$⟩ there z∈xs | left-inverse-of inv (there z∈xs)
  f inv z∈xs | there z∈ys   | left⁺ = z∈ys
  f inv z∈xs | here  z≡x    | left⁺ with to inv ⟨$⟩ here z≡x | left-inverse-of inv (here z≡x)
  f inv z∈xs | here  z≡x    | left⁺ | there z∈ys   | left⁰ = z∈ys
  f inv z∈xs | here  P.refl | left⁺ | here  P.refl | left⁰ with begin
    here P.refl               ≡⟨ P.sym left⁰ 
    from inv ⟨$⟩ here P.refl  ≡⟨ left⁺ 
    there z∈xs                
  ... | ()

  f∘f :  {xs ys z}
        (inv : (z  x  xs)  (z  x  ys)) (p : z  xs) 
        f (Inv.sym inv) (f inv p)  p
  f∘f inv z∈xs with to inv ⟨$⟩ there z∈xs | left-inverse-of inv (there z∈xs)
  f∘f inv z∈xs | there z∈ys  | left⁺ with from inv ⟨$⟩ there z∈ys | right-inverse-of inv (there z∈ys)
  f∘f inv z∈xs | there z∈ys  | P.refl | .(there z∈xs) | _ = P.refl
  f∘f inv z∈xs | here z≡x    | left⁺ with to inv ⟨$⟩ here z≡x | left-inverse-of inv (here z≡x)
  f∘f inv z∈xs | here z≡x    | left⁺  | there z∈ys   | left⁰ with from inv ⟨$⟩ there z∈ys | right-inverse-of inv (there z∈ys)
  f∘f inv z∈xs | here z≡x    | left⁺  | there z∈ys   | P.refl | .(here z≡x) | _ with from inv ⟨$⟩ here z≡x
                                                                                   | right-inverse-of inv (here z≡x)
  f∘f inv z∈xs | here z≡x    | P.refl | there z∈ys   | P.refl | .(here z≡x) | _ | .(there z∈xs) | _ = P.refl
  f∘f inv z∈xs | here P.refl | left⁺  | here  P.refl | left⁰ with begin
    here P.refl               ≡⟨ P.sym left⁰ 
    from inv ⟨$⟩ here P.refl  ≡⟨ left⁺ 
    there z∈xs                
  ... | ()