-- 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≺≈ }