comm_alg/CommAlg/StrictSeries.lean

/-
Most of this file is Copyright (c) 2021 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the Mathlib file LICENSE.
Authors: Chris Hughes
-/
import Mathlib.Order.Lattice
import Mathlib.Data.List.Sort
import Mathlib.Logic.Equiv.Fin
import Mathlib.Logic.Equiv.Functor
import Mathlib.Data.Fintype.Card
import Mathlib.Order.Monotone.Basic

structure StrictSeries (X : Type u) [LT X] : Type u where
  length : ℕ
  toFun : Fin (length + 1) → X
  step' : ∀ i : Fin length, (toFun (Fin.castSucc i)) < (toFun (Fin.succ i))
  --StrictMono toFun

namespace StrictSeries

section FinLemmas

-- TODO: move these to `VecNotation` and rename them to better describe their statement
variable {α : Type _} {m n : ℕ} (a : Fin m.succ → α) (b : Fin n.succ → α)

theorem append_castAdd_aux (i : Fin m) :
    Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b
      (Fin.castSucc <| Fin.castAdd n i) =
      a (Fin.castSucc i) := by
  cases i
  simp [Matrix.vecAppend_eq_ite, *]
#align composition_series.append_cast_add_aux StrictSeries.append_castAdd_aux

theorem append_succ_castAdd_aux (i : Fin m) (h : a (Fin.last _) = b 0) :
    Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b (Fin.castAdd n i).succ =
      a i.succ := by
  cases' i with i hi
  simp only [Matrix.vecAppend_eq_ite, hi, Fin.succ_mk, Function.comp_apply, Fin.castSucc_mk,
    Fin.val_mk, Fin.castAdd_mk]
  split_ifs with h_1
  · rfl
  · have : i + 1 = m := le_antisymm hi (le_of_not_gt h_1)
    calc
      b ⟨i + 1 - m, by simp [this]⟩ = b 0 := congr_arg b (by simp [Fin.ext_iff, this])
      _ = a (Fin.last _) := h.symm
      _ = _ := congr_arg a (by simp [Fin.ext_iff, this])
#align composition_series.append_succ_cast_add_aux StrictSeries.append_succ_castAdd_aux

theorem append_natAdd_aux (i : Fin n) :
    Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b
      (Fin.castSucc <| Fin.natAdd m i) =
      b (Fin.castSucc i) := by
  cases i
  simp only [Matrix.vecAppend_eq_ite, Nat.not_lt_zero, Fin.natAdd_mk, add_lt_iff_neg_left,
    add_tsub_cancel_left, dif_neg, Fin.castSucc_mk, not_false_iff, Fin.val_mk]
#align composition_series.append_nat_add_aux StrictSeries.append_natAdd_aux

theorem append_succ_natAdd_aux (i : Fin n) :
    Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b (Fin.natAdd m i).succ =
      b i.succ := by
  cases' i with i hi
  simp only [Matrix.vecAppend_eq_ite, add_assoc, Nat.not_lt_zero, Fin.natAdd_mk,
    add_lt_iff_neg_left, add_tsub_cancel_left, Fin.succ_mk, dif_neg, not_false_iff, Fin.val_mk]
#align composition_series.append_succ_nat_add_aux StrictSeries.append_succ_natAdd_aux

end FinLemmas


section LT

variable {X : Type u} [LT X]

instance coeFun : CoeFun (StrictSeries X) fun x => Fin (x.length + 1) → X where
  coe := StrictSeries.toFun

