{-# OPTIONS --safe #-}
module Cubical.HITs.AssocList.Properties where


open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP

open import Cubical.Relation.Nullary

open import Cubical.Structures.MultiSet

open import Cubical.Data.Nat   using (ℕ; zero; suc; _+_; +-assoc; isSetℕ)

open import Cubical.HITs.AssocList.Base as AL
open import Cubical.HITs.FiniteMultiset as FMS
  hiding (_++_; unitl-++; unitr-++; assoc-++; cons-++; comm-++)

private
  variable
    ℓ : Level
    A : Type ℓ



multiPer : (a b : A) (m n : ℕ) (xs : AssocList A)
          → ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs
multiPer a b zero n xs = del a (⟨ b , n ⟩∷ xs) ∙ cong (λ ys → ⟨ b , n ⟩∷ ys) (sym (del a xs))
multiPer a b (suc m) zero xs = cong (λ ys → ⟨ a , suc m ⟩∷ ys) (del b xs) ∙ sym (del b (⟨ a , suc m ⟩∷ xs))
multiPer a b (suc m) (suc n) xs =

 ⟨ a , suc m ⟩∷ ⟨ b , suc n ⟩∷ xs               ≡⟨ sym (agg a  m (⟨ b , suc n ⟩∷ xs)) ⟩
 ⟨ a ,  ⟩∷ ⟨ a , m ⟩∷ ⟨ b , suc n ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ a ,  ⟩∷ ys) (multiPer a b m (suc n) xs) ⟩
 ⟨ a ,  ⟩∷ ⟨ b , suc n ⟩∷ ⟨ a , m ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ a ,  ⟩∷ ys) (sym (agg b  n (⟨ a , m ⟩∷ xs))) ⟩
 ⟨ a ,  ⟩∷ ⟨ b ,  ⟩∷ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs ≡⟨ per a b (⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs) ⟩
 ⟨ b ,  ⟩∷ ⟨ a ,  ⟩∷ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs ≡⟨ cong (λ ys → ⟨ b ,  ⟩∷ ⟨ a ,  ⟩∷ ys) (multiPer b a n m xs) ⟩
 ⟨ b ,  ⟩∷ ⟨ a ,  ⟩∷ ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡⟨ cong (λ ys → ⟨ b ,  ⟩∷ ys) (agg a  m (⟨ b , n ⟩∷ xs)) ⟩
 ⟨ b ,  ⟩∷ ⟨ a , suc m ⟩∷ ⟨ b , n ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ b ,  ⟩∷ ys) (multiPer a b (suc m) n xs) ⟩
 ⟨ b ,  ⟩∷ ⟨ b , n ⟩∷ ⟨ a , suc m ⟩∷ xs        ≡⟨ agg b  n (⟨ a , suc m ⟩∷ xs) ⟩
 ⟨ b , suc n ⟩∷ ⟨ a , suc m ⟩∷ xs               ∎





-- Show that association lists and finite multisets are equivalent
multi-∷ : A → ℕ → FMSet A → FMSet A
multi-∷ x zero xs = xs
multi-∷ x (suc n) xs = x ∷ multi-∷ x n xs

multi-∷-agg : (x : A) (m n : ℕ) (b : FMSet A) → multi-∷ x m (multi-∷ x n b) ≡ multi-∷ x (m + n) b
multi-∷-agg x zero n b = refl
multi-∷-agg x (suc m) n b i = x ∷ (multi-∷-agg x m n b i)


infixr  _++_

_++_ : (xs ys : AssocList A) → AssocList A
⟨⟩ ++ ys = ys
(⟨ a , n ⟩∷ xs) ++ ys = ⟨ a , n ⟩∷ (xs ++ ys)
per a b xs i ++ ys = per a b (xs ++ ys) i
agg a m n xs i ++ ys = agg a m n (xs ++ ys) i
del a xs i ++ ys = del a (xs ++ ys) i
trunc xs ys p q i j ++ zs =
  trunc (xs ++ zs) (ys ++ zs) (cong (_++ _) p) (cong (_++ _) q) i j

unitl-++ : (xs : AssocList A) → ⟨⟩ ++ xs ≡ xs
unitl-++ xs = refl

unitr-++ : (xs : AssocList A) → xs ++ ⟨⟩ ≡ xs
unitr-++ = AL.ElimProp.f (trunc _ _) refl λ _ _ → cong (⟨ _ , _ ⟩∷_)

