module Order where

open import Equality
open import EquationalReasoning
open import Function
open import Level
open import Proposition
open import Sum
open import UIP

----------------------------------------------------------------------
-- Partial orders
----------------------------------------------------------------------
record Poset {ℓ : Level}(A : Set ℓ) : Set (lsuc ℓ) where
  infix  _≤_
  field
    _≤_ : A → A → Set ℓ
    instance {{≤isProp}} : {x y : A} → isProp (x ≤ y)
    ≤refl  : (x : A) → x ≤ x
    ≤trans : {x y z : A} → x ≤ y → y ≤ z → x ≤ z
    ≤antisymm : {x y : A} → x ≤ y → y ≤ x → x ≡ y
    
open Poset{{...}} public

{-# DISPLAY Poset._≤_ _ x y = x ≤ y #-}

----------------------------------------------------------------------
-- Total orders
----------------------------------------------------------------------
record Order {ℓ : Level}(A : Set ℓ) : Set (lsuc ℓ) where
  field
    instance {{po}} : Poset A
    ≤tot            : (x y : A) → x ≤ y or y ≤ x

open Order{{...}} public

-- Case analysis on ≤
≤ind :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  {{_ : Order A}}
  (B : A → Set ℓ')
  (_ : (x : A) → isProp (B x))
  (x : A)
  (_ : {y : A} → y ≤ x → B y)
  (_ : {y : A} → x ≤ y → B y)
  → ----------------------------
  (y : A) → B y
≤ind {{α}} B β x f g y =
  orrec
    f
    g
    (λ _ _ → cong f (≤isProp {{po {{α}}}}))
    (λ _ _ → cong g (≤isProp {{po {{α}}}}) )
    (λ _ _ → β y)
    (≤tot y x)

-- Branch on ≤
infix  if≤then_else_by_
if≤then_else_by_ :
   {ℓ ℓ' : Level}
   {A : Set ℓ}
   {{_ : Order A}}
   {B : Set ℓ'}
   (f g : A → A → B)
   (e : (x : A) → f x x ≡ g x x)
   → --------------------------
   A → A → B
(if≤then f else g by e) x y =
  orrec
    (λ _ → f x y)
    (λ _ → g x y)
    (λ _ _ → refl)
    (λ _ _ → refl)
    (λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x))
    (≤tot x y)

if≤then-l :
   {ℓ ℓ' : Level}
   {A : Set ℓ}
   {{_ : Order A}}
   {B : Set ℓ'}
   (f g : A → A → B)
   (e : (x : A) → f x x ≡ g x x)
   {x y : A}
   → -----------------------------------------
   x ≤ y → (if≤then f else g by e) x y ≡ f x y
if≤then-l f g e {x} {y} u =
  let h = orrec
        (λ _ → f x y)
        (λ _ → g x y)
        (λ _ _ → refl)
        (λ _ _ → refl)
        (λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x))
  in
  proof:
    h (≤tot x y)
  ≡[ cong h (∥∥isProp) ]
    h (inl u mod∇)
  ≡[ orcompl (λ _ → f x y) (λ _ → g x y) (λ _ _ → refl) (λ _ _ → refl)
     (λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x)) u ]
    f x y
  qed

if≤then-r :
   {ℓ ℓ' : Level}
   {A : Set ℓ}
   {{_ : Order A}}
   {B : Set ℓ'}
   (f g : A → A → B)
   (e : (x : A) → f x x ≡ g x x)
   {x y : A}
   → -----------------------------------------
   y ≤ x → (if≤then f else g by e) x y ≡ g x y
if≤then-r f g e {x} {y} u =
  let h = orrec
        (λ _ → f x y)
        (λ _ → g x y)
        (λ _ _ → refl)
        (λ _ _ → refl)
        (λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x))
  in
  proof:
    h (≤tot x y)
  ≡[ cong h (∥∥isProp) ]
    h (inr u mod∇)
  ≡[ orcompr (λ _ → f x y) (λ _ → g x y) (λ _ _ → refl) (λ _ _ → refl)
     (λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x)) u ]
    g x y
  qed

∘if≤then :
   {ℓ ℓ' ℓ'' : Level}
   {A : Set ℓ}
   {{_ : Order A}}
   {B : Set ℓ'}
   {C : Set ℓ''}
   (f g : A → A → B)
   (e : (x : A) → f x x ≡ g x x)
   (h : B → C)
   (x y : A)
   → -----------------------------------------------------
   h ((if≤then f else g by e) x y) ≡
   (if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
∘if≤then {ℓ'' = ℓ''} {A} f g e h x = ≤ind E (λ _ → uip) x f' g'
  where
  E : A → Set ℓ''
  E y =
    h ((if≤then f else g by e) x y) ≡
    (if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
    
  f' : {y : A} → y ≤ x → E y
  f' {y} u =
    proof:
      h ((if≤then f else g by e) x y)
    ≡[ cong h (if≤then-r f g e u) ]
      h (g x y)
    ≡[ symm (if≤then-r (h ∘₂ f ) (h ∘₂ g) (λ x → cong h (e x)) u ) ]
      (if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
    qed

  g' : {y : A} → x ≤ y → E y
  g' {y} v =
    proof:
      h ((if≤then f else g by e) x y)
    ≡[ cong h (if≤then-l f g e v) ]
      h (f x y)
    ≡[ symm (if≤then-l (h ∘₂ f ) (h ∘₂ g) (λ x → cong h (e x)) v ) ]
      (if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
    qed