instance inhabited [Inhabited X] : Inhabited (StrictSeries X) :=
  ⟨{  length := 0
      toFun := default
      step' := fun x => x.elim0 }⟩

theorem step (s : StrictSeries X) :
    ∀ i : Fin s.length, (s (Fin.castSucc i)) < (s (Fin.succ i)) :=
  s.step'

theorem coeFn_mk (length : ℕ) (toFun step) :
    (@StrictSeries.mk X _ length toFun step : Fin length.succ → X) = toFun :=
  rfl

theorem lt_succ (s : StrictSeries X) (i : Fin s.length) :
    s (Fin.castSucc i) < s (Fin.succ i) :=
   (s.step _)

instance membership : Membership X (StrictSeries X) :=
  ⟨fun x s => x ∈ Set.range s⟩

theorem mem_def {x : X} {s : StrictSeries X} : x ∈ s ↔ x ∈ Set.range s :=
  Iff.rfl

/-- The ordered `List X` of elements of a `StrictSeries X`. -/
def toList (s : StrictSeries X) : List X :=
  List.ofFn s

/-- Two `StrictSeries` are equal if they are the same length and
have the same `i`th element for every `i` -/
theorem ext_fun {s₁ s₂ : StrictSeries X} (hl : s₁.length = s₂.length)
    (h : ∀ i, s₁ i = s₂ (Fin.cast (congr_arg Nat.succ hl) i)) : s₁ = s₂ := by
  cases s₁; cases s₂
  -- Porting note: `dsimp at *` doesn't work. Why?
  dsimp at hl h
  subst hl
  simpa [Function.funext_iff] using h

@[simp]
theorem length_toList (s : StrictSeries X) : s.toList.length = s.length + 1 := by
  rw [toList, List.length_ofFn]

theorem toList_ne_nil (s : StrictSeries X) : s.toList ≠ [] := by
  rw [← List.length_pos_iff_ne_nil, length_toList]; exact Nat.succ_pos _

theorem chain'_toList (s : StrictSeries X) : List.Chain' (· < ·) s.toList :=
  List.chain'_iff_get.2
    (by
      intro i hi
      simp only [toList, List.get_ofFn]
      rw [length_toList] at hi
      exact s.step ⟨i, hi⟩)

@[simp]
theorem mem_toList {s : StrictSeries X} {x : X} : x ∈ s.toList ↔ x ∈ s := by
  rw [toList, List.mem_ofFn, mem_def]

/-- Make a `StrictSeries X` from the ordered list of its elements. -/
def ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' (· < ·) l) : StrictSeries X
    where
  length := l.length - 1
  toFun i :=
    l.nthLe i
      (by
        conv_rhs => rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
        exact i.2)
  step' := fun ⟨i, hi⟩ => List.chain'_iff_get.1 hc i hi

theorem length_ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' (· < ·) l) :
    (ofList l hl hc).length = l.length - 1 :=
  rfl

theorem ofList_toList (s : StrictSeries X) :
    ofList s.toList s.toList_ne_nil s.chain'_toList = s := by
  refine' ext_fun _ _
  · rw [length_ofList, length_toList, Nat.succ_sub_one]
  · rintro ⟨i, hi⟩
    simp [ofList, toList, -List.ofFn_succ]

@[simp]
theorem ofList_toList' (s : StrictSeries X) :
    ofList s.toList s.toList_ne_nil s.chain'_toList = s :=
  ofList_toList s

@[simp]
theorem toList_ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' (· < ·) l) :
    toList (ofList l hl hc) = l := by
  refine' List.ext_get _ _
  · rw [length_toList, length_ofList,
      tsub_add_cancel_of_le (Nat.succ_le_of_lt <| List.length_pos_of_ne_nil hl)]
  · intro i hi hi'
    dsimp [ofList, toList]
    rw [List.get_ofFn]
    rfl

/-- The last element of a `StrictSeries` -/
def top (s : StrictSeries X) : X :=
  s (Fin.last _)

theorem top_mem (s : StrictSeries X) : s.top ∈ s :=
  mem_def.2 (Set.mem_range.2 ⟨Fin.last _, rfl⟩)

/-- The first element of a `StrictSeries` -/
def bot (s : StrictSeries X) : X :=
  s 0

theorem bot_mem (s : StrictSeries X) : s.bot ∈ s :=
  mem_def.2 (Set.mem_range.2 ⟨0, rfl⟩)

/-- Remove the largest element from a `StrictSeries`. If the toFun `s`
has length zero, then `s.eraseTop = s` -/
@[simps]
def eraseTop (s : StrictSeries X) : StrictSeries X
    where
  length := s.length - 1
  toFun i := s ⟨i, lt_of_lt_of_le i.2 (Nat.succ_le_succ tsub_le_self)⟩
  step' i := by
    have := s.step ⟨i, lt_of_lt_of_le i.2 tsub_le_self⟩
    cases i
    exact this

theorem top_eraseTop (s : StrictSeries X) :
    s.eraseTop.top = s ⟨s.length - 1, lt_of_le_of_lt tsub_le_self (Nat.lt_succ_self _)⟩ :=
  show s _ = s _ from
    congr_arg s
      (by
        ext
        simp only [eraseTop_length, Fin.val_last, Fin.coe_castSucc, Fin.coe_ofNat_eq_mod,
          Fin.val_mk])

@[simp]
theorem bot_eraseTop (s : StrictSeries X) : s.eraseTop.bot = s.bot :=
  rfl

/-- Append two composition toFun `s₁` and `s₂` such that
the least element of `s₁` is the maximum element of `s₂`. -/
@[simps length]
def append (s₁ s₂ : StrictSeries X) (h : s₁.top = s₂.bot) : StrictSeries X where
  length := s₁.length + s₂.length
  toFun := Matrix.vecAppend (Nat.add_succ s₁.length s₂.length).symm (s₁ ∘ Fin.castSucc) s₂
  step' i := by
    refine' Fin.addCases _ _ i
    · intro i
      rw [append_succ_castAdd_aux _ _ _ h, append_castAdd_aux]
      exact s₁.step i
    · intro i
      rw [append_natAdd_aux, append_succ_natAdd_aux]
      exact s₂.step i

theorem coe_append (s₁ s₂ : StrictSeries X) (h) :
    ⇑(s₁.append s₂ h) = Matrix.vecAppend (Nat.add_succ _ _).symm (s₁ ∘ Fin.castSucc) s₂ :=
  rfl

@[simp]
theorem append_castAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot) (i : Fin s₁.length) :
    append s₁ s₂ h (Fin.castSucc <| Fin.castAdd s₂.length i) = s₁ (Fin.castSucc i) := by
  rw [coe_append, append_castAdd_aux _ _ i]

