{-# OPTIONS --rewriting #-}

module Interval where

open import Decidable
open import Equality
open import EqualityRewriting
open import EquationalReasoning
open import Level
open import Order
open import Proposition
open import Sum
open import UIP

----------------------------------------------------------------------
-- Interval
----------------------------------------------------------------------
infixr  _∸_
postulate
  𝕀 : Set

  -- 𝕀 is totally ordered
  instance 𝕀order : Order 𝕀

  -- 𝕀 has a least element
  O : 𝕀
  O≤ : ∀ {i} → O ≤ i

  -- 𝕀 has a greatest element
  I : 𝕀
  ≤I : ∀ {i} → i ≤ I

  -- 𝕀 has a weak form of monus
  _∸_ : 𝕀 → 𝕀 → 𝕀
  ∸≤ : ∀ {i j} → j ≤ i → i ∸ j ≤ i
  ∸∸ : ∀ {i j} → j ≤ i → i ∸ (i ∸ j) ≡ j
  ∸δ : ∀ i → i ∸ i ≡ O

  -- 𝕀 is non-trivial
  O≠I : ¬ (O ≡ I)

  -- 𝕀 is connected [not needed so far]
  -- conn𝕀 :
  --   {ℓ : Level}
  --   {P : 𝕀 → Set ℓ}
  --   (_ : (i : 𝕀) → Dec (P i))
  --   (i j : 𝕀)
  --   → -----------------------
  --   P i → P j

-- The following operations are definable from ≤ and ∸,
-- but postulating them makes it easier to declare some of their
-- properites as rewrites:

  -- minimum
  min : 𝕀 → 𝕀 → 𝕀
  minl : ∀ {i j} → i ≤ j → min i j ≡ i
  minr : ∀ {i j} → j ≤ i → min i j ≡ j

  -- maximum
  max : 𝕀 → 𝕀 → 𝕀
  maxl : ∀ {i j} → j ≤ i → max i j ≡ i
  maxr : ∀ {i j} → i ≤ j → max i j ≡ j

  -- interpolation
  cvx : 𝕀 → 𝕀 → 𝕀 → 𝕀
  cvxl : ∀ {i j k} → i ≤ k → cvx i j k ≡ min (max i j) k
         -- compatibility: if i ≡ k, then
         -- min (max i j) k ≡ i ≡ min i (max (I ∸ j) k)
  cvxr : ∀ {i j k} → k ≤ i → cvx i j k ≡ min i (max (I ∸ j) k)

  -- squash up
  ↑ : 𝕀 → 𝕀
  ↑l : ∀ {i} → i ≤ I ∸ i → ↑ i ≡ I ∸ ((I ∸ i) ∸ i)
  ↑r : ∀ {i} → I ∸ i ≤ i → ↑ i ≡ I
  -- squash down  
  ↓ : 𝕀 → 𝕀
  ↓l : ∀ {i} → i ≤ I ∸ i → ↓ i ≡ O
  ↓r : ∀ {i} → I ∸ i ≤ i → ↓ i ≡ i ∸ (I ∸ i)

----------------------------------------------------------------------
-- Rewriting properties of monus
----------------------------------------------------------------------
∸O : ∀ {i} → i ∸ O ≡ i
∸O {i} =
  proof:
    i ∸ O
  ≡[ cong (i ∸_) (symm (∸δ i)) ]
    i ∸ (i ∸ i)
  ≡[ ∸∸ (≤refl i) ] 
    i
  qed

∸∸I : ∀ {i} → I ∸ (I ∸ i) ≡ i
∸∸I = ∸∸ ≤I

{-# REWRITE ∸δ ∸O ∸∸I #-}

----------------------------------------------------------------------
-- Rewriting properties of minimum
----------------------------------------------------------------------
Omin : ∀ {i} → min O i ≡ O
Omin = minl O≤

Imin : ∀ {i} → min I i ≡ i
Imin {i} = minr ≤I

{-# REWRITE Omin Imin #-}

----------------------------------------------------------------------
-- Rewriting properties of interpolation
----------------------------------------------------------------------
cvxO : ∀ i j → cvx i O j ≡ i
cvxO i j =
  ≤ind (λ k → cvx i O k ≡ i) (λ _ → uip) i a b j
  where
  a : {k : 𝕀} → k ≤ i → cvx i O k ≡ i
  a {k} u =
    proof:
      cvx i O k
    ≡[ cvxr u ]
      min i (max (I ∸ O) k)
    ≡[ cong (λ j → min i (max j k)) ∸O ]
      min i (max I k)
    ≡[ cong (min i) (maxl ≤I) ]
      min i I
    ≡[ minl ≤I ]
      i
    qed

  b : {k : 𝕀} → i ≤ k → cvx i O k ≡ i
  b {k} v =
    proof:
      cvx i O k
    ≡[ cvxl v ]
      min (max i O) k
    ≡[ cong (λ j → min j k) (maxl O≤) ]
      min i k
    ≡[ minl v ]
      i
    qed

cvxI : ∀ i j → cvx i I j ≡ j
cvxI i j =
  ≤ind (λ k → cvx k I j ≡ j) (λ _ → uip) j a b i
  where
  a : {k : 𝕀} → k ≤ j → cvx k I j ≡ j
  a {k} u =
    proof:
      cvx k I j
    ≡[ cvxl u ]
      min (max k I) j
    ≡[ cong (λ i → min i j) (maxr ≤I) ]
      min I j
    ≡[ minr ≤I ]
      j
    qed

  b : {k : 𝕀} → j ≤ k → cvx k I j ≡ j
  b {k} v =
    proof:
      cvx k I j
    ≡[ cvxr v ]
      min k (max (I ∸ I) j)
    ≡[ cong (λ i → min k (max i j))(∸δ I) ]
      min k (max O j)
    ≡[ cong (min k) (maxr O≤) ]
      min k j
    ≡[ minr v ]
      j
    qed

cvxδ : ∀ i j → cvx i j i ≡ i
cvxδ i j =
  proof:
    cvx i j i
  ≡[ cvxl (≤refl i) ]
    min (max i j) i
  ≡[ minr i≤maxij ]
    i
  qed
  where
    i≤maxij : i ≤ max i j
    i≤maxij =
      ≤ind
        (λ k → k ≤ max k j)
        (λ k → ≤isProp {x = k} {max k j})
        j
        (λ {k} u → subst (k ≤_) (symm (maxr u)) u)
        (λ {k} v → subst (k ≤_) (symm (maxl v)) (≤refl k))
        i

cvxOI : ∀ i → cvx O i I ≡ i
cvxOI i =
  proof:
    cvx O i I
  ≡[ cvxl O≤ ]
    min (max O i) I
  ≡[ minl ≤I ]
    max O i
  ≡[ maxr O≤ ]
    i
  qed

{-# REWRITE cvxO cvxI cvxδ cvxOI #-}

----------------------------------------------------------------------
-- Rewrite properties of squash down/up
----------------------------------------------------------------------
↑O : ↑ O ≡ O
↑O = ↑l O≤

↑I : ↑ I ≡ I
↑I = ↑r ≤I

↓O : ↓ O ≡ O
↓O = ↓l O≤

↓I : ↓ I ≡ I
↓I = ↓r ≤I

{-# REWRITE ↑O ↑I ↓O ↓I #-}

----------------------------------------------------------------------
-- Prove properties of 𝕀 by branching over ↓or↑
----------------------------------------------------------------------
↓or↑ : ∀ i → (↓ i ≡ O) or (↑ i ≡ I)
↓or↑ i =
  orrec f g f' g' (λ _ _ → ∥∥isProp) (≤tot i (I ∸ i))
  where
  f : i ≤ I ∸ i → (↓ i ≡ O or ↑ i ≡ I)
  f p = (inl (↓l p)) mod∇
  f' : (p p' : i ≤ I ∸ i) → f p ≡ f p'
  f' p p' = cong f (≤isProp {x = i} {y = I ∸ i} {x = p} {y = p'})
  g : I ∸ i ≤ i → (↓ i ≡ O or ↑ i ≡ I)
  g q = (inr (↑r q)) mod∇ 
  g' : (q q' : I ∸ i ≤ i) → g q ≡ g q'
  g' q q' = cong g (≤isProp {x = I ∸ i} {y = i} {x = q} {y = q'})
  
module _
  {ℓ : Level}
  (P : 𝕀 → Set ℓ)
  (f : ∀ i → ↓ i ≡ O → P i)
  (g : ∀ i → ↑ i ≡ I → P i)
  (h : ∀ i → (u : ↓ i ≡ O)(v : ↑ i ≡ I) →  f i u ≡ g i v)
  where
  
  𝕀ind : ∀ i → P i
  𝕀ind i =
    orrec
      (f i)
      (g i)
      (λ _ _ → cong (f i) uip)
      (λ _ _ → cong (g i) uip)
      (h i)
      (↓or↑ i)
  
  𝕀ind↓ :
    (i : 𝕀)
    (u : ↓ i ≡ O)
    → ------------
    𝕀ind i ≡ f i u
  𝕀ind↓ i u =
    let
      f' = λ _ _ → cong (f i) uip
      g' = λ _ _ → cong (g i) uip
      p  = orrec (f i) (g i) f' g' (h i)
    in
    proof: 
      p (↓or↑ i)
    ≡[ cong p (∥∥isProp {x = ↓or↑ i} {y = inl u mod∇}) ]  
      p (inl u mod∇)
    ≡[ orcompl (f i) (g i) f' g' (h i) u  ]
      f i u
    qed
    
  𝕀ind↑ :
    (i : 𝕀)
    (v : ↑ i ≡ I)
    → ------------
    𝕀ind i ≡ g i v
  𝕀ind↑ i v =
    let
      f' = λ _ _ → cong (f i) uip
      g' = λ _ _ → cong (g i) uip
      p  = orrec (f i) (g i) f' g' (h i)
    in
    proof: 
      p (↓or↑ i)
    ≡[ cong p (∥∥isProp {x = ↓or↑ i} {y = inr v mod∇}) ]  
      p (inr v mod∇)
    ≡[ orcompr (f i) (g i) f' g' (h i) v  ]
      g i v
    qed

----------------------------------------------------------------------
-- Reversal operation
----------------------------------------------------------------------
rev : 𝕀 → 𝕀
rev i = cvx I i O