{-# OPTIONS --no-termination-check #-}

open import Algebra
open import Prelude hiding (P)

module CCS.Hyp.SemiModel {r} {R : Type r} (mod : Semilattice R) {Name : Type r} where

open Semilattice mod

open import CCS.Alg
open import CCS.SemiModel
open import CCS.Hyp.Definition Name R
open import CCS.Hyp.Renaming unitalMagma
open import Hyper.Base

open import CCS.Hyp.Alg unitalMagma public
  hiding
  (⌊-∥; !-⌊; ν-comm; ν𝟘)
import CCS.Hyp.Alg
private module AlgInst = CCS.Hyp.Alg unitalMagma

open ℍ-Alg

private module ℍ-Mod where
  ∥-comm : (x y : Communicator) → x ∥ y ≡ y ∥ x
  ∥-comm x y = cong-ι (λ h → funExt λ m → comm _ _)

  ∥-assoc : ∀ x y z → (x ∥ y) ∥ z ≡ x ∥ (y ∥ z)
  ∥-assoc x y z = cong-ι λ h → funExt λ m → assoc _ _ _
                ⨾ cong₂ _∙_ (cong (flip (ι x) m) (sym (∥-assoc y z h)))
                  (cong₂ _∙_
                  (cong (flip (ι y) m) (sym (∥-assoc x z h) ⨾ cong (_∥ h) (∥-comm x z) ⨾ ∥-assoc z x h))
                  (cong (flip (ι z) m) (cong (_∥ h) (∥-comm x y) ⨾ ∥-assoc y x h)))

  ⌊-assoc : ∀ x y z → (x ⌊ y) ⌊ z ≡ x ⌊ (y ∥ z)
  ⌊-assoc x y z = cong-ι λ h → cong (ι x) (sym (∥-assoc y z h))

  !-∥ : ∀ p → ! p ≡ p ∥ ! p
  !-∥ p = cong-ι λ h → funExt λ m →
    ι (! p) h m ≡⟨⟩
    ι p (! p ∥ h) m ≡˘⟨ idem (ι p (! p ∥ h) m) ⟩
    ι p (! p ∥ h) m ∙ ι p (! p ∥ h) m ≡⟨ cong (λ e → ι p (! p ∥ h) m ∙ ι p (e ∥ h) m) (!-∥ p) ⟩
    ι p (! p ∥ h) m ∙ ι p ((p ∥ ! p) ∥ h) m ≡⟨ cong (λ e → ι p (! p ∥ h) m ∙ ι p e m) (cong (_∥ h) (∥-comm p (! p)) ⨾ ∥-assoc (! p) p h) ⟩
    ι p (! p ∥ h) m ∙ ι p (! p ∥ (p ∥ h)) m ≡⟨⟩
    ι p (! p ∥ h) m ∙ ι (! p) (p ∥ h) m ≡⟨⟩
    ι (p ⌊ ! p) h m ∙ ι (! p ⌊ p) h m ≡⟨⟩
    ι (p ⌊ ! p ⊕ ! p ⌊ p) h m ≡⟨⟩
    ι (p ∥ ! p) h m ∎

  𝟘⊕ : (c : Communicator) → 𝟘 ⊕ c ≡ c
  𝟘⊕ c = cong-ι λ h → funExt λ m → ε∙ _

  ⊕-assoc : (x y z : Communicator) → (x ⊕ y) ⊕ z ≡ x ⊕ (y ⊕ z)
  ⊕-assoc x y z = cong-ι (λ k → funExt λ m → assoc _ _ _)

  ⊕-comm : (x y : Communicator) → x ⊕ y ≡ y ⊕ x
  ⊕-comm x y = cong-ι (λ k → funExt λ m → comm (ι x k m) (ι y k m))

  ⊕-idem : (x : Communicator) → x ⊕ x ≡ x
  ⊕-idem x = cong-ι (λ k → funExt λ m → idem (ι x k m))

  𝟘∥ : ∀ (p : Communicator) → 𝟘 ∥ p ≡ p  
  𝟘∥ p = cong-ι λ h → funExt λ m → ε∙ _ ⨾ cong (flip (ι p) m) (𝟘∥ h)

  ∥𝟘 : ∀ p → p ∥ 𝟘 ≡ p  
  ∥𝟘 p = cong-ι λ h → funExt λ m → ∙ε _ ⨾ cong (flip (ι p) m) (𝟘∥ h) 

  ⌊𝟘 : ∀ p → p ⌊ 𝟘 ≡ p
  ⌊𝟘 x = cong-ι λ h → cong (ι x) (𝟘∥ h)

  module _ ⦃ _ : IsDiscrete Name ⦄ where
    ν-⊕ : ∀ (x : Name) p q → ν x - (p ⊕ q) ≡ ν x - p ⊕ ν x - q
    ν-⊕ x p q = cong-ι λ h → funExt (lemma x p q h)
      where
      lemma : ∀ (x : Name) p q h m → ι (ν x - (p ⊕ q)) h m ≡ ι (ν x - p) h m ∙ ι (ν x - q) h m
      lemma x p q h (𝕚 τ) = refl
      lemma x p q h 𝕥 = refl
      lemma x p q h (𝕚 (inp y)) with x ≟ y
      ... | yes _ = sym (ε∙ _)
      ... | no _ = refl
      lemma x p q h (𝕚 (out y)) with x ≟ y
      ... | yes _ = sym (ε∙ _)
      ... | no _ = refl

    ν-∈-· : ∀ (n : Name) a p → n ∈ₐ a → ν n - a · p ≡ 𝟘
    ν-∈-· n a p n∈a = cong-ι (funExt ∘′ lemma n a p n∈a)
      where
      lemma : ∀ (n : Name) a p → n ∈ₐ a → ∀ h m → ι (ν n - a · p) h m ≡ ι 𝟘 h m
      lemma n a p n∈a h m with n ∈ₘ? m
      ... | yes _ = refl
      lemma n a p n∈a h 𝕥 | no  n∉m = cong (bool _ _) (it-does (n ∈ₘ? 𝕚 a) n∈a)
      lemma n (inp a) p n∈a h (𝕚 b) | no  n∉m = refl
      lemma n τ p n∈a h (𝕚 b) | no  n∉m = refl
      lemma n (out a) p n∈a h (𝕚 τ) | no n∉m = refl
      lemma n (out a) p n∈a h (𝕚 (out b)) | no n∉m = refl
      lemma n (out a) p n∈a h (𝕚 (inp b)) | no n∉m with b ≟ a
      ... | no b≢a = refl
      ... | yes b≡a = absurd (n∉m (n∈a ⨾ sym b≡a))

    ν-∉-· : ∀ (n : Name) a p → n ∉ₐ a → ν n - a · p ≡ a · ν n - p
    ν-∉-· n a p n∉a = cong-ι (funExt ∘′ lemma n a p n∉a)
      where
      lemma : ∀ (n : Name) a p → n ∉ₐ a → ∀ h m → ι (ν n - a · p) h m ≡ ι (a · ν n - p) h m
      lemma n a p n∉a h m with n ∈ₘ? m
      lemma n a p n∉a h 𝕥 | no  n∉m = cong (bool _ _) (it-doesn't (n ∈ₐ? a) n∉a)
      lemma n (inp a) p n∉a h (𝕚 b) | no  n∉m = refl
      lemma n τ p n∉a h (𝕚 b) | no  n∉m = refl
      lemma n (out a) p n∉a h (𝕚 τ) | no n∉m = refl
      lemma n (out a) p n∉a h (𝕚 (out b)) | no n∉m = refl
      lemma n (out a) p n∉a h (𝕚 (inp b)) | no n∉m = refl
      lemma n τ p n∉a h (𝕚 _) | yes n∈m = refl
      lemma n (inp a) p n∉a h (𝕚 _) | yes n∈m = refl
      lemma n (out a) p n∉a h (𝕚 (out _)) | yes n∈m = refl
      lemma n (out a) p n∉a h (𝕚 (inp b)) | yes n∈m with b ≟ a
      ... | no b≢a = refl
      ... | yes b≡a = absurd (n∉a (n∈m ⨾ b≡a))

open ℍ-Mod

hypMod : ⦃ _ : IsDiscrete Name ⦄ → CCSSemiModel Communicator
hypMod = record { ℍ-Mod ; AlgInst ; ccsAlg = hypAlg }


module _ ⦃ _ : IsDiscrete Name ⦄ where
  open CCSSemiModel hypMod using (!-⌊)

  ·⌊-decomp : ∀ a p q → a · p ⌊ q ≡ syncᵢₒ (a · p) q ⊕ stepₗ (a · p) q
  ·⌊-decomp a p q = cong-ι (funExt ∘′ lemma a p q)
    where
    lemma : ∀ a p q r m → ι (a · p) (q ∥ r) m ≡ ι (a · p) (q ⌊ r) m ∙ ι (a · p) (r ⌊ q) m
    lemma a p q r 𝕥 = refl
    lemma (inp x) p q r (𝕚 _) = sym (ε∙ _)
    lemma τ p q r (𝕚 _) = sym (ε∙ _)
    lemma (out _) p q r (𝕚 (out _)) = sym (ε∙ _)
    lemma (out _) p q r (𝕚 τ) = sym (ε∙ _)
    lemma (out b) p q r (𝕚 (inp a)) with a ≟ b
    ... | no  a≢b = sym (ε∙ _)
    ... | yes a≡b = refl


  -- ν-∉-⌊ : ∀ n p q → (ν n - p) ⌊ (ν n - q) ≡ ν n - (p ⌊ ν n - q)
  -- ν-∉-⌊ n p q = cong-ι (funExt ∘′ lemma n p q)
  --   where
  --   lemma : ∀ n p q r m → ι (ν n - p) ( (ν n - q) ∥ r ) m ≡ ι (ν n - (p ⌊ ν n - q)) r m
  --   lemma n p q r 𝕥  =
  --     ι (ν n - p ) (ν n - q ∥ r) 𝕥 ≡⟨⟩
  --     ι p (ν n - (ν n - q ∥ r)) 𝕥 ≡⟨ {!!} ⟩
  --     ι p (ν n - q ∥ ν n - r) 𝕥 ≡⟨⟩
  --     ι (ν n - (p ⌊ ν n - q)) r 𝕥 ∎
  --   lemma n p q r (𝕚 x) = {!!}



-- ν-/ : ∀ (n m : Name) p → ν n - p ≡ ν m - ρ (bic (n / m)) p
-- ν-/ n m p = {!!} ⨾ cong (λ e → ρ (bic (n / m)) (ν e - p)) (sym (swap-leq m n)) ⨾ sym (ν-ρ-comm m (n / m) p)  

  mutual

    ν⇓-⊕ : ∀ (n : Name) p q → ν⇓ n (p ⊕ q) ≡ ν⇓ n p ⊕ ν⇓ n q
    ν⇓-⊕ n p q = cong-ι (funExt ∘′ lemma n p q)
      where
      lemma : ∀ (n : Name) p q h m → ι (ν⇓ n (p ⊕ q)) h m ≡ ι (ν⇓ n p ⊕ ν⇓ n q) h m
      lemma n p q h 𝕥 = refl
      lemma n p q h (𝕚 τ) = refl
      lemma n p q h (𝕚 (out m)) with n ≟ m
      ... | yes n≡m = sym (ε∙ _)
      ... | no n≢m = refl
      lemma n p q h (𝕚 (inp m)) with n ≟ m
      ... | yes n≡m = sym (ε∙ _)
      ... | no n≢m = refl

    ν⇑-⊕ : ∀ (n : Name) p q → ν⇑ n (p ⊕ q) ≡ ν⇑ n p ⊕ ν⇑ n q
    ν⇑-⊕ n p q = cong-ι (funExt ∘′ lemma n p q)
      where
      lemma : ∀ (n : Name) p q h m → ι (ν⇑ n (p ⊕ q)) h m ≡ ι (ν⇑ n p ⊕ ν⇑ n q) h m
      lemma n p q h 𝕥 = refl
      lemma n p q h (𝕚 (inp (𝕚 _))) = refl
      lemma n p q h (𝕚 (inp 𝕥)) = sym (ε∙ _)
      lemma n p q h (𝕚 (out (𝕚 _))) = refl
      lemma n p q h (𝕚 (out 𝕥)) = sym (ε∙ _)
      lemma n p q h (𝕚 τ) = refl

  open CCSAlg hypAlg using (⟦_⟧)

  ι-𝕚-τ→𝟘 : ∀ (p : P Name) q → ι ⟦ p ⟧ q (𝕚 τ) ≡ ε
  ι-𝕚-τ→𝟘 (p₁ `⌊ p₂) q = ι-𝕚-τ→𝟘 p₁ (⟦ p₂ ⟧ ∥ q)
  ι-𝕚-τ→𝟘 (p₁ `∥ p₂) q = cong₂ _∙_ (ι-𝕚-τ→𝟘 p₁ (⟦ p₂ ⟧ ∥ q)) (ι-𝕚-τ→𝟘 p₂ (⟦ p₁ ⟧ ∥ q)) ⨾ ε∙ _
  ι-𝕚-τ→𝟘 `𝟘 q = refl
  ι-𝕚-τ→𝟘 (p₁ `⊕ p₂) q = cong₂ _∙_ (ι-𝕚-τ→𝟘 p₁ q) (ι-𝕚-τ→𝟘 p₂ q) ⨾ ε∙ _
  ι-𝕚-τ→𝟘 (inp x `· p) q = refl
  ι-𝕚-τ→𝟘 (out x `· p) q = refl
  ι-𝕚-τ→𝟘 (τ `· p) q = refl
  ι-𝕚-τ→𝟘 (`ν x - p) q = ι-𝕚-τ→𝟘 p (ν x - q)
  ι-𝕚-τ→𝟘 (`! p) q =
    ι ⟦ `! p ⟧ q (𝕚 τ) ≡⟨ cong (λ e → ι e q (𝕚 τ)) (!-⌊ ⟦ p ⟧) ⟩
    ι (⟦ p ⟧ ⌊ ⟦ `! p ⟧) q (𝕚 τ) ≡⟨⟩
    ι ⟦ p ⟧ (⟦ `! p ⟧ ∥ q) (𝕚 τ) ≡⟨ ι-𝕚-τ→𝟘 p (⟦ `! p ⟧ ∥ q) ⟩
    ε ∎

  sync-τ : ∀ p (q : P Name) → syncᵢₒ (τ · p) ⟦ q ⟧ ≡ 𝟘
  sync-τ p q = cong-ι (funExt ∘′ lemma p q)
    where
    lemma : ∀ p q r m → ι (τ · p) (⟦ q ⟧ ⌊ r) m ≡ ι 𝟘 r m
    lemma p q r (𝕚 x) = refl
    lemma p q r 𝕥 = ι-𝕚-τ→𝟘 q (r ∥ p)

  ι-𝕚-out→𝟘 : ∀ (p : P Name) q (a : Name) → ι ⟦ p ⟧ q (𝕚 (out a)) ≡ ε
  ι-𝕚-out→𝟘 (p₁ `∥ p₂) q a = cong₂ _∙_ (ι-𝕚-out→𝟘 p₁ (⟦ p₂ ⟧ ∥ q) a) (ι-𝕚-out→𝟘 p₂ (⟦ p₁ ⟧ ∥ q) a) ⨾ ε∙ _
  ι-𝕚-out→𝟘 (p₁ `⌊ p₂) q a = ι-𝕚-out→𝟘 p₁ (⟦ p₂ ⟧ ∥ q) a
  ι-𝕚-out→𝟘 `𝟘 q a = refl
  ι-𝕚-out→𝟘 (p₁ `⊕ p₂) q a = cong₂ _∙_ (ι-𝕚-out→𝟘 p₁ q a) (ι-𝕚-out→𝟘 p₂ q a) ⨾ ε∙ _
  ι-𝕚-out→𝟘 (inp x `· p) q a = refl
  ι-𝕚-out→𝟘 (out x `· p) q a = refl
  ι-𝕚-out→𝟘 (τ `· p) q a = refl
  ι-𝕚-out→𝟘 (`ν x - p) q a with x ≟ a
  ... | no _ = ι-𝕚-out→𝟘 p (ν x - q) a
  ... | yes _ = refl
  ι-𝕚-out→𝟘 (`! p) q a =
    ι ⟦ `! p ⟧ q (𝕚 (out a)) ≡⟨ cong (λ e → ι e q (𝕚 (out a))) (!-⌊ ⟦ p ⟧) ⟩
    ι (⟦ p ⟧ ⌊ ⟦ `! p ⟧) q (𝕚 (out a)) ≡⟨⟩
    ι ⟦ p ⟧ (⟦ `! p ⟧ ∥ q) (𝕚 (out a)) ≡⟨ ι-𝕚-out→𝟘 p (⟦ `! p ⟧ ∥ q) a ⟩
    ε ∎

  sync-out : ∀ (a : Name) p (q : P Name) → syncᵢₒ (out a · p) ⟦ q ⟧ ≡ 𝟘
  sync-out a p q = cong-ι (funExt ∘′ lemma a p q)
    where
    lemma : ∀ a (p : Communicator) q r m → ι (out a · p) (⟦ q ⟧ ⌊ r) m ≡ ι 𝟘 r m
    lemma a p q r 𝕥 = ι-𝕚-out→𝟘 q (r ∥ p) a
    lemma a p q r (𝕚 (out x)) = refl
    lemma a p q r (𝕚 τ) = refl
    lemma b p q r (𝕚 (inp a)) with a ≟ b
    ... | no a≢b = refl
    ... | yes a≡b = ι-𝕚-τ→𝟘 q (r ∥ p)

  ι-∉-inp→𝟘 : ∀ (p : P Name) q (a : Name) → a ∉ₚ p → ι ⟦ p ⟧ q (𝕚 (inp a)) ≡ ε
  ι-∉-inp→𝟘 `𝟘 q a a∉p = refl
  ι-∉-inp→𝟘 (p `⊕ q) r a a∉p = cong₂ _∙_ (ι-∉-inp→𝟘 p r a (a∉p ∘ inl)) (ι-∉-inp→𝟘 q r a (a∉p ∘ inr)) ⨾ idem ε
  ι-∉-inp→𝟘 (p `⌊ q) r a a∉p = ι-∉-inp→𝟘 p (⟦ q ⟧ ∥ r) a (a∉p ∘ inl)
  ι-∉-inp→𝟘 (p `∥ q) r a a∉p = cong₂ _∙_ (ι-∉-inp→𝟘 p (⟦ q ⟧ ∥ r) a (a∉p ∘ inl)) (ι-∉-inp→𝟘 q (⟦ p ⟧ ∥ r) a (a∉p ∘ inr)) ⨾ idem ε
  ι-∉-inp→𝟘 (inp x `· p) q a a∉p = refl
  ι-∉-inp→𝟘 (τ `· p) q a a∉p = refl
  ι-∉-inp→𝟘 (out b `· p) q a a∉p with a ≟ b
  ... | no a≢b = refl
  ... | yes a≡b = absurd (a∉p (inl a≡b))
  ι-∉-inp→𝟘 (`! p) q a a∉p = ι-∉-inp→𝟘 p (⟦ `! p ⟧ ∥ q) a a∉p
  ι-∉-inp→𝟘 (`ν b - p) q a a∉p with b ≟ a
  ... | yes _ = refl
  ... | no _ = ι-∉-inp→𝟘 p (ν b - q) a (a∉p ∘ inr)

  sync-∉ : ∀ (a : Name) p (q : P Name) → a ∉ₚ q → syncᵢₒ (inp a · p) ⟦ q ⟧ ≡ 𝟘
  sync-∉ a p q a∉q = cong-ι (funExt ∘′ lemma a p q a∉q)
    where
    lemma : ∀ (a : Name) p (q : P Name) → a ∉ₚ q → ∀ r m → ι (syncᵢₒ (inp a · p) ⟦ q ⟧) r m ≡ ε
    lemma a p q a∉q r 𝕥 = ι-∉-inp→𝟘 q (r ∥ p) a a∉q
    lemma a p q a∉q r (𝕚 _) = refl
  
  open CCSAlg hypAlg using (νₛ_-_; νₛᵣ_-_)
  open CCSSemiModel hypMod using (νₛ-lr)

  open import Data.Fin

  ι-∈-νₛ : ∀ ns p q m → ns ₛ∈ₘ m → ι (νₛ ns - p) q m ≡ ε
  ι-∈-νₛ ns p q m ns∈m = cong (λ p → ι p q m) (νₛ-lr ns p) ⨾ lemma ns p q m ns∈m
    where
    lemma : ∀ ns p q m → ns ₛ∈ₘ m → ι (νₛᵣ ns - p) q m ≡ ε
    lemma (n ∷ ns) p q m (i , ns∈m) with n ∈ₘ? m
    ... | yes _ = refl
    lemma (n ∷ ns) p q m (fz   , ns∈m) | no n∉m = absurd (n∉m ns∈m)
    lemma (n ∷ ns) p q m (fs i , ns∈m) | no n∉m = lemma ns p (ν n - q) m (i , ns∈m)

  ι-∉-νₛ : ∀ ns p q m → ns ₛ∉ₘ m → ι (νₛ ns - p) q m ≡ ι p (νₛ ns - q) m
  ι-∉-νₛ ns p q m ns∉m = cong (λ p → ι p q m) (νₛ-lr ns p) ⨾ lemma ns p q m ns∉m
    where
    open import Data.List.Properties

    lemma : ∀ (ns : List Name) (p q : Communicator) m → ns ₛ∉ₘ m → ι (νₛᵣ ns - p) q m ≡ ι p (νₛ ns - q) m
    lemma [] p q m ns∉m = refl
    lemma (n ∷ ns) p q m ns∉m with n ∈ₘ? m
    ... | yes n∈m = absurd (ns∉m (fz , n∈m))
    ... | no _ = lemma ns p (ν n - q) m (λ { (i , pr) → ns∉m (fs i , pr) } )

  ι-νₛ-𝕥 : (ns : List Name) (p q : Communicator) → ι (νₛ ns - p) q 𝕥 ≡ ι p (νₛ ns - q) 𝕥
  ι-νₛ-𝕥 ns p q = ι-∉-νₛ ns p q 𝕥 (Poly-absurd ∘ snd)