----------------------------------------------------------------------------------------------------
-- Equivalence between Cantor Normal Forms and Finite Hereditary Multisets
----------------------------------------------------------------------------------------------------

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

module Interpretations.CnfEqFhm where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Everything using (iso; isoToEquiv; ua)
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥

open import CantorNormalForm.Everything as C
open import FiniteHereditaryMultiset.Everything as F

{- Cnf to Fhm -}

CtoF : Cnf → Fhm
CtoF 𝟎 = 𝟎
CtoF ω^ a + b [ _ ] = ω^ (CtoF a) ⊕ (CtoF b)


{- Fhm to Cnf -}

insert : Cnf → Cnf → Cnf
≥left-insert : {a b : Cnf} (c : Cnf) → b ≥ left c → a < b
             → b ≥ left (insert a c)
insert a 𝟎 = C.ω^⟨ a ⟩
insert a (ω^ b + c [ r ]) with <-tri a b
... | inl a<b = ω^ b + insert a c [ ≥left-insert c r a<b ]
... | inr a≥b = ω^ a + ω^ b + c [ r ] [ a≥b ]

≥left-insert 𝟎 _ a<b = inl a<b
≥left-insert {a} (ω^ c + d [ _ ]) b≥c a<b with <-tri a c
... | inl a<c = b≥c
... | inr a≥c = inl a<b

insert-swap : (x y z : Cnf)
            → insert x (insert y z) ≡ insert y (insert x z)
insert-swap x y 𝟎 with <-tri x y
insert-swap x y 𝟎 | inl x<y with <-tri y x
insert-swap x y 𝟎 | inl x<y | inl y<x = ⊥.rec (<→≯ x<y y<x)
insert-swap x y 𝟎 | inl x<y | inr y≥x = Cnf⁼ refl (Cnf⁼ refl refl)
insert-swap x y 𝟎 | inr x≥y with <-tri y x
insert-swap x y 𝟎 | inr x≥y | inl y<x = Cnf⁼ refl (Cnf⁼ refl refl)
insert-swap x y 𝟎 | inr x≥y | inr y≥x = Cnf⁼ (≤∧≥→≡ y≥x x≥y) (Cnf⁼ (≤∧≥→≡ x≥y y≥x) refl)
insert-swap x y (ω^ a + b [ _ ]) with <-tri y a
insert-swap x y (ω^ a + b [ _ ]) | inl y<a with <-tri x a
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inl x<a with <-tri y a
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inl x<a | inl y<a' = Cnf⁼ refl (insert-swap x y b)
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inl x<a | inr y≥a  = ⊥.rec (<→≱ y<a y≥a)
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inr x≥a with <-tri y x
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inr x≥a | inl y<x with <-tri y a
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inr x≥a | inl y<x | inl y<a' = Cnf⁼ refl (Cnf⁼ refl refl)
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inr x≥a | inl y<x | inr y≥a  = ⊥.rec (<→≱ y<a y≥a)
insert-swap x y (ω^ a + b [ _ ]) | inl y<a | inr x≥a | inr y≥x = ⊥.rec (<→≱ y<a (≤-trans x≥a y≥x))
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a with <-tri x a
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a with <-tri y a
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a | inl y<a  = ⊥.rec (<→≱ y<a y≥a)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a | inr y≥a' with <-tri x y
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a | inr y≥a' | inl x<y with <-tri x a
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a | inr y≥a' | inl x<y | inl x<a' = Cnf⁼ refl (Cnf⁼ refl refl)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a | inr y≥a' | inl x<y | inr x≥a  = ⊥.rec (<→≱ x<a x≥a)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inl x<a | inr y≥a' | inr x≥y = ⊥.rec (<→≱ x<a (≤-trans y≥a x≥y))
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a with <-tri x y
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inl x<y with <-tri x a
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inl x<y | inl x<a  = ⊥.rec (<→≱ x<a x≥a)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inl x<y | inr x≥a' with <-tri y x
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inl x<y | inr x≥a' | inl y<x = ⊥.rec (<→≱ x<y (inl y<x))
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inl x<y | inr x≥a' | inr y≥x = Cnf⁼ refl (Cnf⁼ refl refl)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inr x≥y with <-tri y x
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inr x≥y | inl y<x with <-tri y a
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inr x≥y | inl y<x | inl y<a  = ⊥.rec (<→≱ y<a y≥a)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inr x≥y | inl y<x | inr y≥a' = Cnf⁼ refl (Cnf⁼ refl refl)
insert-swap x y (ω^ a + b [ _ ]) | inr y≥a | inr x≥a | inr x≥y | inr y≥x = Cnf⁼ (≤∧≥→≡ y≥x x≥y) (Cnf⁼ (≤∧≥→≡ x≥y y≥x) refl)

FtoC : Fhm → Cnf
FtoC = F.rec Cnf-is-set 𝟎 insert insert-swap


{- Isomorphism between Cnf and Fhm -}

insert-+ : (a b : Cnf) (r : a ≥ left b)
         → insert a b ≡ ω^ a + b [ r ]
insert-+ a 𝟎 _ = Cnf⁼ refl refl
insert-+ a (ω^ b + c [ _ ]) a≥b with <-tri a b
... | inl a<b  = ⊥.rec (≤→≯ a≥b a<b)
... | inr a≥b' = Cnf⁼ refl (Cnf⁼ refl refl)

CtoFtoC≡id : (a : Cnf) → FtoC (CtoF a) ≡ a
CtoFtoC≡id 𝟎 = refl
CtoFtoC≡id (ω^ a + b [ r ]) =
  FtoC (CtoF (ω^ a + b [ r ])) ≡⟨ cong₂ insert (CtoFtoC≡id a) (CtoFtoC≡id b) ⟩
  insert a b ≡⟨ insert-+ a b r ⟩
  ω^ a + b [ r ] ∎

insert-⊕ : (a b : Cnf)
         → CtoF (insert a b) ≡ ω^ CtoF a ⊕ CtoF b
insert-⊕ a 𝟎 = refl
insert-⊕ a (ω^ b + c [ _ ]) with <-tri a b
... | inl a<b = cong (ω^ CtoF b ⊕_) (insert-⊕ a c) ∙ swap (CtoF b) (CtoF a) (CtoF c)
... | inr a≥b = refl

FtoCtoF≡id : (a : Fhm) → CtoF (FtoC a) ≡ a
FtoCtoF≡id = indProp (λ _ → trunc _ _) base step
 where
  base : CtoF (FtoC 𝟎) ≡ 𝟎
  base = refl
  step : ∀ x y → CtoF (FtoC x) ≡ x → CtoF (FtoC y) ≡ y
       → CtoF (FtoC (ω^ x ⊕ y)) ≡ ω^ x ⊕ y
  step x y px py =
    CtoF (FtoC (ω^ x ⊕ y)) ≡⟨ insert-⊕ (FtoC x) (FtoC y) ⟩
    ω^ (CtoF (FtoC x)) ⊕ (CtoF (FtoC y)) ≡⟨ cong₂ ω^_⊕_ px py ⟩
    ω^ x ⊕ y ∎

{- Equivalence and path between Cnf and Fhm -}

Cnf≃Fhm : Cnf ≃ Fhm
Cnf≃Fhm = isoToEquiv (iso CtoF FtoC FtoCtoF≡id CtoFtoC≡id)

Cnf≡Fhm : Cnf ≡ Fhm
Cnf≡Fhm = ua Cnf≃Fhm