nbe-for-monoid.agda

{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything

refl₍_₎ : {A : Set} (x : A) → x ≡ x
refl₍ x ₎ = λ i → x

refl : {A : Set} {x : A} → x ≡ x
refl = refl₍ _ ₎

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym p = λ i → p (~ i)

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans {x = x} p q = λ i → hcomp (λ j → λ { (i = i0) → x
                                         ; (i = i1) → q j })
                                (p i)

cong : {A B : Set} (f : A → B) → ∀ {x y} → x ≡ y → f x ≡ f y
cong f p i = f (p i)

infixl 4 _<$>_
infixl 4 _<*>_

_<$>_ = cong

_<*>_ : {A B : Set} {f g : A → B} → f ≡ g → ∀ {x y} → x ≡ y → f x ≡ g y
p <*> q = λ i → p i (q i)

module ≡-Reasoning where
  infix  1 begin_
  infixr 2 _≡⟨_⟩_
  infix  3 _∎

  begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
  begin p = p

  _≡⟨_⟩_ : {A : Set} (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
    → x ≡ z
  x ≡⟨ p ⟩ q = trans p q

  _∎ : {A : Set} (x : A) → x ≡ x
  x ∎ = refl

open ≡-Reasoning

is-prop : Set → Set
is-prop A = (x y : A) → x ≡ y

is-set : Set → Set
is-set A = {x y : A} (p q : x ≡ y) → p ≡ q

module _ {A : Set} (A-is-set : is-set A) where
infixr 5 _∙_
data Monoid (A : Set) : Set where
  ⟨_⟩ : A → Monoid A
  _∙_ : Monoid A → Monoid A → Monoid A
  ε   : Monoid A

  ∙-unitˡ : ∀ xs → ε ∙ xs ≡ xs
  ∙-unitʳ : ∀ xs → xs ∙ ε ≡ xs
  ∙-assoc : ∀ xs ys zs → (xs ∙ ys) ∙ zs ≡ xs ∙ (ys ∙ zs)
  squash  : is-set (Monoid A)

infixr 5 _∷_
data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 5 _++_
_++_ : {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

++-unitˡ : {A : Set} (xs : List A) → [] ++ xs ≡ xs
++-unitˡ xs = refl

++-unitʳ : {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-unitʳ []       = refl
++-unitʳ (x ∷ xs) = cong (x ∷_) (++-unitʳ xs)

++-assoc : {A : Set} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc []       ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (x ∷_) (++-assoc xs ys zs)

postulate
  list-is-set : {A : Set} → is-set (List A)

-- ⟦_⟧ is the normalization function
⟦_⟧ : {A : Set} → Monoid A → List A
⟦ ⟨ x ⟩   ⟧ = x ∷ []
⟦ xs ∙ ys ⟧ = ⟦ xs ⟧ ++ ⟦ ys ⟧
⟦ ε       ⟧ = []
⟦ ∙-unitˡ xs i       ⟧ = ++-unitˡ ⟦ xs ⟧ i
⟦ ∙-unitʳ xs i       ⟧ = ++-unitʳ ⟦ xs ⟧ i
⟦ ∙-assoc xs ys zs i ⟧ = ++-assoc ⟦ xs ⟧ ⟦ ys ⟧ ⟦ zs ⟧ i
⟦ squash  p  q  i  j ⟧ = {!!} -- list-is-set (cong ⟦_⟧ p) (cong ⟦_⟧ q) i j

-- ⌜_⌝ is the embedding of normal forms into regular terms
⌜_⌝ : {A : Set} → List A → Monoid A
⌜ []     ⌝ = ε
⌜ x ∷ xs ⌝ = ⟨ x ⟩ ∙ ⌜ xs ⌝

⌜⌝-resp-++ : {A : Set} (xs ys : List A) → ⌜ xs ++ ys ⌝ ≡ ⌜ xs ⌝ ∙ ⌜ ys ⌝
⌜⌝-resp-++ []       ys = sym (∙-unitˡ ⌜ ys ⌝)
⌜⌝-resp-++ (x ∷ xs) ys = begin
  ⟨ x ⟩ ∙ ⌜ xs ++ ys ⌝  ≡⟨ cong (⟨ x ⟩ ∙_) (⌜⌝-resp-++ _ _) ⟩
  ⟨ x ⟩ ∙ (⌜ xs ⌝ ∙ ⌜ ys ⌝)  ≡⟨ sym (∙-assoc _ _ _ ) ⟩
  (⟨ x ⟩ ∙ ⌜ xs ⌝) ∙ ⌜ ys ⌝  ∎

-- soundness is already done when we spell out the definition of ⟦_⟧
soundness : {A : Set} (xs ys : Monoid A) → xs ≡ ys → ⟦ xs ⟧ ≡ ⟦ ys ⟧
soundness _ _ p = cong ⟦_⟧ p

stability : {A : Set} (xs : List A) → ⟦ ⌜ xs ⌝ ⟧ ≡ xs
stability []       = refl
stability (x ∷ xs) = cong (x ∷_) (stability xs)

completeness : {A : Set} (xs : Monoid A) → ⌜ ⟦ xs ⟧ ⌝ ≡ xs
completeness ⟨ x ⟩     = ∙-unitʳ ⟨ x ⟩
completeness (xs ∙ ys) = begin
  ⌜ ⟦ xs ⟧ ++ ⟦ ys ⟧ ⌝     ≡⟨ ⌜⌝-resp-++ _ _ ⟩
  ⌜ ⟦ xs ⟧ ⌝ ∙ ⌜ ⟦ ys ⟧ ⌝  ≡⟨ _∙_ <$> completeness xs <*> completeness ys ⟩
  xs ∙ ys                  ∎
completeness ε         = refl
completeness (∙-unitˡ xs i)       = {!!} -- those should be trival to prove since
completeness (∙-unitʳ xs i)       = {!!} -- `Monoid A` is a set.
completeness (∙-assoc xs ys zs i) = {!!}
completeness (squash  p  q  i  j) = {!!}