\import Data.Array
\import Data.Or
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set
\open JoinSemilattice
\open MeetSemilattice

\class TotalOrder \extends DistributiveLattice {
  | totality (x y : E) : x <= y || y <= x

  \default meet (x y : E) : E => (tmeet (totality x y)).
  \default meet-left {x y : E} : meet x y <= x => (tmeet (totality x y)).
  \default meet-right {x y : E} : meet x y <= y => (tmeet (totality x y)).
  \default meet-univ {x y z : E} : z <= x -> z <= y -> z <= meet x y => (tmeet (totality x y)). z

  \default join (x y : E) : E => (tjoin (totality x y)).
  \default join-left {x y : E} : x <= join x y => (tjoin (totality x y)).
  \default join-right {x y : E} : y <= join x y => (tjoin (totality x y)).
  \default join-univ {x y z : E} : x <= z -> y <= z -> join x y <= z => (tjoin (totality x y)). z

  | ldistr>= {x} {y} {z} =>
    \case totality y z \with {
      | byLeft y<=z => meet-monotone <=-refl (join-univ y<=z <=-refl) <=∘ join-right
      | byRight z<=y => meet-monotone <=-refl (join-univ <=-refl z<=y) <=∘ join-left
    }

  \lemma meet-isMin (x y : E) : (x ∧ y = x) || (x ∧ y = y)
    => \case totality x y \with {
      | byLeft x<=y => byLeft (<=-antisymmetric Lattice.meet-left (Lattice.meet-univ <=-refl x<=y))
      | byRight y<=x => byRight (<=-antisymmetric Lattice.meet-right (Lattice.meet-univ y<=x <=-refl))
    }

  \lemma meet-prop (P : E -> \Prop) {x y : E} (Px : P x) (Py : P y) : P (x ∧ y)
    => \case meet-isMin x y \with {
      | byLeft p => transportInv P p Px
      | byRight p => transportInv P p Py
    }

  \lemma join-isMax (x y : E) : (x ∨ y = x) || (x ∨ y = y)
    => \case totality x y \with {
      | byLeft x<=y => byRight (<=-antisymmetric (Lattice.join-univ x<=y <=-refl) Lattice.join-right)
      | byRight y<=x => byLeft (<=-antisymmetric (Lattice.join-univ <=-refl y<=x) Lattice.join-left)
    }

  \lemma join-prop (P : E -> \Prop) {x y : E} (Px : P x) (Py : P y) : P (x ∨ y)
    => \case join-isMax x y \with {
      | byLeft p => transportInv P p Px
      | byRight p => transportInv P p Py
    }
} \where {
  \func tmeet {E : Poset} {x y : E} => ||.rec MeetSemilattice.Meet-isProp
                                              (\lam x<=y => (x, E.<=-refl, x<=y, \lam z z<=x _ => z<=x))
                                              (\lam y<=x => (y, y<=x, E.<=-refl, \lam z _ z<=y => z<=y))

  \func tjoin {E : Poset} {x y : E} => ||.rec JoinSemilattice.Join-isProp
                                              (\lam x<=y => (y, x<=y, E.<=-refl, \lam z _ y<=z => y<=z))
                                              (\lam y<=x => (x, E.<=-refl, y<=x, \lam z z<=x _ => z<=x))
}

\class BiorderedSet \extends StrictPoset, Poset {
  | \fixr  <-transitive-right {a1 a2 a3 : E} : a1 <= a2 -> a2 < a3 -> a1 < a3
  | \fixl  <-transitive-left {a1 a2 a3 : E} : a1 < a2 -> a2 <= a3 -> a1 < a3
  | <=-less {a1 a2 : E} : a1 < a2 -> a1 <= a2

  \func op : BiorderedSet \cowith
    | StrictPoset => StrictPoset.op
    | Poset => Poset.op
    | <-transitive-right p q => <-transitive-left q p
    | <-transitive-left p q => <-transitive-right q p
    | <=-less => <=-less
}

