module Cubical.Structures.Set.CMon.Bag.ToCList where
open import Cubical.Structures.Prelude
import Cubical.Data.Empty as ⊥
open import Cubical.Data.Fin
open import Cubical.Data.List renaming (_∷_ to _∷ₗ_)
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎
import Cubical.Structures.Set.Mon.Desc as M
import Cubical.Structures.Set.CMon.Desc as M
import Cubical.Structures.Free as F
open import Cubical.Structures.Set.Mon.Array as A
open import Cubical.Structures.Set.Mon.List as L
open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq
open import Cubical.Structures.Arity hiding (_/_)
open import Cubical.Structures.Set.CMon.QFreeMon
open import Cubical.Structures.Set.CMon.CList
open import Cubical.Structures.Set.CMon.Bag.Base
open import Cubical.Structures.Set.CMon.Bag.Free
open import Cubical.Relation.Nullary
open import Cubical.Data.Fin.LehmerCode hiding (LehmerCode; _∷_; [])
open import Cubical.Structures.Set.CMon.Bag.FinExcept
open Iso
private
variable
ℓ ℓ' ℓ'' : Level
A : Type ℓ
n : ℕ
module IsoToCList {ℓ} (A : Type ℓ) where
open import Cubical.Structures.Set.CMon.CList as CL
open import Cubical.HITs.SetQuotients as Q
open BagDef.Free
module 𝔄 = M.MonSEq < Array A , arrayA > arraySat
module 𝔅 = M.CMonSEq < Bag A , bagFreeDef .α > (bagFreeDef .sat)
module ℭ = M.CMonSEq < CList A , clistAlpha > clistSat
abstract
fromCListHom : structHom < CList A , clistAlpha > < Bag A , bagFreeDef .α >
fromCListHom = ext clistDef squash/ (bagFreeDef .sat) (BagDef.Free.η bagFreeDef)
fromCList : CList A -> Bag A
fromCList = fromCListHom .fst
fromCListIsHom : structIsHom < CList A , clistAlpha > < Bag A , bagFreeDef .α > fromCList
fromCListIsHom = fromCListHom .snd
fromCListE : fromCList [] ≡ 𝔅.e
fromCListE = refl
fromCListConcat : ∀ xs ys -> fromCList (xs ℭ.⊕ ys) ≡ fromCList xs 𝔅.⊕ fromCList ys
fromCListConcat xs ys =
fromCList (xs ℭ.⊕ ys) ≡⟨ sym (fromCListIsHom M.`⊕ ⟪ xs ⨾ ys ⟫) ⟩
_ ≡⟨ 𝔅.⊕Eta ⟪ xs ⨾ ys ⟫ fromCList ⟩
_ ∎
fromCListEta : ∀ x -> fromCList (CL.[ x ]) ≡ Q.[ A.η x ]
fromCListEta x = congS (λ f -> f x)
(ext-η clistDef squash/ (bagFreeDef .sat) (BagDef.Free.η bagFreeDef))
ListToCListHom : structHom < List A , listΑ > < CList A , clistAlpha >
ListToCListHom = ListDef.Free.ext listDef isSetCList (M.cmonSatMon clistSat) CL.[_]
ListToCList : List A -> CList A
ListToCList = ListToCListHom .fst
ArrayToCListHom : structHom < Array A , arrayA > < CList A , clistAlpha >
ArrayToCListHom = structHom∘ < Array A , arrayA > < List A , listΑ > < CList A , clistAlpha >
ListToCListHom ((arrayIsoToList .fun) , arrayIsoToListHom)
ArrayToCList : Array A -> CList A
ArrayToCList = ArrayToCListHom .fst
tab : ∀ n -> (Fin n -> A) -> CList A
tab = curry ArrayToCList
isContr≅ : ∀ {ℓ} {A : Type ℓ} -> isContr A -> isContr (Iso A A)
isContr≅ ϕ = inhProp→isContr idIso \σ1 σ2 ->
SetsIso≡ (isContr→isOfHLevel 2 ϕ) (isContr→isOfHLevel 2 ϕ)
(funExt \x -> isContr→isProp ϕ (σ1 .fun x) (σ2 .fun x))
(funExt \x -> isContr→isProp ϕ (σ1 .inv x) (σ2 .inv x))
isContrFin1≅ : isContr (Iso (Fin 1) (Fin 1))
isContrFin1≅ = isContr≅ isContrFin1
fsuc∘punchOutZero≡ : ∀ {n}
-> (f g : Fin (suc (suc n)) -> A)
-> (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n)))) (p : f ≡ g ∘ σ .fun)
-> (q : σ .fun fzero ≡ fzero)
-> f ∘ fsuc ≡ g ∘ fsuc ∘ punchOutZero σ q .fun
fsuc∘punchOutZero≡ f g σ p q =
f ∘ fsuc ≡⟨ congS (_∘ fsuc) p ⟩
g ∘ σ .fun ∘ fsuc ≡⟨ congS (g ∘_) (funExt (punchOutZero≡fsuc σ q)) ⟩
g ∘ fsuc ∘ punchOutZero σ q .fun ∎
toCListEq : ∀ n
-> (f : Fin n -> A) (g : Fin n -> A) (σ : Iso (Fin n) (Fin n)) (p : f ≡ g ∘ σ .fun)
-> tab n f ≡ tab n g
toCListEq zero f g σ p =
refl
toCListEq (suc zero) f g σ p =
let q : σ ≡ idIso
q = isContr→isProp isContrFin1≅ σ idIso
in congS (tab 1) (p ∙ congS (g ∘_) (congS Iso.fun q))
toCListEq (suc (suc n)) f g σ p =
⊎.rec
(λ 0≡σ0 ->
let IH = toCListEq (suc n) (f ∘ fsuc) (g ∘ fsuc) (punchOutZero σ (sym 0≡σ0)) (fsuc∘punchOutZero≡ f g σ p (sym 0≡σ0))
in case1 IH (sym 0≡σ0)
)
(λ (k , Sk≡σ0) ->
case2 k (sym Sk≡σ0)
(toCListEq (suc n) (f ∘ fsuc) ((g ∼) ∘ pIn (fsuc k)) (punchΣ σ) (sym (IH1-lemma k Sk≡σ0)))
(toCListEq (suc n) (g-σ k) (g ∘ fsuc) (fillΣ k) (sym (funExt (IH2-lemma k Sk≡σ0))))
)
(fsplit (σ .fun fzero))
where
g-σ : ∀ k -> Fin (suc n) -> A
g-σ k (zero , p) = g (σ .fun fzero)
g-σ k (suc j , p) = (g ∼) (1+ (pIn k (j , predℕ-≤-predℕ p)))
IH1-lemma : ∀ k -> fsuc k ≡ σ .fun fzero -> (g ∼) ∘ pIn (fsuc k) ∘ punchΣ σ .fun ≡ f ∘ fsuc
IH1-lemma k Sk≡σ0 =
(g ∼) ∘ pIn (fsuc k) ∘ punchΣ σ .fun
≡⟨ congS (λ z -> (g ∼) ∘ pIn z ∘ punchΣ σ .fun) Sk≡σ0 ⟩
(g ∼) ∘ pIn (σ .fun fzero) ∘ punchΣ σ .fun
≡⟨⟩
(g ∼) ∘ pIn (σ .fun fzero) ∘ pOut (σ .fun fzero) ∘ ((G .fun σ) .snd) .fun ∘ pIn fzero
≡⟨ congS (λ h -> (g ∼) ∘ h ∘ ((G .fun σ) .snd) .fun ∘ (invIso pIso) .fun) (funExt (pInOut (σ .fun fzero))) ⟩
(g ∼) ∘ equivIn σ .fun ∘ pIn fzero
≡⟨⟩
g ∘ σ .fun ∘ fst ∘ pIn fzero
≡⟨ congS (_∘ fst ∘ pIn fzero) (sym p) ⟩
f ∘ fst ∘ pIn fzero
≡⟨ congS (f ∘_) (funExt pInZ≡fsuc) ⟩
f ∘ fsuc ∎
IH2-lemma : ∀ k -> fsuc k ≡ σ .fun fzero -> (j : Fin (suc n)) -> g (fsuc (fillΣ k .fun j)) ≡ (g-σ k) j
IH2-lemma k Sk≡σ0 (zero , r) = congS g Sk≡σ0
IH2-lemma k Sk≡σ0 (suc j , r) =
g (fsuc (equivOut {k = k} (compIso pIso (invIso pIso)) .fun (suc j , r)))
≡⟨⟩
g (fsuc (equivOut {k = k} (compIso pIso (invIso pIso)) .fun (j' .fst)))
≡⟨ congS (g ∘ fsuc) (equivOutBetaΑ {σ = compIso pIso (invIso pIso)} j') ⟩
g (fsuc (fst (pIn k (pOut fzero j'))))
≡⟨⟩
g (fsuc (fst (pIn k (⊎.rec _ (λ k<j -> predℕ (suc j) , _) (suc j <? 0 on _)))))
≡⟨ congS (g ∘ fsuc ∘ fst ∘ pIn k ∘ ⊎.rec _ _) (<?BetaInr (suc j) 0 _ (suc-≤-suc zero-≤)) ⟩
(g ∘ fsuc ∘ fst ∘ pIn k) (predℕ (suc j) , _)
≡⟨ congS {x = predℕ (suc j) , _} {y = j , predℕ-≤-predℕ r} (g ∘ fsuc ∘ fst ∘ pIn k) (Fin-fst-≡ refl) ⟩
(g ∘ fsuc ∘ fst ∘ pIn k) (j , predℕ-≤-predℕ r) ∎
where
j' : FinExcept fzero
j' = (suc j , r) , znots ∘ (congS fst)
case1 : (tab (suc n) (f ∘ fsuc) ≡ tab (suc n) (g ∘ fsuc))
-> σ .fun fzero ≡ fzero
-> tab (suc (suc n)) f ≡ tab (suc (suc n)) g
case1 IH σ0≡0 =
tab (suc (suc n)) f ≡⟨⟩
f fzero ∷ tab (suc n) (f ∘ fsuc) ≡⟨ congS (_∷ tab (suc n) (f ∘ fsuc)) (funExt⁻ p fzero) ⟩
g (σ .fun fzero) ∷ tab (suc n) (f ∘ fsuc) ≡⟨ congS (\k -> g k ∷ tab (suc n) (f ∘ fsuc)) σ0≡0 ⟩
g fzero ∷ tab (suc n) (f ∘ fsuc) ≡⟨ congS (g fzero ∷_) IH ⟩
g fzero ∷ tab (suc n) (g ∘ fsuc) ≡⟨⟩
tab (suc (suc n)) g ∎
case2 : (k : Fin (suc n))
-> σ .fun fzero ≡ fsuc k
-> tab (suc n) (f ∘ fsuc) ≡ tab (suc n) ((g ∼) ∘ pIn (fsuc k))
-> tab (suc n) (g-σ k) ≡ tab (suc n) (g ∘ fsuc)
-> tab (suc (suc n)) f ≡ tab (suc (suc n)) g
case2 k σ0≡Sk IH1 IH2 =
comm (f fzero) (g fzero) (tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc))
(sym (eqn1 IH1)) (sym (eqn2 IH2))
where
eqn1 : tab (suc n) (f ∘ fsuc) ≡ tab (suc n) ((g ∼) ∘ pIn (fsuc k))
-> g fzero ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc) ≡ tab (suc n) (f ∘ fsuc)
eqn1 IH =
g fzero ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc)
≡⟨ congS (λ z -> g z ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc)) (Fin-fst-≡ refl) ⟩
((g ∼) ∘ pIn (fsuc k)) fzero ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc)
≡⟨⟩
tab (suc n) ((g ∼) ∘ pIn (fsuc k))
≡⟨ sym IH ⟩
tab (suc n) (f ∘ fsuc) ∎
g-σ≡ : tab (suc n) (g-σ k) ≡ g (σ .fun fzero) ∷ tab n ((g ∼) ∘ 1+_ ∘ pIn k)
g-σ≡ = congS (λ z -> g (σ .fun fzero) ∷ tab n z)
(funExt λ z -> congS {x = (fst z , pred-≤-pred (snd (fsuc z)))} ((g ∼) ∘ 1+_ ∘ pIn k) (Fin-fst-≡ refl))
eqn2 : tab (suc n) (g-σ k) ≡ tab (suc n) (g ∘ fsuc)
-> f fzero ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc) ≡ tab (suc n) (g ∘ fsuc)
eqn2 IH2 =
f fzero ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc)
≡⟨ congS (λ h -> h fzero ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc)) p ⟩
g (σ .fun fzero) ∷ tab n ((g ∼) ∘ pIn (fsuc k) ∘ fsuc)
≡⟨ congS (λ h -> g (σ .fun fzero) ∷ tab n ((g ∼) ∘ h)) (sym pInFsucNat) ⟩
g (σ .fun fzero) ∷ tab n ((g ∼) ∘ 1+_ ∘ pIn k)
≡⟨ sym g-σ≡ ⟩
tab (suc n) (g-σ k)
≡⟨ IH2 ⟩
tab (suc n) (g ∘ fsuc) ∎
abstract
toCListEq' : ∀ n m f g -> (r : (n , f) ≈ (m , g)) -> tab n f ≡ tab m g
toCListEq' n m f g (σ , p) =
tab n f ≡⟨ toCListEq n f (g ∘ (finSubst n≡m)) (compIso σ (Fin≅ (sym n≡m))) (sym lemma-α) ⟩
(uncurry tab) (n , g ∘ finSubst n≡m) ≡⟨ congS (uncurry tab) (Array≡ n≡m λ _ _ -> congS g (Fin-fst-≡ refl)) ⟩
(uncurry tab) (m , g) ∎
where
n≡m : n ≡ m
n≡m = ≈-length σ
lemma-α : g ∘ finSubst n≡m ∘ (Fin≅ (sym n≡m)) .fun ∘ σ .fun ≡ f
lemma-α =
g ∘ finSubst n≡m ∘ finSubst (sym n≡m) ∘ σ .fun
≡⟨ congS {x = finSubst n≡m ∘ finSubst (sym n≡m)} {y = idfun _} (λ h -> g ∘ h ∘ σ .fun) (funExt (λ x -> Fin-fst-≡ refl)) ⟩
g ∘ σ .fun
≡⟨ sym p ⟩
f ∎
abstract
toCList : Bag A -> CList A
toCList Q.[ (n , f) ] = tab n f
toCList (eq/ (n , f) (m , g) r i) = toCListEq' n m f g r i
toCList (squash/ xs ys p q i j) =
isSetCList (toCList xs) (toCList ys) (congS toCList p) (congS toCList q) i j
toCListEta : (xs : Array A) -> toCList Q.[ xs ] ≡ ArrayToCList xs
toCListEta xs = refl
toCListE : toCList 𝔅.e ≡ CL.[]
toCListE = refl
toCListConcat : ∀ xs ys -> toCList (xs 𝔅.⊕ ys) ≡ toCList xs ℭ.⊕ toCList ys
toCListConcat =
elimProp (λ _ -> isPropΠ (λ _ -> isSetCList _ _)) λ xs ->
elimProp (λ _ -> isSetCList _ _) λ ys ->
sym (ArrayToCListHom .snd M.`⊕ ⟪ xs ⨾ ys ⟫)
toCListFromCListEta : ∀ x -> toCList (fromCList CL.[ x ]) ≡ CL.[ x ]
toCListFromCListEta x = refl
fromCListToCListEta : ∀ x -> fromCList (toCList Q.[ A.η x ]) ≡ Q.[ A.η x ]
fromCListToCListEta x = fromCListEta x
toCListFromCList : ∀ xs -> toCList (fromCList xs) ≡ xs
toCListFromCList =
elimCListProp.f _
(congS toCList fromCListE ∙ toCListE)
(λ x {xs} p ->
toCList (fromCList (x ∷ xs)) ≡⟨ congS toCList (fromCListConcat CL.[ x ] xs) ⟩
toCList (fromCList CL.[ x ] 𝔅.⊕ fromCList xs) ≡⟨ toCListConcat (fromCList CL.[ x ]) (fromCList xs) ⟩
toCList (fromCList CL.[ x ]) ℭ.⊕ toCList (fromCList xs) ≡⟨ congS (toCList (fromCList CL.[ x ]) ℭ.⊕_) p ⟩
toCList (fromCList CL.[ x ]) ℭ.⊕ xs ≡⟨ congS {x = toCList (fromCList CL.[ x ])} {y = CL.[ x ]} (ℭ._⊕ xs) (toCListFromCListEta x) ⟩
CL.[ x ] ℭ.⊕ xs
∎)
(isSetCList _ _)
fromListToCList : ∀ xs -> fromCList (toCList xs) ≡ xs
fromListToCList = elimProp (λ _ -> squash/ _ _) (uncurry lemma)
where
lemma : (n : ℕ) (f : Fin n -> A) -> fromCList (toCList Q.[ n , f ]) ≡ Q.[ n , f ]
lemma zero f =
fromCList (toCList Q.[ zero , f ]) ≡⟨ congS fromCList (toCListEta (zero , f)) ⟩
fromCList [] ≡⟨ fromCListE ⟩
𝔅.e ≡⟨ congS Q.[_] (eEta _ (zero , f) refl refl) ⟩
Q.[ zero , f ] ∎
lemma (suc n) f =
fromCList (toCList Q.[ suc n , f ])
≡⟨ congS fromCList (toCListEta (suc n , f)) ⟩
fromCList (ArrayToCList (suc n , f))
≡⟨ congS (fromCList ∘ ArrayToCList) (sym (η+fsuc f)) ⟩
fromCList (ArrayToCList (A.η (f fzero) ⊕ (n , f ∘ fsuc)))
≡⟨ congS fromCList $ sym (ArrayToCListHom .snd M.`⊕ ⟪ A.η (f fzero) ⨾ (n , f ∘ fsuc) ⟫) ⟩
fromCList (f fzero ∷ ArrayToCList (n , f ∘ fsuc))
≡⟨ fromCListConcat CL.[ f fzero ] (ArrayToCList (n , f ∘ fsuc)) ⟩
fromCList CL.[ f fzero ] 𝔅.⊕ fromCList (ArrayToCList (n , f ∘ fsuc))
≡⟨ congS (𝔅._⊕ fromCList (ArrayToCList (n , f ∘ fsuc))) (fromCListEta (f fzero)) ⟩
Q.[ A.η (f fzero) ] 𝔅.⊕ fromCList (ArrayToCList (n , f ∘ fsuc))
≡⟨ congS (λ zs -> Q.[ A.η (f fzero) ] 𝔅.⊕ fromCList zs) (sym (toCListEta (n , f ∘ fsuc))) ⟩
Q.[ A.η (f fzero) ] 𝔅.⊕ fromCList (toCList Q.[ n , f ∘ fsuc ])
≡⟨ congS (Q.[ A.η (f fzero) ] 𝔅.⊕_) (lemma n (f ∘ fsuc)) ⟩
Q.[ A.η (f fzero) ] 𝔅.⊕ Q.[ n , f ∘ fsuc ]
≡⟨ QFreeMon.[ A ]IsMonHom (PermRel A) .snd M.`⊕ ⟪ _ ⨾ _ ⟫ ⟩
Q.[ A.η (f fzero) 𝔄.⊕ (n , f ∘ fsuc) ]
≡⟨ congS Q.[_] (η+fsuc f) ⟩
Q.[ suc n , f ] ∎
BagToCList : Iso (Bag A) (CList A)
BagToCList = iso toCList fromCList toCListFromCList fromListToCList
bagDef' : ∀ {ℓ ℓ'} -> BagDef.Free ℓ ℓ' 2
bagDef' {ℓ = ℓ} {ℓ' = ℓ'} = BagDef.isoAux .fun (Bag , bagFreeAux)
where
clistFreeAux : BagDef.FreeAux ℓ ℓ' 2 CList
clistFreeAux = (inv BagDef.isoAux clistDef) .snd
bagFreeAux : BagDef.FreeAux ℓ ℓ' 2 Bag
bagFreeAux = subst (BagDef.FreeAux ℓ ℓ' 2)
(funExt λ X -> isoToPath $ invIso (IsoToCList.BagToCList X)) clistFreeAux