@[simp]
theorem append_succ_castAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot)
    (i : Fin s₁.length) : append s₁ s₂ h (Fin.castAdd s₂.length i).succ = s₁ i.succ := by
  rw [coe_append, append_succ_castAdd_aux _ _ _ h]

@[simp]
theorem append_natAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot) (i : Fin s₂.length) :
    append s₁ s₂ h (Fin.castSucc <| Fin.natAdd s₁.length i) = s₂ (Fin.castSucc i) := by
  rw [coe_append, append_natAdd_aux _ _ i]

@[simp]
theorem append_succ_natAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot) (i : Fin s₂.length) :
    append s₁ s₂ h (Fin.natAdd s₁.length i).succ = s₂ i.succ := by
  rw [coe_append, append_succ_natAdd_aux _ _ i]

/-- Add an element to the top of a `StrictSeries` -/
@[simps length]
def snoc (s : StrictSeries X) (x : X) (hsat : s.top < x) : StrictSeries X where
  length := s.length + 1
  toFun := Fin.snoc s x
  step' i := by
    refine' Fin.lastCases _ _ i
    · rwa [Fin.snoc_castSucc, Fin.succ_last, Fin.snoc_last, ← top]
    · intro i
      rw [Fin.snoc_castSucc, ← Fin.castSucc_fin_succ, Fin.snoc_castSucc]
      exact s.step _
#align composition_series.snoc StrictSeries.snoc

@[simp]
theorem top_snoc (s : StrictSeries X) (x : X) (hsat : s.top < x) :
    (snoc s x hsat).top = x :=
  Fin.snoc_last (α := fun _ => X) _ _
#align composition_series.top_snoc StrictSeries.top_snoc

@[simp]
theorem snoc_last (s : StrictSeries X) (x : X) (hsat : s.top < x) :
    snoc s x hsat (Fin.last (s.length + 1)) = x :=
  Fin.snoc_last (α := fun _ => X) _ _
#align composition_series.snoc_last StrictSeries.snoc_last

@[simp]
theorem snoc_castSucc (s : StrictSeries X) (x : X) (hsat : s.top < x)
    (i : Fin (s.length + 1)) : snoc s x hsat (Fin.castSucc i) = s i :=
  Fin.snoc_castSucc (α := fun _ => X) _ _ _
#align composition_series.snoc_cast_succ StrictSeries.snoc_castSucc

@[simp]
theorem bot_snoc (s : StrictSeries X) (x : X) (hsat : s.top < x) :
    (snoc s x hsat).bot = s.bot := by rw [bot, bot, ← snoc_castSucc s _ _ 0, Fin.castSucc_zero]
#align composition_series.bot_snoc StrictSeries.bot_snoc

theorem mem_snoc {s : StrictSeries X} {x y : X} {hsat : s.top < x} :
    y ∈ snoc s x hsat ↔ y ∈ s ∨ y = x := by
  simp only [snoc, mem_def]
  constructor
  · rintro ⟨i, rfl⟩
    refine' Fin.lastCases _ (fun i => _) i
    · right
      simp
    · left
      simp
  · intro h
    rcases h with (⟨i, rfl⟩ | rfl)
    · use Fin.castSucc i
      simp
    · use Fin.last _
      simp
#align composition_series.mem_snoc StrictSeries.mem_snoc


end LT

section Preorder

variable {X : Type _} [Preorder X]

protected theorem strictMono (s : StrictSeries X) : StrictMono s :=
  Fin.strictMono_iff_lt_succ.2 s.lt_succ

