-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of CCSLRefinement is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

open import Relation.Binary.Core
open import Relation.Binary
open import Refinement
open import Data.Product
open import Data.Sum hiding (map₂) renaming (swap to swap⊎)
open import Function
open import Helper
open import Relation.Binary.PropositionalEquality
open import Data.Empty

module CCSLRefinement (Support : Set)
  {_≈₁_ _≈₂_ _≺₁_ _≺₂_ : Rel Support _}
  (ispo₁ : IsStrictPartialOrder _≈₁_ _≺₁_)
  (ispo₂ : IsStrictPartialOrder _≈₂_ _≺₂_)
  (refines : (_≈₁_ , _≺₁_) ≺≈ (_≈₂_ , _≺₂_))  where

open import CCSL (record {isStrictPartialOrder = ispo₁}) as 
open import CCSL (record {isStrictPartialOrder = ispo₂}) as 

≼₁→₂ : ₁._≼_  ₂._≼_
≼₁→₂ (inj₁ i≈₁j) = inj₁ (≈₁→₂ refines i≈₁j)
≼₁→₂ (inj₂ i≺₁j) = swap⊎ (≺₁→₂ refines i≺₁j)

_≲₁◅ₙ_ : REL ₁.Clock ₂.Clock _
(Ticks₁  _) ≲₁◅ₙ (Ticks₂  _) = 
   (∀ (y :  Ticks₂)   λ (x :  Ticks₁)  x ₂.≈' y) ×
   (∀ (x :  Ticks₁)   λ (y :  Ticks₂)  y ₂.≈' x)

e∘a≡id :  {c₁ c₂} (p : c₁ ≲₁◅ₙ c₂)  (∀ {i :  (Ticks c₂)} 
  i ₂.≡' (proj₁  proj₂ p  proj₁  (proj₁ p)) i)
e∘a≡id (u , _) {i} with u i
e∘a≡id (_ , v) | j , j≈₂i with v j
e∘a≡id {c₂ = c₂} _ {i} | _ , j≈₂i | k , k≈₂j =
  ₂.≈→≡ {c₂} {i} {k} (₂.sym≈ (₂.trans≈ k≈₂j j≈₂i))

⊑≲₁◅ₙ :  {c₁₁ c₁₂ c₂₁ c₂₂} 
  c₁₁ ₁.⊑ c₁₂  c₁₁ ≲₁◅ₙ c₂₁  c₁₂ ≲₁◅ₙ c₂₂  c₂₁ ₂.⊑ c₂₂
⊑≲₁◅ₙ o (p , _) (_ , s) i₂₁ = (i₂₁ , ₂.refl≈)
  >[ id -⟦ ₂.trans≈ ⟧- ₂.sym≈ ]> p
  >[ id -⟦ ₂.trans≈ ⟧- ≈₁→₂ refines ]> o
  >[ id -⟦ ₂.trans≈ ⟧- ₂.sym≈ ]> s

♯≲₁◅ₙ :  {c₁₁ c₁₂ c₂₁ c₂₂} 
  c₂₁ ₂.♯ c₂₂  c₁₁ ≲₁◅ₙ c₂₁  c₁₂ ≲₁◅ₙ c₂₂  c₁₁ ₁.♯ c₁₂
♯≲₁◅ₙ p (q , r) (s , t) x y x≈₁y with r x | t y
♯≲₁◅ₙ p (q , r) (s , t) x y x≈₁y | rx , rx≈₂x | ty , ty≈₂y =
  p rx ty (₂.trans≈ (₂.trans≈ rx≈₂x (≈₁→₂ refines x≈₁y)) (₂.sym≈ ty≈₂y))

⋃≲₁◅ₙ :  {c₁₁ c₁₀ c₁₂ c₂} 
  c₁₁ ≲₁◅ₙ c₂  c₁₂ ≲₁◅ₙ c₂  c₁₀ ₁.≋ c₁₁  c₁₂  c₁₀ ≲₁◅ₙ c₂
⋃≲₁◅ₙ (p , _) _ (_ , u) .proj₁ x = (x , ₂.refl≈)
  >[ flip ₂.trans≈ ]> p
  >[ id -⟦ flip ₂.trans≈ ⟧- (₂.sym≈  ≈₁→₂ refines) ]> u  map₂ inj₁
⋃≲₁◅ₙ _ _ (t , _) .proj₂ x with t x
⋃≲₁◅ₙ (_ , q) _ _ .proj₂ _ | ((i , inj₁ tc₁₁i) , i≈₁x) =
  ((i , tc₁₁i) , ≈₁→₂ refines i≈₁x) >[ flip ₂.trans≈ ]> q
⋃≲₁◅ₙ _ (_ , s) _ .proj₂ _ | ((i , inj₂ tc₁₂i) , i≈₁x) =
  ((i , tc₁₂i) , ≈₁→₂ refines i≈₁x) >[ flip ₂.trans≈ ]> s

∽≲₁◅ₙ :  {c₁ c₂₁ c₂₂}  c₁ ≲₁◅ₙ c₂₁  c₁ ≲₁◅ₙ c₂₂  c₂₁ ₂.∽ c₂₂
∽≲₁◅ₙ (p , _) (_ , s) .proj₁ x = (x , ₂.refl≈)
  >[ id -⟦ ₂.trans≈ ⟧- ₂.sym≈ ]> p
  >[ id -⟦ ₂.trans≈ ⟧- ₂.sym≈ ]> s
∽≲₁◅ₙ (_ , q) (r , _) .proj₂ x = (x , ₂.refl≈)
  >[ id -⟦ ₂.trans≈ ⟧- ₂.sym≈ ]> r
  >[ id -⟦ ₂.trans≈ ⟧- ₂.sym≈ ]> q

_≲₁◅₁_ : REL ₁.Clock ₂.Clock _
(Ticks₁  _) ≲₁◅₁ (Ticks₂  _) = 
   (∀ (y :  Ticks₂)  ∃! (₁._≈'_) λ (x :  Ticks₁)  x ₂.≈' y) ×
   (∀ (x :  Ticks₁)   λ (y :  Ticks₂)  y ₂.≈' x)

≲→≲₁◅₁ :  {c₁ c₂}  c₁ ≲₁◅₁ c₂  c₁ ≲₁◅ₙ c₂
≲→≲₁◅₁ (p , q) = ∃!→∃  p , q

≲₁◅₁→≈₂→₁ :  {c₁₁ c₂₁}  c₁₁ ≲₁◅₁ c₂₁  {k l :  (Ticks c₁₁)}
   k ₂.≈' l  k ₁.≈' l
≲₁◅₁→≈₂→₁ {c₁₁} {c₂₁} (p , q) {k} {l} k≈₂l with q k | q l
... | u , u≈₂k | v , v≈₂l with ₂.≈→≡ {c₂₁} {u} {v}
  (₂.trans≈ (₂.trans≈ u≈₂k k≈₂l) (₂.sym≈ v≈₂l))
... | refl with p u
... | j , j≈₂u , ∃! =
  ₁.trans≈ (₁.sym≈ (∃! {k} (₂.sym≈ u≈₂k))) (∃! {l} (₂.sym≈ v≈₂l))

≲₁◅₁→≺₁→₂ :  {c₁₁ c₂₁}  c₁₁ ≲₁◅₁ c₂₁  {k l :  (Ticks c₁₁)}
   k ₁.≺' l  k ₂.≺' l
≲₁◅₁→≺₁→₂ {c₁₁} {c₂₁} p {k} {l} k≺₁l with ≺₁→₂ refines k≺₁l
... | inj₁ k≺₂l = k≺₂l
... | inj₂ k≈₂l =
  ⊥-elim (₁.irrefl≈≺ (≲₁◅₁→≈₂→₁ {c₁₁} {c₂₁} p {k} {l} k≈₂l) k≺₁l)

a∘e≡id :  {c₁ c₂} (p : c₁ ≲₁◅₁ c₂)  (∀ {i :  (Ticks c₁)} 
  i ₂.≡' (proj₁  proj₁ p  proj₁  (proj₂ p)) i)
a∘e≡id (_ , v) {i} with v i
a∘e≡id (u , _) | j , j≈₂i with u j
a∘e≡id {c₁} {c₂} p {i} | j , j≈₂i | k , k≈₂j , _ =
  ₁.≈→≡ {c₁} {i} {k} (≲₁◅₁→≈₂→₁ {c₁} {c₂} p {i} {k}
    (₂.sym≈ (₂.trans≈ k≈₂j j≈₂i)))

≺≺₂→≺≺₁ :  {c₁₁ c₁₂ c₂₁ c₂₂}  c₁₁ ≲₁◅₁ c₂₁  c₁₂ ≲₁◅₁ c₂₂
   c₂₁ ₂.≺≺ c₂₂  c₁₁ ₁.≺≺ c₁₂

≺≺₂→≺≺₁ (p , _) (_ , q₁) prec .h = proj₁  p  h prec  proj₁  q₁
≺≺₂→≺≺₁ {c₁₁} {_} {c₂₁} (p , q) (_ , q₁) prec .congruent {i} {j} i≈₁j
  with q₁ i | q₁ j ; ... | i₁ , i₁≈₂i | j₁ , j₁≈₂j with p (h prec i₁) | p (h prec j₁)
... | i₃ , i₃≈₂i₂ , _ | j₃ , j₃≈₂j₂ , _ with ≈₁→₂ refines i≈₁j
... | i≈₂j with ₂.trans≈ (₂.trans≈ i₁≈₂i i≈₂j) (₂.sym≈ j₁≈₂j)
... | i₁≈₂j₁ with congruent prec {i₁} {j₁} i₁≈₂j₁
... | i₂≈₂j₂ with ₂.trans≈ i₃≈₂i₂ (₂.trans≈ i₂≈₂j₂ (₂.sym≈ j₃≈₂j₂))
... | i₃≈₂j₃ = ≲₁◅₁→≈₂→₁ {c₁₁} {c₂₁} (p , q) {i₃} {j₃} i₃≈₂j₃
≺≺₂→≺≺₁ (p , _) (_ , q₁) prec .precedes i with q₁ i
... | j , j≈₂i with p (h prec j)
... | _ , k≈₂hj , _ with precedes prec j
... | hj≺₂j with ₂.≺≈≈→≺ hj≺₂j (₂.sym≈ k≈₂hj) j≈₂i
... | k≺₂i = ≺₂→₁ refines k≺₂i
≺≺₂→≺≺₁ {_} {c₁₂} {_} {c₂₂} _ q _ .preserves {i} {j} i≺₁j
  with ≲₁◅₁→≺₁→₂ {c₁₂} {c₂₂} q {i} {j} i≺₁j
≺≺₂→≺≺₁ (p , _) (_ , q₁) prec .preserves {i} {j} _ | i≺₂j with q₁ i | q₁ j
... | i₁ , i₁≈i | j₁ , j₁≈j  with p (h prec i₁) | p (h prec j₁)
... | _ , i₃≈₂i₂ , _ | _ , j₃≈₂j₂ , _
  with ₂.≺≈≈→≺ i≺₂j (₂.sym≈ i₁≈i) (₂.sym≈ j₁≈j)
... | i₁≺₂j₁ with preserves prec {i₁} {j₁} i₁≺₂j₁
... | i₂≺₂j₂ with ₂.≺≈≈→≺ i₂≺₂j₂ (₂.sym≈ i₃≈₂i₂) (₂.sym≈ j₃≈₂j₂)
... | i₃≺₂j₃ = ≺₂→₁ refines i₃≺₂j₃
≺≺₂→≺≺₁ {c₁₁} {c₁₂} {c₂₁} {c₂₂} (p , q) (p₁ , q₁) prec .dense
  {i₀} {j₀} {k₃} i₃≺₁k₃ k₃≺₁j₃ with q₁ i₀ | q₁ j₀ | q k₃
... | i₁ , i₁≈₂i | j₁ , j₁≈₂j | k₂ , k₂≈₂k₃
  with p (h prec i₁) | p (h prec j₁)
... | i₃ , i₃≈₂i₂ , _ | j₃ , j₃≈₂j₂ , _
  with ≲₁◅₁→≺₁→₂ {c₁₁} {c₂₁} (p , q) {i₃} {k₃} i₃≺₁k₃
... | i₃≺₂k₃ with ≲₁◅₁→≺₁→₂ {c₁₁} {c₂₁} (p , q) {k₃} {j₃} k₃≺₁j₃
... | k₃≺₂j₃ with ₂.≺≈≈→≺ i₃≺₂k₃ i₃≈₂i₂ (₂.sym≈ k₂≈₂k₃)
... | i₂≺₂k₂ with ₂.≺≈≈→≺ k₃≺₂j₃ (₂.sym≈ k₂≈₂k₃) j₃≈₂j₂
... | k₂≺₂j₂ with dense prec {i₁} {j₁} {k₂} i₂≺₂k₂ k₂≺₂j₂
... | k₁ , hk₁≈₂k₂ with p₁ k₁
... | k₀ , k₀≈₂k₁ , _ with ₂.trans≈ (proj₂ (q₁ k₀)) k₀≈₂k₁
... | qk₀≈₂k₁ with congruent prec {proj₁ (q₁ k₀)} {k₁} qk₀≈₂k₁
... | hqk₀≈₂hk₁ with ₂.trans≈ (₂.trans≈ hqk₀≈₂hk₁ hk₁≈₂k₂) k₂≈₂k₃
... | hqk₀≈₂k₃ with ₂.trans≈
  (proj₁ (proj₂ (p (h prec (proj₁ (q₁ k₀)))))) hqk₀≈₂k₃
... | phqk₀≈₂k₃ = k₀ , ≲₁◅₁→≈₂→₁ {c₁₁} {c₂₁} (p , q)
  {proj₁ (p (h prec (proj₁ (q₁ k₀))))} {k₃} phqk₀≈₂k₃

prec₁→≼≼₂ :  {c₁₁ c₁₂ c₂₁ c₂₂} {_R_ : Rel ₁.Support _}
   _R_  ₁._≼_  c₁₁ ≲₁◅₁ c₂₁  c₁₂ ≲₁◅₁ c₂₂
   ₁.Precedence _R_ c₁₁ c₁₂  c₂₁ ₂.≼≼ c₂₂

prec₁→≼≼₂ _ (p , q) (p₁ , q₁) prec .h = proj₁  q  h prec  proj₁  p₁
prec₁→≼≼₂ {_} {c₁₂} {_} {c₂₂} _ (p , q) (p₁ , q₁) prec .congruent
  {i₀} {j₀} i₀≈₂j₀ with p₁ i₀ | p₁ j₀
... | i₁ , i₁≈₂i₀ , _ | j₁ , j₁≈₂j₀ , _ with q (h prec i₁) | q (h prec j₁)
... | i₃ , i₃≈₂hi₁ | j₃ , j₂≈₂hj₁
  with ₂.trans≈ i₁≈₂i₀ (₂.trans≈ i₀≈₂j₀ (₂.sym≈ j₁≈₂j₀))
... | i₁≈₂j₁ with ≲₁◅₁→≈₂→₁ {c₁₂} {c₂₂} (p₁ , q₁) {i₁} {j₁} i₁≈₂j₁
... | i₁≈₁j₁ with ≈₁→₂ refines (congruent prec {i₁} {j₁} i₁≈₁j₁)
... | hi₁≈₂hj₁ = ₂.trans≈ i₃≈₂hi₁ (₂.trans≈ hi₁≈₂hj₁ (₂.sym≈ j₂≈₂hj₁))
prec₁→≼≼₂ R⇒≼₁ (p , q) (p₁ , q₁) prec .precedes i₀ with p₁ i₀
... | i₁ , i₁≈₂i₀ , _ with precedes prec i₁
... | hi₁Ri₁ with ≼₁→₂ (R⇒≼₁ hi₁Ri₁) 
... | hi₁≼₂i₁ with q (h prec i₁)
... | i₃ , i₃≈₂hi₁ = ₂.trans≼ (inj₁ i₃≈₂hi₁) (₂.trans≼ hi₁≼₂i₁ (inj₁ i₁≈₂i₀))
prec₁→≼≼₂ {c₁₁} {_} {c₂₁} _ (p , q) (p₁ , q₁) prec .preserves
  {i₀} {j₀} i₀≺₂j₀ with p₁ i₀ | p₁ j₀
... | i₁ , i₁≈₂i₀ , _ | j₁ , j₁≈₂j₀ , _ with q (h prec i₁) | q (h prec j₁)
... | i₃ , i₃≈₂hi₁ | j₃ , j₂≈₂hj₁
  with ₂.≺≈≈→≺ i₀≺₂j₀ (₂.sym≈ i₁≈₂i₀) (₂.sym≈ j₁≈₂j₀)
... | i₁≺₂j₁ with ≺₂→₁ refines i₁≺₂j₁
... | i₁≺₁j₁ with preserves prec {i₁} {j₁} i₁≺₁j₁
... | hi₁≺₁hj₁ with
  ≲₁◅₁→≺₁→₂ {c₁₁} {c₂₁} (p , q) {h prec i₁} {h prec j₁} hi₁≺₁hj₁
... | hi₁≺₂hj₁ = ₂.≺≈≈→≺ hi₁≺₂hj₁ (₂.sym≈ i₃≈₂hi₁) (₂.sym≈ j₂≈₂hj₁)
prec₁→≼≼₂ {_} {c₁₂} {_} {c₂₂} _ (p , q) (p₁ , q₁) prec .dense
  {i₀} {j₀} {k₃} i₃≺₂k₃ k₃≺₂j₃ with p₁ i₀ | p₁ j₀ | p k₃
... | i₁ , i₁≈₂i₀ , _ | j₁ , j₁≈₂j₀ , _ | k₂ , k₂≈₂k₃ , _
  with q (h prec i₁) | q (h prec j₁)
... | i₃ , i₃≈₂i₂ | j₃ , j₃≈₂j₂
  with ≺₂→₁ refines (₂.≺≈≈→≺ i₃≺₂k₃ i₃≈₂i₂ (₂.sym≈ k₂≈₂k₃))
... | i₂≺₁k₂ with ≺₂→₁ refines (₂.≺≈≈→≺ k₃≺₂j₃ (₂.sym≈ k₂≈₂k₃) j₃≈₂j₂)
... | k₂≺₁j₂ with dense prec {i₁} {j₁} {k₂} i₂≺₁k₂ k₂≺₁j₂
... | k₁ , hk₁≈₁k₂ with q₁ k₁
... | k₀ , k₀≈₂k₁ with ₂.trans≈ (proj₁ (proj₂ (p₁ k₀))) k₀≈₂k₁
... | pk₀≈₂k₁
  with ≲₁◅₁→≈₂→₁ {c₁₂} {c₂₂} (p₁ , q₁) {proj₁ (p₁ k₀)} {k₁} pk₀≈₂k₁
... | pk₀≈₁k₁ with congruent prec {proj₁ (p₁ k₀)} {k₁} pk₀≈₁k₁
... | hpk₀≈₁hk₁ with ₂.trans≈ (₂.trans≈ (≈₁→₂ refines hpk₀≈₁hk₁)
  (≈₁→₂ refines hk₁≈₁k₂)) k₂≈₂k₃
... | hpk₀≈₂k₃ = k₀ , ₂.trans≈ (proj₂ (q (h prec (proj₁ (p₁ k₀))))) hpk₀≈₂k₃

≺≺₁→≼≼₂ :  {c₁₁ c₁₂ c₂₁ c₂₂}  c₁₁ ≲₁◅₁ c₂₁  c₁₂ ≲₁◅₁ c₂₂
   c₁₁ ₁.≺≺ c₁₂  c₂₁ ₂.≼≼ c₂₂
≺≺₁→≼≼₂ = prec₁→≼≼₂ inj₂

≼≼₁→≼≼₂ :  {c₁₁ c₁₂ c₂₁ c₂₂}  c₁₁ ≲₁◅₁ c₂₁  c₁₂ ≲₁◅₁ c₂₂
   c₁₁ ₁.≼≼ c₁₂  c₂₁ ₂.≼≼ c₂₂
≼≼₁→≼≼₂ = prec₁→≼≼₂ id