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

open import Algebra
open import Prelude hiding (P)

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

open Semilattice mod

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

open import CCS.Hyp.SemiModel {R = R} mod hiding (⟦_⟧ᶜ)

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

private instance
  hypAlgInst : ⦃ _ : IsDiscrete A ⦄ → CCSAlg (Communicator A R)
  hypAlgInst {A = A} = hypAlg {Name = A}

private instance
  _ : ⦃ _ : IsDiscrete A ⦄ → CCSSemiModel (Communicator A R)
  _ = hypMod 

module _ {A B : Type r} ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄ where
  ρ-hom : ∀  (f : A ⇔ B) p → ρ (bic f) ⟦ p ⟧ ≡ ⟦ `ρ (fun f) p ⟧
  ρ-hom f `𝟘 = cong-ι λ h → refl
  ρ-hom f (p `⊕ q) = ρ-⊕ (bic f) ⟦ p ⟧ ⟦ q ⟧ ⨾ cong₂ _⊕_ (ρ-hom f p) (ρ-hom f q)
  ρ-hom f (p `∥ q) = ρ-⊕ (bic f) ⟦ p ⌊ q ⟧ ⟦ q ⌊ p ⟧ ⨾ cong₂ _⊕_ (ρ-hom f (p ⌊ q)) (ρ-hom f (q ⌊ p))
  ρ-hom f′ (x `· p) = cong-ι (funExt ∘′ lemma x p)
    where
    f = bic f′
    lemma : ∀ (a : Act A) p q m → ι (ρ f ⟦ a · p ⟧) q m ≡ ι ⟦ `ρ (fst f) (a · p) ⟧ q m
    lemma a p q 𝕥 =
      ι (ρ f ⟦ a · p ⟧) q 𝕥 ≡⟨⟩
      ι ⟦ a · p ⟧ (ρ (swap f) q) 𝕥 ≡⟨⟩
      ι (ρ (swap f) q) ⟦ p ⟧ (𝕚 a) ≡⟨⟩
      ι q (ρ f ⟦ p ⟧) (𝕚 (map-act (fst f) a)) ≡⟨ cong (flip (ι q) _) (ρ-hom f′ p) ⟩
      ι ⟦ `ρ (fst f) (a · p) ⟧ q 𝕥 ∎
      
    lemma (out a) p q (𝕚 (inp b)) with snd f b ≟ a | b ≟ fst f a
    ... | no _ | no _ = refl
    ... | yes _ | yes _ = cong (flip (ι q) (𝕚 τ)) (ρ-hom f′ p)
    ... | yes f⁻b≡a | no b≢fa = absurd (b≢fa (sym (rightInv f′ b) ⨾ cong (f .fst) f⁻b≡a))
    ... | no f⁻b≢a | yes b≡fa = absurd (f⁻b≢a (cong (f .snd) b≡fa ⨾ leftInv f′ a))
    lemma (inp a) p q (𝕚 b) = refl
    lemma τ       p q (𝕚 b) = refl
    lemma (out a) p q (𝕚 (out b)) = refl
    lemma (out a) p q (𝕚 τ) = refl

  ρ-hom f′ (`ν n - p) = cong-ι (funExt ∘′ lemma n p)
    where
    f = bic f′
    lemma : ∀ (n : A) p q m → ι (ρ f ⟦ ν n - p ⟧) q m ≡ ι ⟦ `ρ (fst f) (ν n - p) ⟧ q m
    lemma n p q 𝕥 =
      ι (ρ f ⟦ ν n - p ⟧) q 𝕥 ≡⟨⟩
      ι ⟦ p ⟧ (ν n - ρ (swap f) q) 𝕥 ≡⟨ cong (flip (ι ⟦ p ⟧) 𝕥) (ν-ρ-comm n (sym-⇔ f′) q) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ν (fst f n) - q)) 𝕥 ≡⟨⟩
      ι (ρ f ⟦ p ⟧) (ν (fst f n) - q) 𝕥 ≡⟨ cong (λ e → ι e (ν (fst f n) - q) 𝕥) (ρ-hom f′ p) ⟩
      ι ⟦ `ρ (fst f) p ⟧ (ν (fst f n) - q) 𝕥 ≡⟨⟩
      ι ⟦ `ν fst f n - `ρ (fst f) p ⟧ q 𝕥 ∎
    lemma n p q (𝕚 τ) =
      ι (ρ f ⟦ ν n - p ⟧) q (𝕚 τ) ≡⟨⟩
      ι ⟦ p ⟧ (ν n - ρ (swap f) q) (𝕚 τ) ≡⟨ cong (flip (ι ⟦ p ⟧) (𝕚 τ)) (ν-ρ-comm n (sym-⇔ f′) q) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ν (fst f n) - q)) (𝕚 τ) ≡⟨⟩
      ι (ρ f ⟦ p ⟧) (ν (fst f n) - q) (𝕚 τ) ≡⟨ cong (λ e → ι e (ν (fst f n) - q) (𝕚 τ)) (ρ-hom f′ p) ⟩
      ι ⟦ `ρ (fst f) p ⟧ (ν (fst f n) - q) (𝕚 τ) ≡⟨⟩
      ι ⟦ `ν fst f n - `ρ (fst f) p ⟧ q (𝕚 τ) ∎
    lemma n p q (𝕚 (out x)) with n ≟ snd f x | fst f n ≟ x
    ... | no  n≢f⁻x | yes fn≡x = absurd (n≢f⁻x (sym (leftInv f′ n) ⨾ cong (f .snd) fn≡x))
    ... | yes n≡f⁻x | no fn≢x = absurd (fn≢x (cong (f .fst) n≡f⁻x ⨾ rightInv f′ x ))
    ... | yes n≡f⁻x | yes fn≡x = refl
    ... | no  n≢f⁻x | no fn≢x =
      ι ⟦ p ⟧ (ν n - ρ (swap f) q) (𝕚 (out (f .snd x))) ≡⟨ cong (flip (ι ⟦ p ⟧) (𝕚 (out (f .snd x)))) (ν-ρ-comm n (sym-⇔ f′) q) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ν f .fst n - q)) (𝕚 (out (f .snd x))) ≡⟨⟩
      ι (ρ f ⟦ p ⟧) (ν f .fst n - q) (𝕚 (out x)) ≡⟨ cong (λ e → ι e (ν f .fst n - q) (𝕚 (out x))) (ρ-hom f′ p) ⟩
      ι ⟦ `ρ (f .fst) p ⟧ (ν f .fst n - q) (𝕚 (out x)) ∎
    lemma n p q (𝕚 (inp x)) with n ≟ snd f x | fst f n ≟ x
    ... | no  n≢f⁻x | yes fn≡x = absurd (n≢f⁻x (sym (leftInv f′ n) ⨾ cong (f .snd) fn≡x))
    ... | yes n≡f⁻x | no fn≢x = absurd (fn≢x (cong (f .fst) n≡f⁻x ⨾ rightInv f′ x ))
    ... | yes n≡f⁻x | yes fn≡x = refl
    ... | no  n≢f⁻x | no fn≢x =
      ι ⟦ p ⟧ (ν n - ρ (swap f) q) (𝕚 (inp (f .snd x))) ≡⟨ cong (flip (ι ⟦ p ⟧) (𝕚 (inp (f .snd x)))) (ν-ρ-comm n (sym-⇔ f′) q) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ν f .fst n - q)) (𝕚 (inp (f .snd x))) ≡⟨⟩
      ι (ρ f ⟦ p ⟧) (ν f .fst n - q) (𝕚 (inp x)) ≡⟨ cong (λ e → ι e (ν f .fst n - q) (𝕚 (inp x))) (ρ-hom f′ p) ⟩
      ι ⟦ `ρ (f .fst) p ⟧ (ν f .fst n - q) (𝕚 (inp x)) ∎

  ρ-hom f (`! p) = cong (ρ (bic f)) (!-⌊ ⟦ p ⟧) ⨾ ρ-hom f (p `⌊ `! p) ⨾ sym (!-⌊ ⟦ `ρ (fun f) p ⟧)

  ρ-hom f (p `⌊ q) = cong-ι (funExt ∘′ lemma f p q)
    where

    lemma : ∀ f p q h m → ι (ρ (bic f) ⟦ p ⌊ q ⟧) h m ≡ ι ⟦ `ρ (fun f) (p ⌊ q) ⟧ h m
    lemma f′ p q h 𝕥 =
      let f = bic f′
      in
      ι (ρ f ⟦ p `⌊ q ⟧) h 𝕥 ≡⟨⟩
      ι ⟦ p ⟧ (⟦ q ⟧ ∥ ρ (swap f) h) 𝕥 ≡˘⟨ cong (λ e → ι ⟦ p ⟧ (e ∥ ρ (swap f) h) 𝕥) (ρ⁻¹ (swap f) (leftInv f′) ⟦ q ⟧) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ρ f ⟦ q ⟧) ∥ ρ (swap f) h) 𝕥 ≡˘⟨ cong (flip (ι ⟦ p ⟧) 𝕥) (ρ-∥ (sym-⇔ f′) (ρ f ⟦ q ⟧) h) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ρ f ⟦ q ⟧ ∥ h)) 𝕥 ≡⟨⟩
      ι (ρ f ⟦ p ⟧) (ρ f ⟦ q ⟧ ∥ h) 𝕥 ≡⟨ cong₂ (λ a b → ι a (b ∥ h) 𝕥) (ρ-hom f′ p) (ρ-hom f′ q) ⟩
      ι ⟦ `ρ (fst f) p ⟧ (⟦ `ρ (fst f) q ⟧ ∥ h) 𝕥 ≡⟨⟩
      ι ⟦ `ρ (fst f) p `⌊ `ρ (fst f) q ⟧ h 𝕥 ∎
    lemma f′ p q h (𝕚 (emit e m)) =
      let f = bic f′
      in
      ι ⟦ p ⟧ (⟦ q ⟧ ∥ ρ (swap f) h) (𝕚 (emit e (f .snd m)))         ≡˘⟨ cong (flip (ι ⟦ p ⟧) (𝕚 (emit e (f .snd m)))) (ρ⁻¹ (swap f) (leftInv f′) (⟦ q ⟧ ∥ ρ (swap f) h)) ⟩
      ι (ρ f ⟦ p ⟧)      (ρ f (⟦ q ⟧ ∥ ρ (swap f) h)) (𝕚 (emit e m)) ≡⟨ cong₂ (λ a b → ι a b (𝕚 (emit e m))) (ρ-hom f′ p) (ρ-∥ f′ ⟦ q ⟧ (ρ (swap f) h) ⨾ cong₂ _∥_ (ρ-hom f′ q) (ρ⁻¹ f (rightInv f′) h)) ⟩
      ι ⟦ `ρ (fst f) p `⌊ `ρ (fst f) q ⟧ h (𝕚 (emit e m)) ∎
    lemma f′ p q h (𝕚 τ) =
      let f = bic f′
      in
      ι (ρ f ⟦ p `⌊ q ⟧) h (𝕚 τ) ≡⟨⟩
      ι ⟦ p ⟧ (⟦ q ⟧ ∥ ρ (swap f) h) (𝕚 τ) ≡˘⟨ cong (λ e → ι ⟦ p ⟧ (e ∥ ρ (swap f) h) (𝕚 τ)) (ρ⁻¹ (swap f) (leftInv f′) ⟦ q ⟧) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ρ f ⟦ q ⟧) ∥ ρ (swap f) h) (𝕚 τ) ≡˘⟨ cong (flip (ι ⟦ p ⟧) (𝕚 τ)) (ρ-∥ (sym-⇔ f′) (ρ f ⟦ q ⟧) h) ⟩
      ι ⟦ p ⟧ (ρ (swap f) (ρ f ⟦ q ⟧ ∥ h)) (𝕚 τ) ≡⟨⟩
      ι (ρ f ⟦ p ⟧) (ρ f ⟦ q ⟧ ∥ h) (𝕚 τ) ≡⟨ cong₂ (λ a b → ι a (b ∥ h) (𝕚 τ)) (ρ-hom f′ p) (ρ-hom f′ q) ⟩
      ι ⟦ `ρ (fst f) p ⟧ (⟦ `ρ (fst f) q ⟧ ∥ h) (𝕚 τ) ≡⟨⟩
      ι ⟦ `ρ (fst f) p `⌊ `ρ (fst f) q ⟧ h (𝕚 τ) ∎

module _ {A : Type r} ⦃ disc : IsDiscrete A ⦄ where
  open import Swaps {A = A} ⦃ disc ⦄
  open import CCS.Hyp.SemiModel {R = R} mod {Name = A} using (⟦_⟧ᶜ)

  open import CCS.Hyp.Properties.Restrict mod ⦃ disc ⦄

  ν-ν-ρ : ∀ n m p →
    ν n - ν m - ρ (n /͍ m) p ≡ ρ (n /͍ m) (ν n - ν m - p)
  ν-ν-ρ n m p =
    ν n - ν m - ρ (n /͍ m) p ≡⟨ cong (ν n -_) (ν-ρ-comm m (n /⇔ m) p) ⟩
    ν n - ρ (n /͍ m) (ν (m /↔ n) m - p) ≡⟨ cong (λ e → ν n - ρ (n /͍ m) (ν e - p)) (swap-leq m n) ⟩
    ν n - ρ (n /͍ m) (ν n - p) ≡⟨ ν-ρ-comm n (n /⇔ m) (ν n - p) ⟩
    ρ (n /͍ m) (ν (m /↔ n) n - ν n - p) ≡⟨ cong (λ e → ρ (n /͍ m) (ν e - ν n - p)) (swap-req m n) ⟩
    ρ (n /͍ m) (ν m - ν n - p) ≡⟨ cong (ρ (n /͍ m)) (ν-comm m n p) ⟩
    ρ (n /͍ m) (ν n - ν m - p) ∎

  ρ-ν-ν : ∀ n m p → ρ (n /͍ m) (ν n - ν m - p) ≡ ν n - ν m - p
  ρ-ν-ν n m p = cong-ι (funExt ∘′ lemma n m p)
    where
    open import Data.Bool.Properties

    lemma : ∀ n m p q r →
      ι (ρ (n /͍ m) (ν n - ν m - p)) q r ≡ ι (ν n - ν m - p) q r
    lemma n m p q 𝕥 =
      ι (ρ (n /͍ m) (ν n - ν m - p)) q 𝕥 ≡⟨⟩
      ι p (ν m - ν n - ρ (m /͍ n) q) 𝕥 ≡⟨ cong (flip (ι p) 𝕥) (ν-ν-ρ m n q) ⟩
      ι p (ρ (m /͍ n) (ν m - ν n - q)) 𝕥 ≡⟨ cong (flip (ι p) 𝕥) (ρ-ν-ν m n q) ⟩
      ι p (ν m - ν n - q) 𝕥 ≡⟨⟩
      ι (ν n - ν m - p) q 𝕥 ∎
    lemma n m p q (𝕚 τ) =
      ι p (ν m - ν n - ρ (m /͍ n) q) (𝕚 τ) ≡⟨ cong (flip (ι p) (𝕚 τ)) (ν-ν-ρ m n q) ⟩
      ι p (ρ (m /͍ n) (ν m - ν n - q)) (𝕚 τ) ≡⟨ cong (flip (ι p) (𝕚 τ)) (ρ-ν-ν m n q) ⟩
      ι p (ν m - ν n - q) (𝕚 τ) ∎
    lemma n m p q (𝕚 (emit e s)) with m ≟ s | s ≟ m | n ≟ s | s ≟ n
    ... | yes m≡s | no  s≢m | _ | _ = absurd (s≢m (sym m≡s))
    ... | no  s≢m | yes m≡s | _ | _ = absurd (s≢m (sym m≡s))
    ... | yes m≡s | yes s≡m | _ | _ = cong (bool _ _) (it-does (n ≟ n) refl) ⨾ sym (if-idem ε _ )
    ... | no  m≢s | no  s≢m | yes n≡s | no  s≢n = absurd (s≢n (sym n≡s))
    ... | no  m≢s | no  s≢m | no  s≢n | yes n≡s = absurd (s≢n (sym n≡s))
    ... | no  m≢s | no  s≢m | yes n≡s | yes s≡n = cong (bool _ _) (it-doesn't (n ≟ m) (s≢m ∘ (s≡n ⨾_))) ⨾ cong (bool _ _) (it-does (m ≟ m) refl)
    ... | no  m≢s | no  s≢m | no  n≢s | no  s≢n = cong (bool _ _) (it-doesn't (n ≟ s) n≢s) ⨾ cong (bool _ _) (it-doesn't (m ≟ s) m≢s) ⨾ cong (flip (ι p) (𝕚 (emit e s))) (ν-ν-ρ m n q ⨾ ρ-ν-ν m n q)

  ν-ρ-∉ : ∀ (n m : A) (p : P A) → n ∉ₚ p → ν n - ρ (m /͍ n) ⟦ p ⟧ᶜ ≡ ⟦ ν m - p ⟧ᶜ
  ν-ρ-∉ n m p n∉p =
    ν n - ρ (m /͍ n) ⟦ p ⟧ᶜ                     ≡˘⟨ cong (λ e → ν n - ρ (m /͍ n) e) (ν-∉ n p n∉p) ⟩
    ν n - ρ (m /͍ n) (ν n - ⟦ p ⟧ᶜ)             ≡˘⟨ cong (λ e → ν n - ρ (m /͍ n) (ν e - ⟦ p ⟧)) (swap-req n m) ⟩
    ν n - ρ (m /͍ n) (ν (n /↔ m) m - ⟦ p ⟧ᶜ)   ≡˘⟨ cong (ν n -_) (ν-ρ-comm m (m /⇔ n) ⟦ p ⟧) ⟩
    ν n - ν m - ρ (m /͍ n) ⟦ p ⟧ᶜ               ≡˘⟨ ρ-ν-ν n m (ρ (m /͍ n) ⟦ p ⟧ᶜ) ⟩
    ρ (n /͍ m) (ν n - ν m - ρ (m /͍ n) ⟦ p ⟧ᶜ)   ≡˘⟨ ν-ν-ρ n m (ρ (m /͍ n) ⟦ p ⟧) ⟩
    ν n - ν m - ρ (n /͍ m) (ρ (m /͍ n) ⟦ p ⟧ᶜ)   ≡⟨ cong (λ e → ν n - ν m - e) (ρ-∘ (n /͍ m) (m /͍ n) ⟦ p ⟧ ⨾ cong (flip ρ ⟦ p ⟧) (cong₂ _,_ (funExt (swap-inv n m)) (funExt (swap-inv n m))) ⨾ ρ-id ⟦ p ⟧) ⟩
    ν n - ν m - ⟦ p ⟧ᶜ                         ≡⟨ ν-comm n m ⟦ p ⟧ ⟩
    ν m - ν n - ⟦ p ⟧ᶜ                         ≡⟨ cong (ν m -_) (ν-∉ n p n∉p) ⟩
    ν m - ⟦ p ⟧ᶜ                               ≡⟨⟩
    ⟦ ν m - p ⟧ᶜ ∎