protected theorem injective (s : StrictSeries X) : Function.Injective s :=
  s.strictMono.injective

@[simp]
protected theorem inj (s : StrictSeries X) {i j : Fin s.length.succ} : s i = s j ↔ i = j :=
  s.injective.eq_iff

theorem total {s : StrictSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s) : x ≤ y ∨ y ≤ x := by
  rcases Set.mem_range.1 hx with ⟨i, rfl⟩
  rcases Set.mem_range.1 hy with ⟨j, rfl⟩
  rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]
  exact le_total i j

theorem toList_injective : Function.Injective (@StrictSeries.toList X _) :=
  fun s₁ s₂ (h : List.ofFn s₁ = List.ofFn s₂) => by
  have h₁ : s₁.length = s₂.length :=
    Nat.succ_injective
      ((List.length_ofFn s₁).symm.trans <| (congr_arg List.length h).trans <| List.length_ofFn s₂)
  have h₂ : ∀ i : Fin s₁.length.succ, s₁ i = s₂ (Fin.cast (congr_arg Nat.succ h₁) i) :=
    congr_fun <| List.ofFn_injective <| h.trans <| List.ofFn_congr (congr_arg Nat.succ h₁).symm _
  cases s₁
  cases s₂
  dsimp at h h₁ h₂
  subst h₁
  simp only [mk.injEq, heq_eq_eq, true_and]
  simp only [Fin.cast_refl] at h₂
  exact funext h₂

theorem toList_sorted (s : StrictSeries X) : s.toList.Sorted (· < ·) :=
  List.pairwise_iff_get.2 fun i j h => by
    dsimp [toList]
    rw [List.get_ofFn, List.get_ofFn]
    exact s.strictMono h

theorem toList_nodup (s : StrictSeries X) : s.toList.Nodup :=
  s.toList_sorted.nodup

/-- Two `StrictSeries` on a preorder are equal if they have the same elements. See also `ext_fun`. -/
@[ext]
theorem ext {s₁ s₂ : StrictSeries X} (h : ∀ x, x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂ :=
  toList_injective <|
    List.eq_of_perm_of_sorted
      (by
        classical
        exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
          (Finset.ext <| by simp [*]))
      s₁.toList_sorted s₂.toList_sorted

@[simp]
theorem le_top {s : StrictSeries X} (i : Fin (s.length + 1)) : s i ≤ s.top :=
  s.strictMono.monotone (Fin.le_last _)

theorem le_top_of_mem {s : StrictSeries X} {x : X} (hx : x ∈ s) : x ≤ s.top :=
  let ⟨_i, hi⟩ := Set.mem_range.2 hx
  hi ▸ le_top _

@[simp]
theorem bot_le {s : StrictSeries X} (i : Fin (s.length + 1)) : s.bot ≤ s i :=
  s.strictMono.monotone (Fin.zero_le _)

theorem bot_le_of_mem {s : StrictSeries X} {x : X} (hx : x ∈ s) : s.bot ≤ x :=
  let ⟨_i, hi⟩ := Set.mem_range.2 hx
  hi ▸ bot_le _

-- TODO this should be in section LT
theorem length_pos_of_mem_ne {s : StrictSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s)
    (hxy : x ≠ y) : 0 < s.length :=
  let ⟨i, hi⟩ := hx
  let ⟨j, hj⟩ := hy
  have hij : i ≠ j := mt s.inj.2 fun h => hxy (hi ▸ hj ▸ h)
  hij.lt_or_lt.elim
    (fun hij => lt_of_le_of_lt (zero_le (i : ℕ)) (lt_of_lt_of_le hij (Nat.le_of_lt_succ j.2)))
      fun hji => lt_of_le_of_lt (zero_le (j : ℕ)) (lt_of_lt_of_le hji (Nat.le_of_lt_succ i.2))

-- TODO this should be in section LT
theorem forall_mem_eq_of_length_eq_zero {s : StrictSeries X} (hs : s.length = 0) {x y}
    (hx : x ∈ s) (hy : y ∈ s) : x = y :=
  by_contradiction fun hxy => pos_iff_ne_zero.1 (length_pos_of_mem_ne hx hy hxy) hs

theorem eraseTop_top_le (s : StrictSeries X) : s.eraseTop.top ≤ s.top := by
  simp [eraseTop, top, s.strictMono.le_iff_le, Fin.le_iff_val_le_val, tsub_le_self]

-- TODO this should be in section LT
theorem mem_eraseTop_of_ne_of_mem {s : StrictSeries X} {x : X} (hx : x ≠ s.top) (hxs : x ∈ s) :
    x ∈ s.eraseTop := by
  rcases hxs with ⟨i, rfl⟩
  have hi : (i : ℕ) < (s.length - 1).succ := by
    conv_rhs => rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
    exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [top, s.inj, Fin.ext_iff] using hx)
  refine' ⟨Fin.castSucc i, _⟩
  simp [Fin.ext_iff, Nat.mod_eq_of_lt hi]

