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

-- This version of Interval 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
open import Relation.Unary
open import Agda.Primitive
open import Data.Product
open import Relation.Nullary
open import Data.Sum hiding (map₂)
open import Function

module Interval (Inst : StrictPartialOrder lzero lzero lzero) where

open import Instant Inst public

data Interval : Set where
  ⟦_-_⟧ : (α β : Support)  Interval
  ⟦_-∞⟦ : (α : Support)  Interval

_∈ᵢ_ : Support  Interval  Set
v ∈ᵢ  α -∞⟦ = α  v
v ∈ᵢ  α - β  = α  v × ¬ (β  v)

inf : Interval  Support
inf  α - _  = α
inf  α -∞⟦ = α

_⊂ᵢ_ : Rel Interval _
I ⊂ᵢ J = (_∈ᵢ I)  (_∈ᵢ J)

≈∈ :  {i₁ i₂ I}  i₁  i₂  i₁ ∈ᵢ I  i₂ ∈ᵢ I
≈∈ {I =  α - β } i₁≈i₂ (α≼i₁ , ¬β≺i₁)
  = ≼-resp-≈₁ i₁≈i₂ α≼i₁ ,
     β≺i₂  ¬β≺i₁ (≺-resp-≈₁ (sym≈ i₁≈i₂) β≺i₂))
≈∈ {I =  α -∞⟦} i₁≈i₂ (inj₁ α≈i₁) = inj₁ (trans≈ α≈i₁ i₁≈i₂)
≈∈ {I =  α -∞⟦} i₁≈i₂ (inj₂ α≺i₁) = inj₂ (≺-resp-≈₁ i₁≈i₂ α≺i₁)

trans⊂ : Transitive _⊂ᵢ_
trans⊂ u v = v  u

sameB :  {i j k}  j  k  i ∈ᵢ  j - k   i  j
sameB j≈k = sym≈  (uncurry ≼→¬≺→≈)  map₂ (_∘ (≺-resp-≈₂ j≈k))