{-# OPTIONS --without-K --guardedness --no-sized-types #-}


{-
  #####################################################################

  This file centralizes all the lemmas and propositions from the paper
  "Infinite Types, Infinite Data, Infinite Interaction" to make it
  easier to check that the Agda code does indeed correspond to the
  paper's properties.

  Note that all the files are compiled with the flags "--without-K" to
  make sure only intensional equality is used.

  Most of the files are compiled with the flag "--safe" as well, but a
  couple of them make use of the pragma "TERMINATING" to switch the
  termination checker off.

  The corresponding functions are written in such a way as to make it
  obvious that the functions do indeed terminate, and that the problems
  come from an over-eager termination checker.

    - RTC/free-monad.agda
      The function requiring the pragma TERMINATING has been rewritten
      using auxilliary functions to make the termination checker
      happy.

    - RTC/comonad.agda


  #####################################################################
-}


-- definitions
open import prelude
open import equality
open import RTC
open import Simulations
open import Bisimulation
open import Layering


-- proofs of properties
import InteractionSystems.properties
import RTC.free-monad
import Bisimulation.reflexivity
import Bisimulation.symmetry
import Bisimulation.transitivity
import InteractionSystems.WTC-isomorphisms
import Simulations.identity
open import Simulations.composition using () renaming (composition to sim-composition)
import Simulations.eval-composition
import RTC.WTC
import InteractionSystems.execution
import RTC.comonad
import RTC.eval-epsilon
import Layering.WTC
import Layering.WTC-bis



module PAPER
  -- we will occasionaly need function extensionality
  (fun-ext : {X : Set} {Y : Pow X} (f g : (x : X) → Y x) (eq : (x : X) → (f x) ≡ (g x)) → f ≡ g) where



---------------------------------------------
-- basic properties of interaction systems --
---------------------------------------------

--
-- the definition of interaction systems can be found in file dtt.agda
-- if I : Set, IS I is the (large) type of interaction systems over I
-- the extension of interaction systems can be found in file dtt.agda
-- if w : IS I then ⟦ w ⟧ : Pow I → Pow I

lemma-3-3 : {I : Set} (w : IS I) (X Y : Pow I) → (X ⊂ Y) → (⟦ w ⟧(X) ⊂ ⟦ w ⟧(Y))
lemma-3-3 = functoriality


--
-- the composition of interaction systems can be found in file InteractionSystems.agda
-- it is written with ○
module lemma-3-6 {I : Set} (w₁ w₂ : IS I) (X : Pow I) where

  functions : ⟦ w₂ ⟧ (⟦ w₁ ⟧ X) == ⟦ w₂ ○ w₁ ⟧ (X)       -- "U == V" is  "(U ⊂ V) × (V ⊂ U)"
  functions = InteractionSystems.properties.composition.lemma₂ w₂ w₁ X ,
              InteractionSystems.properties.composition.lemma₁ w₂ w₁ X

  -- this requires function extensionality
  isomorphism : let f = fst functions in
                let g = snd functions in
                ({i : I} (x : _) → f (g {i} x) ≡ x)
                ×
                ({i : I} (x : _) → g (f {i} x) ≡ x)
  isomorphism = InteractionSystems.properties.composition.lemma-eq₂ w₂ w₁ fun-ext X ,
                InteractionSystems.properties.composition.lemma-eq₁ w₂ w₁ fun-ext X


--
-- duality of interaction systems is defined in file InteractionSystems.agda
-- it is written with a postfix ⊥
module lemma-3-8 {I : Set} (w : IS I) (X : Pow I) where
  functions :
    let open IS w renaming (Command to A ; Response to D ; next to n) in
    ⟦ w ⊥ ⟧ X  ==  λ i → Π (A i) λ a → Σ (D i a) λ d → X (n a d)
  functions = InteractionSystems.properties.duality.lemma₁ w X ,
              InteractionSystems.properties.duality.lemma₂ w X

  -- this requires function extensionality
  isomorphism :
    let open IS w renaming (Command to A ; Response to D ; next to n) in
    let f = fst functions in
    let g = snd functions in
    ({i : I} (x : _) → (f (g {i} x)) ≡ x)
    ×
    ({i : I} (x : _) → (g (f {i} x)) ≡ x)
  isomorphism = InteractionSystems.properties.duality.lemma-eq₁ w X fun-ext ,
                InteractionSystems.properties.duality.lemma-eq₂ w X fun-ext



------------------------------------------------------------
-- Reflexive and transitive closure (RTC), aka free monad --
------------------------------------------------------------

--
-- the definition of w * can be found in file RTC.agda
module lemma-3-10 {I : Set} (w : IS I) where
  -- I never defined "_∪_" since I've never had to use disjoint product.
  -- Instead of proving "X ∪ ⟦ w ⟧ (⟦ w * ⟧ X) ⊂ ⟦ w * ⟧ X", I prove the 2 inclusions
  -- "X ⊂ ⟦ w * ⟧ X" and "⟦ w ⟧ (⟦ w * ⟧ X) ⊂ ⟦ w * ⟧ X".
  incl₁ : (X : Pow I) → X ⊂ ⟦ w * ⟧ X
  incl₁ = RTC.free-monad.reflexive w

  incl₂ : (X : Pow I) → ⟦ w ⟧ (⟦ w * ⟧ X) ⊂ ⟦ w * ⟧ X
  incl₂ = RTC.free-monad.transitive w

  least : (X Y : Pow I) → (X ⊂ Y) → (⟦ w ⟧ Y ⊂ Y) → ⟦ w * ⟧ X ⊂ Y
  least = RTC.free-monad.least w



------------------
-- bisimilarity --
------------------

--
-- bisimilatiry is defined in file Bisimulation.agda, it is written ≈.

--
-- ≈ is an equivalence relation
module lemma-3-11 {I : Set} (w : IS I) where

  reflexivity : {i : I} (T : ν w i) → T ≈ T
  reflexivity = Bisimulation.reflexivity.reflexivity w

  symmetry : {i : I} {T₁ T₂ : ν w i} → (T₁ ≈ T₂) → T₂ ≈ T₁
  symmetry = Bisimulation.symmetry.symmetry w

  transitivity : {i : I} {T₁ T₂ T₃ : ν w i} → (T₁ ≈ T₂) → (T₂ ≈ T₃) → T₁ ≈ T₃
  transitivity = Bisimulation.transitivity.transitivity w


--
-- If C is a weakly terminal coalgebra for ⟦ w ⟧, then C is a retract
-- (up to bisimulation) of ν w
module corollary-3-13 {I : Set} (w : IS I)
  (C : Pow I)
  (wtc : WTC w C)      -- weakly terminal coalgebras (WTC) are defined in InteractionSystems.agda
  where

  f : C ⊂ ν w
  f = InteractionSystems.WTC-isomorphisms.f w C wtc

  g : ν w ⊂ C
  g = InteractionSystems.WTC-isomorphisms.g w C wtc

  lemma : {i : I} (T : ν w i) → f (g T) ≈ T
  lemma T = InteractionSystems.WTC-isomorphisms.lemma w C wtc T



------------------------
-- linear simulations --
------------------------

--
-- linear simulations are defined in file Simulations.agda
-- we write w₁ ⊸ w₂ for the type of linear simulations from w₁ to w₂

--
-- evaluation function for linear simulations
lemma-4-3 : {I₁ I₂ : Set} (w₁ : IS I₁) (w₂ : IS I₂) → (S : w₁ ⊸ w₂) →
            let open Simulation S using (R) in
            (i₁ : I₁) → (i₂ : I₂) → R i₁ i₂ →
            ν (w₁ ⊥) i₁ → ν (w₂ ⊥) i₂
lemma-4-3 w₁ w₂ S i₁ i₂ = linear-evaluation w₁ w₂ S

-- a synonym
eval : _
eval = lemma-4-3


--
-- the identity simulation is defined in file Simulations/identity.agda

--
-- the composition of 2 simulations is defined in file Simulations/composition.agda
-- the relation part is indeed defined as the relational composition of the relation parts


--
-- composition of simulation corresponds to evaluation of compositions
lemma-4-5 : {I₁ I₂ I₃ : Set} (w₁ : IS I₁) (w₂ : IS I₂) (w₃ : IS I₃)
            (RSim : w₁ ⊸ w₂) (SSim : w₂ ⊸ w₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) →
            let open Simulation RSim using (R) in
            let open Simulation SSim using () renaming (R to S) in
            (r : R i₁ i₂) (s : S i₂ i₃) →
            (T : ν (w₁ ⊥) i₁) →
            eval w₁ w₃ (sim-composition SSim RSim) i₁ i₃ (i₂ , (s , r)) T ≈ eval w₂ w₃ SSim i₂ i₃ s (eval w₁ w₂ RSim i₁ i₂ r T)
lemma-4-5 w₁ w₂ w₃ RSim SSim i₁ i₂ i₃ = Simulations.eval-composition.lemma RSim SSim


--
-- ν (w * ⊥) is a weakly terminal algebra for ν (w ⊥)
module lemma-4-7 {I : Set} (w : IS I) where

  elim : ν (w * ⊥) ⊂ ⟦ w ⊥ ⟧ (ν (w * ⊥))
  elim = RTC.WTC.elim w fun-ext

  intro : (X : Pow I) (coalg : X ⊂ ⟦ w ⊥ ⟧ X) → X ⊂ ν (w * ⊥)
  intro = RTC.WTC.intro w fun-ext

  comp :  (X : Pow I) (coalg : X ⊂ ⟦ w ⊥ ⟧ X) (i : I) (x : X i) →
          elim (intro X coalg x)
          ≡
          functoriality (w ⊥) X (ν (w * ⊥)) (intro X coalg) (coalg x)
  comp X coalg i x = RTC.WTC.comp w fun-ext X coalg i x

  wtc : WTC (w ⊥) (ν (w * ⊥))
  wtc = record {
    elim = elim ;
    intro = intro ;
    comp = comp }


--
-- general evaluation
corollary-4-9 :  {I₁ I₂ : Set} (w₁ : IS I₁) (w₂ : IS I₂) → (S : (w₁ *) ⊸ w₂) →
            let open Simulation S using (R) in
            (i₁ : I₁) → (i₂ : I₂) → R i₁ i₂ →
            ν (w₁ ⊥) i₁ → ν (w₂ ⊥) i₂
corollary-4-9 w₁ w₂ S i₁ i₂ r T₁ =
  let T₁' : ν ((w₁ *) ⊥) i₁
      T₁' = lemma-4-7.intro w₁ (ν (w₁ ⊥)) νElim T₁ in
  lemma-4-3 (w₁ *) w₂ S i₁ i₂ r T₁'

-- a synonym
eval* : _
eval* = corollary-4-9


--
-- Sambin's execution formula
lemma-4-10 :  (I : Set) (w : IS I) (X : Pow I) → (⟦ w * ⟧ X) ≬ (ν (w ⊥)) → X ≬ (ν (w ⊥))
lemma-4-10 I w X = InteractionSystems.execution.lemma w X


--
-- comonad structure for w ↦ w *
module proposition-4-11 (I : Set) (w : IS I) where
  epsilon : (w *) ⊸ w
  epsilon = RTC.comonad.epsilon w

  delta : (w *) ⊸ (w * *)
  delta = RTC.comonad.delta w

  -- Is it possible to prove the comonad laws in intensional type theory?
  --


--
-- composition of general simulations
-- only the fact that
--  eval (epsilon w) ≈ "the mediating morphism ν (w * ⊥) ⊂ ν (w ⊥)
-- is formalized
proposition-4-14 :  (I : Set) (w : IS I) (i : I) (T : ν (w * ⊥) i) →
        lemma-4-3 (w *) w (proposition-4-11.epsilon I w) i i refl T
        ≈
        νIntro (ν (w * ⊥)) (lemma-4-7.elim w) T
proposition-4-14 I w i T = RTC.eval-epsilon.lemma w fun-ext T



--------------------------------------
-- layering and layered simulations --
--------------------------------------

--
-- layering is defined in file Layering.agda

--
-- layering transform an infinite branching structure into an infinte
-- linear structure

-- To make defining evaluation easier, we prove a slightly different
-- version than what appears in the paper: instead of using
-- ⟨ LayeredTS w i₀ ⟩ (written "⟪ w , i₀ ⟫ in the paper), we use
-- [ LayeredTS w i₀ ] ⊥ which is isomorphic:
--   - ⟨ ... ⟩ has trivial reactions
--   - [ ... ] has trivial actions
-- The two are simply related by duality.
-- The proof corresponding to that of the paper can be found in file Layering/WTC-bis.agda
module lemma-5-3 (I : Set) (w : IS I) (i₀ : I) where

  open IS (w #) using () renaming (Command to A#)

  C : Pow (A# i₀)
  C = νextend w i₀

  W : IS (A# i₀)
  W = [ LayeredTS w i₀ ] ⊥

  elim : C ⊂ ⟦ W ⟧ C
  elim = Layering.WTC.elim w i₀

  intro : (X : Pow (A# i₀)) → (coalg : X ⊂ ⟦ W ⟧ X) → X ⊂ C
  intro = Layering.WTC.intro w i₀

  comp :  (X : Pow (A# i₀)) → (coalg : X ⊂ ⟦ W ⟧ X) (α : A# i₀) (x : X α) →
       elim (intro X coalg x)
       ≡
       functoriality W X C (intro X coalg) (coalg x)
  comp = Layering.WTC.comp w i₀

  wtc : WTC W C
  wtc = record {
      elim = elim ;
      intro = intro ;
      comp = comp }


--
-- if w has trivial reactions, then ν w is a weakly terminal coalgebra for ⟦ w ⊥ ⊥ ⟧
module lemma-5-5 (I : Set) (v : TS I) where

  -- an interaction system with trivial reactions is obtained as the "angelic update"
  -- of a transition system (this is the case for ⟨⟨ w , i₀ ⟩⟩ in the paper)
  w : IS I
  w = ⟨ v ⟩

  elim : ν w ⊂ ⟦ w ⊥ ⊥ ⟧ (ν w)
  elim = InteractionSystems.properties.update-duality-WTC.elim v

  intro : (X : Pow I) → (X ⊂ ⟦ w ⊥ ⊥ ⟧ X) → X ⊂ ν w
  intro X coalg = InteractionSystems.properties.update-duality-WTC.intro v coalg

  comp : (X : Pow I) (coalg : X ⊂ ⟦ w ⊥ ⊥ ⟧ X) → (i : I) → (x : X i) →
          elim (intro X coalg x)
          ≡
          functoriality (w ⊥ ⊥) X (ν w) (intro X coalg) (coalg x)
  comp X coalg i x = InteractionSystems.properties.update-duality-WTC.comp v X coalg i x

  wtc : WTC (⟨ v ⟩ ⊥ ⊥) (ν ⟨ v ⟩)
  wtc = record {
      elim = elim ;
      intro = intro ;
      comp = comp }

--
-- evaluation of general layered simulations
-- Because we use "[ LayeredTS ... ]" rather than "⟨ LayeredTS ... ⟩ ⊥", we don't
-- need to use the functions ⟨ LayeredTS ... ⟩ ↔ ⟨ LayeredTS ... ⟩ ⊥ ⊥
theorem-5-8 : {I₁ I₂ : Set} (w₁ : IS I₁) (w₂ : IS I₂) →
            (i₁ : I₁) → (i₂ : I₂) →
            (S : ([ LayeredTS (w₁ ⊥) i₁ ] *) ⊸ [ LayeredTS (w₂ ⊥) i₂ ] ) →
            let open Simulation S using (R) in
            R Leaf Leaf →
            ν (w₁ ⊥) i₁ → ν (w₂ ⊥) i₂
theorem-5-8 {I₁} {I₂} w₁ w₂ i₁ i₂ S r T₁ =
  let open IS (w₁ ⊥ #) using () renaming (Command to A₁#) in
  let T₁' : νextend (w₁ ⊥) i₁ Leaf
      T₁' = λ _ → T₁ in
  let T₁'' : ν ([ LayeredTS (w₁ ⊥) i₁ ] ⊥) Leaf
      T₁'' = νIntro (νextend (w₁ ⊥) i₁) (lemma-5-3.elim I₁ (w₁ ⊥) i₁) T₁' in
  let T₂'' : ν ([ LayeredTS (w₂ ⊥) i₂ ] ⊥) Leaf
      T₂'' = eval* [ LayeredTS (w₁ ⊥) i₁ ] [ LayeredTS (w₂ ⊥) i₂ ] S Leaf Leaf r T₁'' in
  let T₂' : νextend (w₂ ⊥) i₂ Leaf
      T₂' = lemma-5-3.intro I₂ (w₂ ⊥) i₂ (ν ([ LayeredTS (w₂ ⊥) i₂ ] ⊥)) νElim T₂'' in
  let T₂ : ν (w₂ ⊥) i₂
      T₂ = T₂' ⋆ in
  T₂


-- EOF --
---------