theorem mem_eraseTop {s : StrictSeries X} {x : X} (h : 0 < s.length) :
    x ∈ s.eraseTop ↔ x ≠ s.top ∧ x ∈ s := by
  simp only [mem_def]
  dsimp only [eraseTop]
  constructor
  · rintro ⟨i, rfl⟩
    have hi : (i : ℕ) < s.length := by
      conv_rhs => rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
      exact i.2
    simp [top, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
  · intro h
    exact mem_eraseTop_of_ne_of_mem h.1 h.2

theorem lt_top_of_mem_eraseTop {s : StrictSeries X} {x : X} (h : 0 < s.length)
    (hx : x ∈ s.eraseTop) : x < s.top := by
    rw [mem_eraseTop h] at hx
    let ⟨i, hi⟩ := Set.mem_range.2 hx.2
    rw [←hi]
    apply s.strictMono
    apply lt_of_le_of_ne i.le_last
    intro hc
    exact ((hc ▸ hi).symm ▸ hx).1 rfl
    --hi ▸ le_top _
  -- lt_of_le_of_ne (le_top_of_mem ((mem_eraseTop h).1 hx).2) ((mem_eraseTop h).1 hx).1
-- #align composition_series.lt_top_of_mem_erase_top StrictSeries.lt_top_of_mem_eraseTop

theorem isMaximal_eraseTop_top {s : StrictSeries X} (h : 0 < s.length) :
    s.eraseTop.top < s.top := lt_top_of_mem_eraseTop h (top_mem _)
--   have : s.length - 1 + 1 = s.length := by
--     conv_rhs => rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
--   rw [top_eraseTop, top]
--   convert s.step ⟨s.length - 1, Nat.sub_lt h zero_lt_one⟩; ext; simp [this]
-- #align composition_series.is_maximal_erase_top_top StrictSeries.isMaximal_eraseTop_top

-- TODO should be in LT
theorem eq_snoc_eraseTop {s : StrictSeries X} (h : 0 < s.length) :
    s = snoc (eraseTop s) s.top (isMaximal_eraseTop_top h) := by
  ext x
  simp [mem_snoc, mem_eraseTop h]
  by_cases h : x = s.top <;> simp [*, s.top_mem]

-- TODO should be in LT
@[simp]
theorem snoc_eraseTop_top {s : StrictSeries X} (h : s.eraseTop.top < s.top) :
    s.eraseTop.snoc s.top h = s :=
  have h : 0 < s.length :=
    Nat.pos_of_ne_zero
      (by
        intro hs
        refine' ne_of_gt h _
        simp [top, Fin.ext_iff, hs])
  (eq_snoc_eraseTop h).symm

-- section `Equivalent` doesn't apply here

theorem length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {s₁ s₂ : StrictSeries X}
    (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) (hs₁ : s₁.length = 0) : s₂.length = 0 := by
  have : s₁.bot = s₁.top := congr_arg s₁ (Fin.ext (by simp [hs₁]))
  have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans (this.trans ht)).symm
  -- Porting note: Was `simpa [Fin.ext_iff]`.
  rw [Fin.ext_iff] at this
  simpa

theorem length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos {s₁ s₂ : StrictSeries X}
    (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) : 0 < s₁.length → 0 < s₂.length :=
  not_imp_not.1
    (by
      simp only [pos_iff_ne_zero, Ne.def, not_iff_not, Classical.not_not]
      exact length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb.symm ht.symm)

theorem eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {s₁ s₂ : StrictSeries X}
    (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) (hs₁0 : s₁.length = 0) : s₁ = s₂ := by
  have : ∀ x, x ∈ s₁ ↔ x = s₁.top := fun x =>
    ⟨fun hx => forall_mem_eq_of_length_eq_zero hs₁0 hx s₁.top_mem, fun hx => hx.symm ▸ s₁.top_mem⟩
  have : ∀ x, x ∈ s₂ ↔ x = s₂.top := fun x =>
    ⟨fun hx =>
      forall_mem_eq_of_length_eq_zero
        (length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb ht hs₁0) hx s₂.top_mem,
      fun hx => hx.symm ▸ s₂.top_mem⟩
  ext
  simp [*]

end Preorder

end StrictSeries