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

open import Prelude hiding (P; A)

module CCS.Fresh.Hyp where

open import Data.Nat

private
  A : Type
  A = ℕ

open import CCS.Alg
open import CCS.SemiModel
import CCS.Proc as ℙ
open import Algebra

open ℙ using (Proc)

open import Data.Set renaming (⟦_⟧ to 𝒦⟦_⟧)

open import Hyper.Base
open import CCS.Hyp.Definition A (Proc A)

open CCSAlg ⦃ ... ⦄
open CCSSemiModel ⦃ ... ⦄

instance
  _ : CCSAlg (Proc A)
  _ = ℙ.procAlg

instance
  _ : CCSSemiModel (Proc A)
  _ = ℙ.procMod

open import CCS.Hyp.Properties {R = Proc A} ℙ.procMod hiding (⊕⌊)

instance
  _ : CCSAlg Communicator
  _ = hypAlg

instance
  _ : CCSSemiModel Communicator
  _ = hypMod


open import CCS.Hyp.Interp {R = Proc A} ℙ.procAlg ⦃ it ⦄

open import CCS.Hyp.Rho {R = Proc A} ⊕-semilattice
open import CCS.Hyp.Properties.Restrict {R = Proc A} ⊕-semilattice ⦃ it ⦄
open import CCS.Hyp.Properties.RestrictPar {R = Proc A} ⊕-semilattice ⦃ it ⦄

open import CCS.Fresh
open import Swaps