-- | A linearly ordered set.
\class LinearOrder \extends BiorderedSet {
  | <-comparison (y : E) {x z : E} : x < z -> x < y || y < z
  | <-connectedness {x y : E} : Not (x < y) -> Not (y < x) -> x = y

  | <= => <=
  | <=-refl => <-irreflexive
  | <=-transitive {x} {y} {z} x<=y y<=z => \case <-comparison y __ \with {
    | byLeft z<y => y<=z z<y
    | byRight y<x => x<=y y<x
  }
  | <=-antisymmetric x<=y y<=x => <-connectedness y<=x x<=y

  | <-transitive-right {a1} {a2} {a3} a2/<a1 a2<a3 => \case <-comparison a1 a2<a3 \with {
    | byLeft a2<a1 => absurd (a2/<a1 a2<a1)
    | byRight a1<a3 => a1<a3
  }
  | <-transitive-left {a1} {a2} {a3} a1<a2 a3/<a2 => \case <-comparison a3 a1<a2 \with {
    | byLeft a1<a3 => a1<a3
    | byRight a3<a2 => absurd (a3/<a2 a3<a2)
  }
  | <=-less p => \lam q => <-irreflexive (<-transitive p q)

  \func op : LinearOrder \cowith
    | StrictPoset => StrictPoset.op
    | <-comparison y x<z => \case <-comparison y x<z \with {
      | byLeft z<y => byRight z<y
      | byRight y<x => byLeft y<x
    }
    | <-connectedness p q => <-connectedness q p
} \where {
  \class With# \extends LinearOrder, Set#
    | # x y => x < y || y < x
    | #-irreflexive x#x => \case x#x \with {
      | byLeft x<x => <-irreflexive x<x
      | byRight x<x => <-irreflexive x<x
    }
    | #-symmetric x#y => \case x#y \with {
      | byLeft x<y => byRight x<y
      | byRight y<x => byLeft y<x
    }
    | #-comparison x y z x#z => \case x#z \with {
      | byLeft x<z => \case <-comparison y x<z \with {
        | byLeft x<y => byLeft (byLeft x<y)
        | byRight y<z => byRight (byLeft y<z)
      }
      | byRight z<x => \case <-comparison y z<x \with {
        | byLeft z<y => byRight (byRight z<y)
        | byRight y<x => byLeft (byRight y<x)
      }
    }
    | tightness x/#y => <-connectedness (\lam x<y => x/#y (byLeft x<y)) (\lam y<x => x/#y (byRight y<x))

  \type \infix  <= {A : StrictPoset} (a a' : A) => Not (a' < a)

  \lemma <_<= {A : StrictPoset} {a a' : A} (p : a < a') : a <= a'
    => \lam q => <-irreflexive (<-transitive p q)

  \lemma notLess {A : StrictPoset} {a a' : A} (p : a <= a') (q : a' < a) : Empty
    => p q

  -- | A linearly ordered set with decidable inequality.
  \class Dec \extends LinearOrder, DecSet, TotalOrder {
    \field trichotomy (x y : E) : Tri x y

    | <-comparison y {x} {z} x<z => \case trichotomy x y \with {
      | less x<y => byLeft x<y
      | equals x=y => byRight (transport (`< z) x=y x<z)
      | greater y<x => byRight (<-transitive y<x x<z)
    }
    | <-connectedness {x} {y} x/<y y/<x => \case trichotomy x y \with {
      | less x<y => absurd (x/<y x<y)
      | equals x=y => x=y
      | greater y<x => absurd (y/<x y<x)
    }
    | totality x y => \case trichotomy x y \with {
      | less x<y => byLeft (<=-less x<y)
      | equals x=y => byLeft (rewrite x=y <-irreflexive)
      | greater y<x => byRight (<=-less y<x)
    }

    | meet x y => \case trichotomy x y \with {
      | less _ => x
      | equals _ => x
      | greater _ => y
    }
    | meet-left => unfold (mcases <=-refl \with {
      | greater y<x => <=-less y<x
    })
    | meet-right => unfold (mcases \with {
      | less x<y => <=-less x<y
      | equals x=y => rewrite x=y <=-refl
      | greater _ => <=-refl
    })
    | meet-univ z<=x z<=y => unfold (mcases z<=x \with {
      | greater _ => z<=y
    })

    | join x y => \case trichotomy x y \with {
      | less _ => y
      | equals _ => x
      | greater _ => x
    }
    | join-left => unfold (mcases <=-refl \with {
      | less x<y => <=-less x<y
    })
    | join-right => unfold (mcases \with {
      | less _x => <=-refl
      | equals x=y => rewrite x=y <=-refl
      | greater y<x => <=-less y<x
    })
    | join-univ x<=z y<=z => unfold (mcases x<=z \with {
      | less _ => y<=z
    })

    \default decideEq x y => \case trichotomy x y \with {
      | less x<y => no (\lam x=y => <-irreflexive (transport (`< y) x=y x<y))
      | equals x=y => yes x=y
      | greater y<x => no (\lam x=y => <-irreflexive (transport (y <) x=y y<x))
    }

    \func op : Dec \cowith
      | LinearOrder => LinearOrder.op
      | decideEq => decideEq
      | trichotomy x y => \case trichotomy x y \with {
        | less y<x => greater y<x
        | equals x=y => equals x=y
        | greater x<y => less x<y
      }
  }

  \func <-dec {A : Dec} (a a' : A) : Decide (a < a') \cowith
    | decide => \case dec<_<= a a' \with {
      | inl a<a' => yes a<a'
      | inr a'<=a => no a'<=a
    }

  \lemma <=_/= {A : Dec} {a a' : A} (p : a <= a') (q : a /= a') : a < a'
    => \case trichotomy a a' \with {
         | less r => r
         | equals r => absurd (q r)
         | greater r => absurd (p r)
       }

  \func <=-dec {A : Dec} {a a' : A} (p : a <= a') : (a < a') `Or` (a = a') => \case trichotomy a a' \with {
    | less a<a' => inl a<a'
    | equals a=a' => inr a=a'
    | greater a'<a => absurd (p a'<a)
  }

  \func dec<_<= {A : Dec} (a a' : A) : (a < a') `Or` (a' <= a) => \case trichotomy a a' \with {
    | less a<a' => inl a<a'
    | equals a=a' => inr (rewrite a=a' <-irreflexive)
    | greater a'<a => inr (<=-less a'<a)
  }

  \lemma dec<_reduce {A : Dec} {a a' : A} (p : a < a') : dec<_<= a a' = inl p
    => unfold dec<_<= (mcases contradiction \with {
      | less a<a' => pmap inl propPath
    })

  \lemma dec<=_reduce {A : Dec} {a a' : A} (p : a' <= a) : dec<_<= a a' = inr p
    => unfold dec<_<= (mcases (pmap inr propPath) \with {
      | less a<a' => contradiction
    })

  \lemma dec<= {A : Dec} (a a' : A) : Set.Dec (a <= a')
    => \case dec<_<= a' a \with {
         | inl q => no \lam p => <-irreflexive (<-transitive-left q p)
         | inr q => yes q
       }

  \lemma trichotomy<_reduce {A : Dec} {a a' : A} (p : a < a') : trichotomy a a' = less p
    => cases (trichotomy a a') contradiction \with {
      | less q => pmap less propPath
    }

  \lemma trichotomy=_reduce {A : Dec} {a a' : A} (p : a = a') : trichotomy a a' = equals p
    => cases (trichotomy a a') contradiction \with {
      | equals q => pmap equals propPath
    }

  \lemma trichotomy>_reduce {A : Dec} {a a' : A} (p : a' < a) : trichotomy a a' = greater p
    => cases (trichotomy a a') contradiction \with {
      | greater q => pmap greater propPath
    }

  \lemma <_meet-univ {A : Dec} {x y z : A} (p : x < y) (q : x < z) : x < y ∧ z
    => \case dec<_<= y z \with {
      | inl y<z => rewrite (meet_<= (<=-less y<z)) p
      | inr z<=y => rewrite (meet-comm *> meet_<= z<=y) q
    }

  \lemma Big_<_meet-univ {A : Dec} {l : Array A} {x y : A} (p : y < x) (f : \Pi (i : Fin l.len) -> y < l i) : y < Big (∧) x l \elim l
    | nil => p
    | :: a l => <_meet-univ (f ) (Big_<_meet-univ p (\lam i => f (suc i)))

  \lemma <_join-univ {A : Dec} {x y z : A} (p : x < z) (q : y < z) : x ∨ y < z
    => \case dec<_<= x y \with {
      | inl x<y => rewrite (join_<= (<=-less x<y)) q
      | inr y<=x => rewrite (join-comm *> join_<= y<=x) p
    }

  \lemma Big_<_join-univ {A : Dec} {l : Array A} {x y : A} (p : x < y) (f : \Pi (i : Fin l.len) -> l i < y) : Big (∨) x l < y \elim l
    | nil => p
    | :: a l => <_join-univ (f ) (Big_<_join-univ p (\lam i => f (suc i)))
}

\class DenseLinearOrder \extends LinearOrder
  | isDense {x z : E} : x < z -> ∃ (y : E) (x < y) (y < z)
  \where {
    \class Dec \extends DenseLinearOrder, LinearOrder.Dec
  }

\class UnboundedDenseLinearOrder \extends DenseLinearOrder
  | withoutUpperBound (x : E) : ∃ (y : E) (x < y)
  | withoutLowerBound (x : E) : ∃ (y : E) (y < x)
  \where {
    \class Dec \extends UnboundedDenseLinearOrder, DenseLinearOrder.Dec
  }

\data Tri {A : StrictPoset} (a a' : A)
  | less (a < a')
  | equals (a = a')
  | greater (a > a')
  \where
    \use \level levelProp : \Prop