{-# OPTIONS --safe #-}

module CCS.SemiModel where

open import Prelude hiding (P)
open import CCS.Alg
open import Algebra

record CCSSemiModel (C : Type c) : Type (ℓsuc c) where
  field ⦃ ccsAlg ⦄ : CCSAlg C
  open CCSAlg ccsAlg

  open CCSAlg ccsAlg public
    using ()
    renaming (Name to MName)

  field
    𝟘⊕ : ∀ p → 𝟘 ⊕ p ≡ p
    ⊕-assoc : ∀ x y z → (x ⊕ y) ⊕ z ≡ x ⊕ (y ⊕ z)
    ⊕-comm : ∀ x y → x ⊕ y ≡ y ⊕ x
    ⊕-idem : ∀ x → x ⊕ x ≡ x

    ⌊-∥ : ∀ p q → p ∥ q ≡ (p ⌊ q) ⊕ (q ⌊ p)
    ⌊-assoc : ∀ x y z → (x ⌊ y) ⌊ z ≡ x ⌊ (y ∥ z)

    𝟘⌊ : ∀ p → 𝟘 ⌊ p ≡ 𝟘
    ⌊𝟘 : ∀ p → p ⌊ 𝟘 ≡ p
    ⊕⌊ : ∀ p q r → (p ⊕ q) ⌊ r ≡ (p ⌊ r) ⊕ (q ⌊ r)

    ν𝟘 : ∀ x → ν x - 𝟘 ≡ 𝟘
    ν-comm : ∀ x y p → ν x - ν y - p ≡ ν y - ν x - p
    ν-⊕ : ∀ x p q → ν x - (p ⊕ q) ≡ ν x - p ⊕ ν x - q

    !-⌊ : ∀ p → ! p ≡ p ⌊ ! p
    !-∥ : ∀ p → ! p ≡ p ∥ ! p

    ν-∈-· : ∀ n a p → n ∈ₐ a → ν n - a · p ≡ 𝟘
    ν-∉-· : ∀ n a p → n ∉ₐ a → ν n - a · p ≡ a · ν n - p

  ⊕𝟘 : ∀ p → p ⊕ 𝟘 ≡ p
  ⊕𝟘 p = ⊕-comm p 𝟘 ⨾ 𝟘⊕ p

  ⊕-semilattice : Semilattice C
  ⊕-semilattice = record
    { commutativeMonoid = record
      { monoid = record
        { _∙_ = _⊕_
        ; ε = 𝟘
        ; ε∙ = 𝟘⊕
        ; ∙ε = ⊕𝟘
        ; assoc = ⊕-assoc
        }
      ; comm = ⊕-comm
      }
    ; idem = ⊕-idem
    }

  𝟘∥ : ∀ p → 𝟘 ∥ p ≡ p
  𝟘∥ p = ⌊-∥ 𝟘 p ⨾ cong₂ _⊕_ (𝟘⌊ p) (⌊𝟘 p) ⨾ 𝟘⊕ p

  ∥-comm : ∀ p q → p ∥ q ≡ q ∥ p
  ∥-comm p q = ⌊-∥ p q ⨾ ⊕-comm _ _ ⨾ sym (⌊-∥ q p)

  ∥𝟘 : ∀ p → p ∥ 𝟘 ≡ p
  ∥𝟘 p = ∥-comm p 𝟘 ⨾ 𝟘∥ p

  ⌊-comm : ∀ x y z → x ⌊ y ⌊ z ≡ x ⌊ z ⌊ y
  ⌊-comm x y z =
    x ⌊ y ⌊ z ≡⟨ ⌊-assoc x y z ⟩
    x ⌊ (y ∥ z) ≡⟨ cong (x ⌊_) (∥-comm y z) ⟩
    x ⌊ (z ∥ y) ≡˘⟨ ⌊-assoc x z y ⟩
    x ⌊ z ⌊ y ∎

  ∥-assoc : ∀ x y z → (x ∥ y) ∥ z ≡ x ∥ (y ∥ z)
  ∥-assoc x y z =
    (x ∥ y) ∥ z                             ≡⟨ ⌊-∥ (x ∥ y) z ⟩
    (x ∥ y)         ⌊ z       ⊕ z ⌊ (x ∥ y) ≡⟨ cong (λ e → e ⌊ z ⊕ z ⌊ (x ∥ y)) (⌊-∥ x y) ⟩
    (x ⌊ y ⊕ y ⌊ x) ⌊ z       ⊕ z ⌊ (x ∥ y) ≡⟨ cong (_⊕ z ⌊ (x ∥ y)) (⊕⌊ (x ⌊ y) (y ⌊ x) z) ⟩
    (x ⌊  y ⌊ z  ⊕ y ⌊ x ⌊ z) ⊕ z ⌊ (x ∥ y) ≡⟨ cong₂ _⊕_ (cong₂ _⊕_ (⌊-assoc x y z) (⌊-comm y x z)) (cong (z ⌊_) (∥-comm x y) ⨾ sym (⌊-assoc z y x)) ⟩
    (x ⌊ (y ∥ z) ⊕ y ⌊ z ⌊ x) ⊕ z ⌊  y ⌊ x   ≡⟨ ⊕-assoc (x ⌊ (y ∥ z)) (y ⌊ z ⌊ x) (z ⌊ y ⌊ x) ⟩
     x ⌊ (y ∥ z) ⊕ (y ⌊ z ⌊ x ⊕ z ⌊  y ⌊ x)  ≡˘⟨ cong (x ⌊ (y ∥ z) ⊕_) (⊕⌊ (y ⌊ z) (z ⌊ y) x) ⟩
     x ⌊ (y ∥ z) ⊕ (y ⌊ z ⊕ z ⌊ y) ⌊ x      ≡˘⟨ cong (λ e → x ⌊ (y ∥ z) ⊕ e ⌊ x) (⌊-∥ y z) ⟩
     x ⌊ (y ∥ z) ⊕ (y ∥ z)         ⌊ x      ≡˘⟨ ⌊-∥ x (y ∥ z) ⟩
     x ∥ (y ∥ z) ∎

  open import Data.List.Properties

  νₛ-comm-∷ : ∀ x xs p → ν x - νₛ xs - p ≡ νₛ xs - ν x - p
  νₛ-comm-∷ x xs p = foldl-fusion (ν x -_) p (flip (ν-comm x)) xs

  νₛ-comm : ∀ xs ys p → νₛ xs - νₛ ys - p ≡ νₛ ys - νₛ xs - p
  νₛ-comm xs ys p = sym (foldl-fusion (νₛ ys -_) p (λ p y → sym (νₛ-comm-∷ y ys p)) xs)

  νₛ-⊕ : ∀ x p q → νₛ x - (p ⊕ q) ≡ νₛ x - p ⊕ νₛ x - q
  νₛ-⊕ []       p q = refl
  νₛ-⊕ (x ∷ xs) p q = cong (νₛ xs -_) (ν-⊕ x p q) ⨾ νₛ-⊕ xs (ν x - p) (ν x - q)

  νₛ-lr : ∀ ns p → νₛ ns - p ≡ νₛᵣ ns - p
  νₛ-lr [] p = refl
  νₛ-lr (n ∷ ns) p =
    νₛ n ∷ ns - p ≡⟨⟩
    νₛ ns - ν n - p ≡˘⟨ νₛ-comm-∷ n ns p ⟩
    ν n - νₛ ns - p ≡⟨ cong (ν n -_) (νₛ-lr ns p) ⟩
    ν n - νₛᵣ ns - p ≡⟨⟩
    νₛᵣ n ∷ ns - p ∎

  νₛ-𝟘 : ∀ ns → νₛ ns - 𝟘 ≡ 𝟘
  νₛ-𝟘 [] = refl
  νₛ-𝟘 (n ∷ ns) = cong (νₛ ns -_) (ν𝟘 n) ⨾ νₛ-𝟘 ns

  open import Data.Fin

  module _ ⦃ _ : IsDiscrete Name ⦄ where

    νₛ-∈-· : ∀ ns a p → ns ₛ∈ₐ a → νₛ ns - a · p ≡ 𝟘
    νₛ-∈-· (n ∷ ns) a p (fz   , n∈a) = cong (νₛ ns -_) (ν-∈-· n a p n∈a) ⨾ νₛ-𝟘 ns
    νₛ-∈-· (n ∷ ns) a p (fs i , ns∈a) with n ∈ₐ? a
    ... | yes n∈a = cong (νₛ ns -_) (ν-∈-· n a p n∈a) ⨾ νₛ-𝟘 ns
    ... | no  n∉a = cong (νₛ ns -_) (ν-∉-· n a p n∉a) ⨾ νₛ-∈-· ns a (ν n - p) (i , ns∈a)

  νₛ-∉-· : ∀ ns a p → ns ₛ∉ₐ a → νₛ ns - a · p ≡ a · νₛ ns - p
  νₛ-∉-· []       a p ns∉a = refl
  νₛ-∉-· (n ∷ ns) a p ns∉a = cong (νₛ ns -_) (ν-∉-· n a p (ns∉a ∘ (fz ,_))) ⨾ νₛ-∉-· ns a (ν n - p) (ns∉a ∘ there {P = _∈ₐ a} n)

  ν⌊-⊕ : ∀ p q ns r → νₛ ns - ((p ⊕ q) ⌊ r) ≡ νₛ ns - (p ⌊ r) ⊕ νₛ ns - (q ⌊ r)
  ν⌊-⊕ p q ns r =
    νₛ ns - ((p ⊕ q) ⌊ r) ≡⟨ cong (νₛ ns -_) (⊕⌊ _ _ _) ⟩
    νₛ ns - (p ⌊ r ⊕ q ⌊ r) ≡⟨ νₛ-⊕ ns (p ⌊ r) (q ⌊ r) ⟩
    νₛ ns - (p ⌊ r) ⊕ νₛ ns - (q ⌊ r) ∎

  ν⌊-𝟘 : ∀ ns r → νₛ ns - (𝟘 ⌊ r) ≡ 𝟘
  ν⌊-𝟘 ns r = cong (νₛ ns -_) (𝟘⌊ r) ⨾ νₛ-𝟘 ns