import Mathlib.Order.Lattice
import Mathlib.Order.RelSeries

/-!

Lattice Definitions.

This file provides some definitions for lattices. It used to be more critical
when this was an Agda project, since it defined (semi)lattices, the ordering
relation, etc. However, these have been lifted into `Mathlib.Order.Lattice`
etc.. What remains are a couple of theorems about folds, as well
as `FiniteHeightLattice`, the core concept of lattice-based static
program analyses. See the documentation on that class for more information. -/

namespace Spa

/-- Predicate for binary functions independently monotone in both their arguments. -/
def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
    (f : α → β → γ) : Prop :=
  (∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·))

section Folds

variable {α β : Type*} [Preorder α] [Preorder β]

/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/
lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
    (hf₁ : ∀ b, Monotone (f · b)) (hf₂ : ∀ a, Monotone (f a ·)) :
    l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by
  induction hl with
  | nil => exact hb
  | cons hxy _ ih =>
    exact le_trans (hf₁ _ hxy) (hf₂ _ ih)

/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/
lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
    (hf₁ : ∀ a, Monotone (f · a)) (hf₂ : ∀ b, Monotone (f b ·)) :
    l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
  induction hl generalizing b₁ b₂ with
  | nil => exact hb
  | cons hxy _ ih =>
    exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))

omit [Preorder α] in
/-- (right) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
lemma foldr_mono' (l : List α) (f : α → β → β)
    (hf : ∀ a, Monotone (f a ·)) : Monotone (l.foldr f ·) := by
  intro b₁ b₂ hb
  induction l with
  | nil => exact hb
  | cons x xs ih => exact hf x ih

omit [Preorder α] in
/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
lemma foldl_mono' (l : List α) (f : β → α → β)
    (hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by
  intro b₁ b₂ hb
  induction l generalizing b₁ b₂ with
  | nil => exact hb
  | cons x xs ih => exact ih (hf x hb)

end Folds

/-- Predicate on types with `Preorder` that claims all $<$ chains in the type have at most `n` comparisons. -/
def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
  ∀ c : LTSeries α, c.length ≤ n

/-- Wrapper over `LTSeries` that exposes its beginning and end points, as well as its length, as part of the type. -/
structure PointedLTSeries (α : Type*) (f t : α) (n : ℕ) [Preorder α] where
  series : LTSeries α
  head_series : series.head = f
  last_series : series.last = t
  length_series : series.length = n

/-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
  height : ℕ
  longestChain : PointedLTSeries α ⊥ ⊤ height
  chains_bounded : BoundedChains α height

namespace FiniteHeightLattice

variable (α : Type*) [Lattice α] [FiniteHeightLattice α]

/-- The bottom element `⊥` of a finite height lattice is _actually_ the least element. -/
lemma bot_le (a : α) : (⊥ : α) ≤ a := by
  by_cases heq : ⊥ ⊓ a = ⊥
  · exact inf_eq_left.mp heq
  · exfalso
    have lc := FiniteHeightLattice.longestChain (α := α)
    have hlt : ⊥ ⊓ a < lc.series.head := by
      rw [lc.head_series]
      exact lt_of_le_of_ne inf_le_left heq
    have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt)
    rw [RelSeries.cons_length, lc.length_series] at hbound
    omega

end FiniteHeightLattice

end Spa