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

-- This version of Refinement 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 Data.Sum
open import Data.Product
open import Relation.Binary
open import Relation.Binary.Construct.Union
open import Agda.Primitive
open import Function
open import Relation.Binary.PropositionalEquality

module Refinement {a} {I : Set a} where

record Transform {} (≈₁ ≈₂ ≺₁ ≺₂ : Rel I )
  (T≈₁₂ T≈₂₁ T≺₁₂ T≺₂₁ : _  _  Rel I ) : Set (lsuc a  ) where
  field
     ≈₁→₂ : ≈₁  T≈₁₂ ≈₂ ≺₂
     ≈₂→₁ : ≈₂  T≈₂₁ ≈₁ ≺₁
     ≺₁→₂ : ≺₁  T≺₁₂ ≈₂ ≺₂
     ≺₂→₁ : ≺₂  T≺₂₁ ≈₁ ≺₁

open Transform public

_≈≈_ :  {}  Rel (Rel I  × Rel I ) _
(≈₁ , ≺₁) ≈≈ (≈₂ , ≺₂) = Transform ≈₁ ≈₂ ≺₁ ≺₂
     ≈₂ _  ≈₂)
     ≈₁ _  ≈₁)
     _ ≺₂  ≺₂)
     _ ≺₁  ≺₁)

_≺≈_ :  {}  Rel (Rel I  × Rel I ) _
(≈₁ , ≺₁) ≺≈ (≈₂ , ≺₂) = Transform ≈₁ ≈₂ ≺₁ ≺₂
     ≈₂ _  ≈₂)
     ≈₁ ≺₁  ≈₁  (≺₁  flip ≺₁))
     ≈₂ ≺₂  ≺₂  ≈₂)
     _ ≺₁  ≺₁)

refl≈≈ :  {}  Reflexive (_≈≈_ {})
refl≈≈ = record
  { ≺₁→₂ = id ; ≺₂→₁ = id ; ≈₁→₂ = id ; ≈₂→₁ = id }

sym≈≈ :  {}  Symmetric (_≈≈_ {})
sym≈≈ x≈≈y .≈₁→₂ = ≈₂→₁ x≈≈y
sym≈≈ x≈≈y .≈₂→₁ = ≈₁→₂ x≈≈y
sym≈≈ x≈≈y .≺₁→₂ = ≺₂→₁ x≈≈y
sym≈≈ x≈≈y .≺₂→₁ = ≺₁→₂ x≈≈y

trans≈≈ :  {}  Transitive (_≈≈_ {})
trans≈≈ i≈≈j j≈≈k .≈₁→₂ = (≈₁→₂ j≈≈k)  ≈₁→₂ i≈≈j
trans≈≈ i≈≈j j≈≈k .≈₂→₁ = (≈₂→₁ i≈≈j)  ≈₂→₁ j≈≈k
trans≈≈ i≈≈j j≈≈k .≺₁→₂ = (≺₁→₂ j≈≈k)  ≺₁→₂ i≈≈j
trans≈≈ i≈≈j j≈≈k .≺₂→₁ = (≺₂→₁ i≈≈j)  ≺₂→₁ j≈≈k

equiv≈≈ :  {}  IsEquivalence (_≈≈_ {})
equiv≈≈ = record { refl = refl≈≈ ; sym = sym≈≈ ; trans = trans≈≈ }

trans≺≈ :  {}  Transitive (_≺≈_ {})
trans≺≈ i≺≈j j≺≈k .≈₁→₂ = (≈₁→₂ j≺≈k)  ≈₁→₂ i≺≈j
trans≺≈ i≺≈j j≺≈k .≈₂→₁ x with ≈₂→₁ j≺≈k x
trans≺≈ i≺≈j _ .≈₂→₁ _ | inj₁ y = ≈₂→₁ i≺≈j y
trans≺≈ i≺≈j _ .≈₂→₁ _ | inj₂ (inj₁ y) = inj₂ (inj₁ (≺₂→₁ i≺≈j y))
trans≺≈ i≺≈j _ .≈₂→₁ _ | inj₂ (inj₂ y) = inj₂ (inj₂ (≺₂→₁ i≺≈j y))
trans≺≈ i≺≈j _ .≺₁→₂ x with ≺₁→₂ i≺≈j x
trans≺≈ _ j≺≈k .≺₁→₂ _ | inj₁ y = ≺₁→₂ j≺≈k y
trans≺≈ _ j≺≈k .≺₁→₂ _ | inj₂ y = inj₂ (≈₁→₂ j≺≈k y)
trans≺≈ i≺≈j j≺≈k .≺₂→₁ = (≺₂→₁ i≺≈j)  ≺₂→₁ j≺≈k

refl≺≈ :  {}  (_≈≈_ {})  (_≺≈_ {})
refl≺≈ i≈≈j .≈₁→₂ = ≈₁→₂ i≈≈j
refl≺≈ i≈≈j .≈₂→₁ = inj₁  ≈₂→₁ i≈≈j
refl≺≈ i≈≈j .≺₁→₂ = inj₁  ≺₁→₂ i≈≈j
refl≺≈ i≈≈j .≺₂→₁ = ≺₂→₁ i≈≈j

preorder≺≈≈ :  {}  IsPreorder _≈≈_ (_≺≈_ {})
preorder≺≈≈ = record {
  isEquivalence = equiv≈≈ ;
  reflexive = refl≺≈ ;
  trans = trans≺≈ }

antisym≺≈ :  {}  Antisymmetric _≈≈_ (_≺≈_ {})
antisym≺≈ i≺≈j _ .≈₁→₂ = ≈₁→₂ i≺≈j
antisym≺≈ _ j≺≈i .≈₂→₁ = ≈₁→₂ j≺≈i
antisym≺≈ _ j≺≈i .≺₁→₂ = ≺₂→₁ j≺≈i
antisym≺≈ i≺≈j _ .≺₂→₁ = ≺₂→₁ i≺≈j

partialOrder≺≈≈ :  {}  IsPartialOrder _≈≈_ (_≺≈_ {})
partialOrder≺≈≈ = record {
  isPreorder = preorder≺≈≈ ;
  antisym = antisym≺≈ }