assoc-++ : (xs ys zs : AssocList A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ = AL.ElimProp.f (isPropΠ2 (λ _ _ → trunc _ _))
                      (λ ys zs → refl)
                      λ x n p ys zs → cong (⟨ _ , _ ⟩∷_) (p ys zs)

cons-++ : ∀ x n (xs : AssocList A) → ⟨ x , n ⟩∷ xs ≡ xs ++ (⟨ x , n ⟩∷ ⟨⟩)
cons-++ x n = AL.ElimProp.f (trunc _ _) refl
  λ y m p → multiPer _ _ _ _ _ ∙ cong (⟨ _ , _ ⟩∷_) p

comm-++ : (xs ys : AssocList A) → xs ++ ys ≡ ys ++ xs
comm-++ = AL.ElimProp.f (isPropΠ (λ _ → trunc _ _))
  (sym ∘ unitr-++)
  λ x n {xs} p ys → cong (⟨ _ , _ ⟩∷_) (p ys)
                  ∙ cong (_++ _) (cons-++ x n ys)
                  ∙ sym (assoc-++ ys _ xs)


AL→FMS : AssocList A → FMSet A
AL→FMS = AL.Rec.f FMS.trunc [] multi-∷ comm multi-∷-agg λ _ _ → refl


FMS→AL : FMSet A → AssocList A
FMS→AL = FMS.Rec.f AL.trunc ⟨⟩ (λ x xs → ⟨ x ,  ⟩∷ xs) per



AL→FMS∘FMS→AL≡id : section {A = AssocList A} AL→FMS FMS→AL
AL→FMS∘FMS→AL≡id = FMS.ElimProp.f (FMS.trunc _ _) refl (λ x p → cong (λ ys → x ∷ ys) p)


-- need a little lemma for other direction
multi-∷-id : (x : A) (n : ℕ) (u : FMSet A)
            → FMS→AL (multi-∷ x n u) ≡ ⟨ x , n ⟩∷ FMS→AL u
multi-∷-id x zero u = sym (del x (FMS→AL u))
multi-∷-id x (suc n) u = FMS→AL (multi-∷ x (suc n) u)     ≡⟨ cong (λ ys → ⟨ x ,  ⟩∷ ys) (multi-∷-id x n u) ⟩
                         ⟨ x ,  ⟩∷ ⟨ x , n ⟩∷ (FMS→AL u) ≡⟨ agg x  n (FMS→AL u) ⟩
                         ⟨ x , (suc n) ⟩∷ (FMS→AL u)      ∎

FMS→AL∘AL→FMS≡id : retract {A = AssocList A} AL→FMS FMS→AL
FMS→AL∘AL→FMS≡id = AL.ElimProp.f (AL.trunc _ _) refl (λ x n {xs} p → (multi-∷-id x n (AL→FMS xs)) ∙ cong (λ ys → ⟨ x , n ⟩∷ ys) p)




AssocList≃FMSet : AssocList A ≃ FMSet A
AssocList≃FMSet = isoToEquiv (iso AL→FMS FMS→AL AL→FMS∘FMS→AL≡id FMS→AL∘AL→FMS≡id)

FMSet≃AssocList : FMSet A ≃ AssocList A
FMSet≃AssocList = isoToEquiv (iso FMS→AL AL→FMS FMS→AL∘AL→FMS≡id AL→FMS∘FMS→AL≡id)


AssocList≡FMSet : AssocList A ≡ FMSet A
AssocList≡FMSet = ua AssocList≃FMSet




-- We want to define a multiset structure on AssocList A, we use the recursor to define the count-function


module _(discA : Discrete A) where
 setA = Discrete→isSet discA



 ALcount-⟨,⟩∷* : A → A → ℕ → ℕ → ℕ
 ALcount-⟨,⟩∷* a x n xs with discA a x
 ... | yes a≡x = n + xs
 ... | no  a≢x = xs


 ALcount-per* :  (a x y : A) (xs : ℕ)
                →  ALcount-⟨,⟩∷* a x  (ALcount-⟨,⟩∷* a y  xs)
                 ≡ ALcount-⟨,⟩∷* a y  (ALcount-⟨,⟩∷* a x  xs)
 ALcount-per* a x y xs with discA a x | discA a y
 ALcount-per* a x y xs | yes a≡x | yes a≡y = refl
 ALcount-per* a x y xs | yes a≡x | no  a≢y = refl
 ALcount-per* a x y xs | no  a≢x | yes a≡y = refl
 ALcount-per* a x y xs | no  a≢x | no  a≢y = refl


 ALcount-agg* :  (a x : A) (m n xs : ℕ)
                →  ALcount-⟨,⟩∷* a x m (ALcount-⟨,⟩∷* a x n xs)
                 ≡ ALcount-⟨,⟩∷* a x (m + n) xs
 ALcount-agg* a x m n xs with discA a x
 ... | yes _ = +-assoc m n xs
 ... | no  _ = refl

 ALcount-del* :  (a x : A) (xs : ℕ) → ALcount-⟨,⟩∷* a x  xs ≡ xs
 ALcount-del* a x xs with discA a x
 ... | yes _ = refl
 ... | no  _ = refl


 ALcount : A → AssocList A → ℕ
 ALcount a = AL.Rec.f isSetℕ  (ALcount-⟨,⟩∷* a) (ALcount-per* a) (ALcount-agg* a) (ALcount-del* a)



 AL-with-str : MultiSet A setA
 AL-with-str = (AssocList A , ⟨⟩ , ⟨_,  ⟩∷_ , ALcount)


-- We want to show that Al-with-str ≅ FMS-with-str as multiset-structures
 FMS→AL-EquivStr : MultiSetEquivStr A setA (FMS-with-str discA) (AL-with-str) FMSet≃AssocList
 FMS→AL-EquivStr = refl , (λ a xs → refl) , φ
  where
  φ : ∀ a xs → FMScount discA a xs ≡ ALcount a (FMS→AL xs)
  φ a = FMS.ElimProp.f (isSetℕ _ _) refl ψ
   where
   ψ :  (x : A) {xs : FMSet A}
      → FMScount discA a xs ≡ ALcount a (FMS→AL xs)
      → FMScount discA a (x ∷ xs) ≡ ALcount a (FMS→AL (x ∷ xs))
   ψ x {xs} p = subst B α θ
    where
    B = λ ys → FMScount discA a (x ∷ xs) ≡ ALcount a ys

    α : ⟨ x ,  ⟩∷ FMS→AL xs ≡ FMS→AL (x ∷ xs)
    α = sym (multi-∷-id x  xs)

    θ : FMScount discA a (x ∷ xs) ≡ ALcount a (⟨ x ,  ⟩∷ (FMS→AL xs))
    θ with discA a x
    ... | yes _ = cong suc p
    ... | no ¬p = p



 FMS-with-str≡AL-with-str : FMS-with-str discA ≡ AL-with-str
 FMS-with-str≡AL-with-str = sip (multiSetUnivalentStr A setA)
                                (FMS-with-str discA) AL-with-str
                                (FMSet≃AssocList , FMS→AL-EquivStr)