ν-⌊-rewrite : ∀ (ns : List A) n p q
            → νₛ ns - ⟦ ν n - p ⌊ q ⟧ᶜ ≡
              νₛ (# (p ⌊ q) ∷ ns) - ⟦ `ρ (n /→ # (p ⌊ q)) p ⌊ q ⟧
ν-⌊-rewrite ns n p q =
  let m = # (p ⌊ q)
      m∉ = #-∉ (p ⌊ q)
  in

  νₛ ns - ⟦ ν n - p ⌊ q ⟧

    ≡⟨⟩

  νₛ ns - (ν n - ⟦ p ⟧ ⌊ ⟦ q ⟧)

    ≡˘⟨ cong (λ e → νₛ ns - (e ⌊ ⟦ q ⟧) ) (ν-ρ-∉ m n p (m∉ ∘ inl)) ⟩

  νₛ ns - (ν m - ρ (n /͍ m) ⟦ p ⟧ ⌊ ⟦ q ⟧)

    ≡˘⟨ cong (λ e → νₛ ns - (ν m - ρ (n /͍ m) ⟦ p ⟧ ⌊ e)) (ν-∉ m q (m∉ ∘ inr) ) ⟩

  νₛ ns - (ν m - ρ (n /͍ m) ⟦ p ⟧ ⌊ ν m - ⟦ q ⟧)

    ≡⟨ cong (νₛ ns -_) (ν-ν-ν-⌊ m _ _) ⟩

  νₛ ns - ν m - (ν m - ρ (n /͍ m) ⟦ p ⟧ ⌊ ν m - ⟦ q ⟧)

    ≡˘⟨ cong (νₛ ns -_) (ν-⌊-ν m _ _) ⟩

  νₛ ns - ν m - (ρ (n /͍ m) ⟦ p ⟧ ⌊ ν m - ⟦ q ⟧)

    ≡⟨ cong (λ e → νₛ ns - ν m - (ρ (n /͍ m) ⟦ p ⟧ ⌊ e)) (ν-∉ m q (m∉ ∘ inr)) ⟩

  νₛ ns - ν m - (ρ (n /͍ m) ⟦ p ⟧ ⌊ ⟦ q ⟧)

    ≡⟨ cong (λ e → νₛ m ∷ ns - (e ⌊ ⟦ q ⟧)) (ρ-hom (n /⇔ m) p)  ⟩

  νₛ ns - ν m - (⟦ `ρ (n /↔ m) p ⟧ ⌊ ⟦ q ⟧)

    ≡˘⟨ cong (λ e → νₛ m ∷ ns - (⟦ e ⟧ ⌊ ⟦ q ⟧)) ( ρ-∉-↔ n m p (m∉ ∘ inl)) ⟩

  νₛ ns - ν m - (⟦ `ρ (n /→ m) p ⟧ ⌊ ⟦ q ⟧)

    ∎

open import Data.Fin

ν-sync-rewrite : ∀ (ns : List A) (n : A) (a : Act A) p q
            → νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ) ≡
              νₛ (# ((a · p) ⌊ q) ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ # ((a · p) ⌊ q)) q ⟧
ν-sync-rewrite ns n a p q = cong-ι (funExt ∘′ lemma)
  where
  m : A
  m = # ((a · p) ⌊ q)

  m∉ : m ∉ₚ ((a · p) ⌊ q)
  m∉ = #-∉ ((a · p) ⌊ q)

  lemma : ∀ r h → ι (νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) r h ≡ ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ m) q ⟧) r h
  lemma r h with ns ₛ∈ₘ? h
  ... | yes (i , ns∈h) =
    ι (νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) r h ≡⟨ ι-∈-νₛ ns _ _ h (i , ns∈h) ⟩
    𝟘 ≡˘⟨ ι-∈-νₛ (m ∷ ns) _ _ h (fs i , ns∈h) ⟩
    ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ m) q ⟧) r h ∎
  ... | no ns∉h with m ∈ₘ? h
  ... | no m∉h =

    ι (νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) r h

      ≡⟨ ι-∉-νₛ ns _ _ h ns∉h ⟩

    ι (syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) (νₛ ns - r) h

      ≡⟨⟩

    ι ⟦ a · p ⟧ᶜ ((ν n - ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) h

      ≡˘⟨ cong (λ e → ι ⟦ a · p ⟧ᶜ (e ⌊ (νₛ ns - r)) h) (ν-ρ-∉ m n q (m∉ ∘ inr)) ⟩

    ι ⟦ a · p ⟧ᶜ ((ν m - ρ (n /͍ m) ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) h

      ≡˘⟨ cong (λ e → ι e ((ν m - ρ (n /͍ m) ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) h) (ν-∉ m (a · p) (m∉ ∘ inl)) ⟩

    ι (ν m - ⟦ a · p ⟧ᶜ) ((ν m - ρ (n /͍ m) ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) h

      ≡⟨ cong (bool _ _) (it-doesn't (m ∈ₘ? h) m∉h) ⟩

    ι ⟦ a · p ⟧ᶜ (ν m - ((ν m - ρ (n /͍ m) ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r))) h

      ≡⟨ cong (flip (ι ⟦ a · p ⟧) h) (ν-ν-⌊ m _ _) ⟩

    ι ⟦ a · p ⟧ᶜ (ν m - ((ν m - ρ (n /͍ m) ⟦ q ⟧ᶜ) ⌊ (ν m - νₛ ns - r))) h

      ≡˘⟨ cong (flip (ι ⟦ a · p ⟧) h) (ν-⌊-ν m _ _) ⟩

    ι ⟦ a · p ⟧ᶜ (ν m - (ρ (n /͍ m) ⟦ q ⟧ᶜ ⌊ (ν m - νₛ ns - r))) h

      ≡˘⟨ cong (bool _ _) (it-doesn't (m ∈ₘ? h) m∉h) ⟩

    ι (ν m - ⟦ a · p ⟧ᶜ) ((ρ (n /͍ m) ⟦ q ⟧ᶜ ⌊ (ν m - νₛ ns - r))) h

      ≡⟨ cong (λ e → ι e (ρ (n /͍ m) ⟦ q ⟧ᶜ ⌊ (ν m - νₛ ns - r)) h) (ν-∉ m (a · p) (m∉ ∘ inl)) ⟩

    ι ⟦ a · p ⟧ᶜ (ρ (n /͍ m) ⟦ q ⟧ᶜ ⌊ (ν m - νₛ ns - r)) h

      ≡⟨⟩

    ι (syncᵢₒ ⟦ a · p ⟧ᶜ (ρ (n /͍ m) ⟦ q ⟧ᶜ)) (ν m - νₛ ns - r) h

      ≡˘⟨ cong (bool _ _) (it-doesn't (m ∈ₘ? h) m∉h) ⟩

    ι (ν m - syncᵢₒ ⟦ a · p ⟧ᶜ (ρ (n /͍ m) ⟦ q ⟧ᶜ)) (νₛ ns - r) h

      ≡˘⟨ ι-∉-νₛ ns _ _ h ns∉h ⟩

    ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ᶜ (ρ (n /͍ m) ⟦ q ⟧ᶜ)) r h

      ≡⟨ cong (λ e → ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ᶜ e) r h) (ρ-hom (n /⇔ m) q) ⟩

    ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /↔ m) q ⟧) r h

      ≡˘⟨ cong (λ e → ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ e ⟧) r h) (ρ-∉-↔ n m q (m∉ ∘ inr)) ⟩

    ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ m) q ⟧) r h ∎

  lemma r (𝕚 (inp b)) | no ns∉h | yes m∈h =

    ι (νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) r (𝕚 (inp b))

      ≡⟨ ι-∉-νₛ ns _ _ (𝕚 (inp b)) ns∉h ⟩

    ι (syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) (νₛ ns - r) (𝕚 (inp b))

      ≡⟨⟩

    ι ⟦ a · p ⟧ᶜ ((ν n - ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) (𝕚 (inp b))

      ≡⟨ ι-∉-inp→𝟘 (a · p) ((ν n - ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) b (m∉ ∘ inl ∘ subst (_∈ₚ (a · p)) (sym m∈h)) ⟩

    𝟘

      ≡˘⟨ cong (bool _ _) (it-does (m ≟ b) m∈h) ⟩

    ι (ν m - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ `ρ (n /→ m) q ⟧ᶜ) (νₛ ns - r) (𝕚 (inp b))

      ≡˘⟨ ι-∉-νₛ ns _ _ (𝕚 (inp b)) ns∉h ⟩

    ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ m) q ⟧) r (𝕚 (inp b)) ∎

  lemma r (𝕚 (out b)) | no ns∉h | yes m∈h =

    ι (νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) r (𝕚 (out b))

      ≡⟨ ι-∉-νₛ ns _ _ (𝕚 (out b)) ns∉h ⟩

    ι (syncᵢₒ ⟦ a · p ⟧ᶜ (ν n - ⟦ q ⟧ᶜ)) (νₛ ns - r) (𝕚 (out b))

      ≡⟨⟩

    ι ⟦ a · p ⟧ᶜ ((ν n - ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) (𝕚 (out b))

      ≡⟨ ι-𝕚-out→𝟘 (a · p) ((ν n - ⟦ q ⟧ᶜ) ⌊ (νₛ ns - r)) b ⟩

    𝟘

      ≡˘⟨ cong (bool _ _) (it-does (m ≟ b) m∈h) ⟩

    ι (ν m - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ `ρ (n /→ m) q ⟧ᶜ) (νₛ ns - r) (𝕚 (out b))

      ≡˘⟨ ι-∉-νₛ ns _ _ (𝕚 (out b)) ns∉h ⟩

    ι (νₛ (m ∷ ns) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ m) q ⟧) r (𝕚 (out b)) ∎