-- Order theory
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Order
import Cumulus.Relation
import Set
import Function

predicate IsLinearOrder (A r : Set) := IsPartialOrder(A, r) ∧ (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) ∨ relates(r, y, x))
predicate StrictOrder (A r : Set) := RelationBetween(r, A, A) ∧ (IrreflexiveOn(A, r) ∧ TransitiveOn(A, r))
predicate StrictLinearOrder (A r : Set) := StrictOrder(A, r) ∧ ConnectedOn(A, r)
predicate LowerBound (A r S a : Set) := a ∈ A ∧ (S ⊆ A) ∧ (∀ x ∈ S, relates(r, a, x))
predicate UpperBound (A r S a : Set) := a ∈ A ∧ (S ⊆ A) ∧ (∀ x ∈ S, relates(r, x, a))
predicate Least (A r S a : Set) := a ∈ S ∧ LowerBound(A, r, S, a)
predicate Greatest (A r S a : Set) := a ∈ S ∧ UpperBound(A, r, S, a)
predicate Comparable (r x y : Set) := relates(r, x, y) ∨ relates(r, y, x)
predicate Chain (A r C : Set) :=
  (C ⊆ A) ∧ (∀ x ∈ C, ∀ y ∈ C, Comparable(r, x, y))
predicate ChainOfChains (A r S : Set) :=
  (∀ C ∈ S, Chain(A, r, C)) ∧
  (∀ C ∈ S, ∀ D ∈ S, ((C ⊆ D) ∨ (D ⊆ C)))
predicate Maximal (A r m : Set) :=
  m ∈ A ∧ (∀ x ∈ A, relates(r, m, x) → x = m)
predicate ZornCondition (A r : Set) :=
  IsPartialOrder(A, r) ∧
  (∀ C, Chain(A, r, C) → ∃ u, UpperBound(A, r, C, u))
predicate WellOrder (A r : Set) := StrictLinearOrder(A, r) ∧ wellFoundedOn(r, A)
predicate InitialSegment (A r I : Set) :=
  (I ⊆ A) ∧
  (∀ x ∈ I, ∀ y ∈ A, relates(r, y, x) → y ∈ I)
predicate ProperInitialSegment (A r I : Set) := InitialSegment(A, r, I) ∧ I ≠ A
predicate OrderEmbedding (f A r B s : Set) :=
  InjectiveBetween(f, A, B) ∧
  (∀ x ∈ A, ∀ y ∈ A, ∀ u ∈ B, ∀ v ∈ B,
    relates(f, x, u) → relates(f, y, v) → (relates(r, x, y) ↔ relates(s, u, v)))
predicate OrderIsomorphism (f A r B s : Set) :=
  BijectiveBetween(f, A, B) ∧
  (∀ x ∈ A, ∀ y ∈ A, ∀ u ∈ B, ∀ v ∈ B,
    relates(f, x, u) → relates(f, y, v) → (relates(r, x, y) ↔ relates(s, u, v)))

theorem WellOrder.strict_linear (A r : Set)
  requires h : WellOrder(A, r)
  shows StrictLinearOrder(A, r)
proof
  simp [WellOrder]

theorem WellOrder.well_founded (A r : Set)
  requires h : WellOrder(A, r)
  shows wellFoundedOn(r, A)
proof
  simp [WellOrder]

theorem InitialSegment.subset (A r I : Set)
  requires h : InitialSegment(A, r, I)
  shows (I ⊆ A)
proof
  simp [InitialSegment]

theorem InitialSegment.empty (A r : Set)
  shows InitialSegment(A, r, empty)
proof
  simp [InitialSegment, Subset, set.empty]

theorem InitialSegment.full (A r : Set)
  shows InitialSegment(A, r, A)
proof
  simp [InitialSegment, Subset]

theorem ProperInitialSegment.initial (A r I : Set)
  requires h : ProperInitialSegment(A, r, I)
  shows InitialSegment(A, r, I)
proof
  simp [ProperInitialSegment]

theorem OrderIsomorphism.bijective (f A r B s : Set)
  requires h : OrderIsomorphism(f, A, r, B, s)
  shows BijectiveBetween(f, A, B)
proof
  simp [OrderIsomorphism]

theorem OrderIsomorphism.embedding (f A r B s : Set)
  requires h : OrderIsomorphism(f, A, r, B, s)
  shows OrderEmbedding(f, A, r, B, s)
proof
  rcases h with ⟨bijective, ordered⟩
  constructor
  . have injective := Bijective.injective at f, A, B
    exact injective with bijective
  . exact ordered

theorem IsLinearOrder.partial (A r : Set)
  requires h : IsLinearOrder(A, r)
  shows IsPartialOrder(A, r)
proof
  rcases h with ⟨partial, total⟩
  exact partial

theorem IsPartialOrder.reflexive (A r : Set)
  requires h : IsPartialOrder(A, r)
  shows ReflexiveOn(A, r)
proof
  simp [IsPartialOrder, IsPreorder]

theorem IsPartialOrder.transitive (A r : Set)
  requires h : IsPartialOrder(A, r)
  shows TransitiveOn(A, r)
proof
  simp [IsPartialOrder, IsPreorder]

theorem IsPartialOrder.antisymmetric (A r : Set)
  requires h : IsPartialOrder(A, r)
  shows AntisymmetricOn(A, r)
proof
  simp [IsPartialOrder]

theorem Chain.subset (A r C : Set)
  requires h : Chain(A, r, C)
  shows (C ⊆ A)
proof
  simp [Chain]

theorem Chain.empty (A r : Set)
  shows Chain(A, r, empty)
proof
  simp [Chain, Subset, set.empty]

theorem Chain.singleton (A r x : Set)
  requires order : IsPartialOrder(A, r)
  requires hx : x ∈ A
  shows Chain(A, r, {x})
proof
  constructor
    intros y hy
    have equal := singleton.membership.forward with hy
    rwa equal
  . intros y hy z hz
    have equalY := singleton.membership.forward with hy
    have equalZ := singleton.membership.forward with hz
    rw [equalY, equalZ]
    left
    have reflexive := IsPartialOrder.reflexive with order
    exact reflexive with x, hx

theorem Chain.union (A r S : Set)
  requires family : ChainOfChains(A, r, S)
  shows Chain(A, r, ⋃(S))
proof
  rcases family with ⟨chains, nested⟩
  constructor
  . apply union.subset
    intros C0 hC0S
    exact Chain.subset with (chains with C0, hC0S)
  . intros x hx y hy
    simp [set.union] at hx
    obtain ⟨C1, hC1S, hxC1⟩ := hx
    simp [set.union] at hy
    obtain ⟨D1, hD1S, hyD1⟩ := hy
    have alternatives := nested with C1, hC1S, D1, hD1S
    cases alternatives with subsetCD | subsetDC
    . obtain ⟨subsetD, comparableD⟩ := chains with D1, hD1S
      exact comparableD with x, (subsetCD with x, hxC1), y, hyD1
    . obtain ⟨subsetC, comparableC⟩ := chains with C1, hC1S
      exact comparableC with x, hxC1, y, (subsetDC with y, hyD1)

theorem ZornCondition.order (A r : Set)
  requires h : ZornCondition(A, r)
  shows IsPartialOrder(A, r)
proof
  simp [ZornCondition]

theorem ZornCondition.upper_bound (A r C : Set)
  requires h : ZornCondition(A, r)
  requires chain : Chain(A, r, C)
  shows ∃ u, UpperBound(A, r, C, u)
proof
  rcases h with ⟨order, bounded⟩
  exact bounded with C, chain

theorem ZornCondition.nonempty (A r : Set)
  requires h : ZornCondition(A, r)
  shows Nonempty(A)
proof
  have emptyChain := Chain.empty at A, r
  obtain ⟨u, huA, _, _⟩ := ZornCondition.upper_bound with h, emptyChain
  refine ⟨u, huA⟩

theorem StrictOrder.irreflexive (A r : Set)
  requires h : StrictOrder(A, r)
  shows IrreflexiveOn(A, r)
proof
  simp [StrictOrder]

theorem StrictOrder.transitive (A r : Set)
  requires h : StrictOrder(A, r)
  shows TransitiveOn(A, r)
proof
  simp [StrictOrder]

theorem StrictLinearOrder.strict (A r : Set)
  requires h : StrictLinearOrder(A, r)
  shows StrictOrder(A, r)
proof
  simp [StrictLinearOrder]

theorem StrictLinearOrder.connected (A r : Set)
  requires h : StrictLinearOrder(A, r)
  shows ConnectedOn(A, r)
proof
  simp [StrictLinearOrder]

theorem StrictLinearOrder.relation (A r : Set)
  requires h : StrictLinearOrder(A, r)
  shows RelationBetween(r, A, A)
proof
  simp [StrictLinearOrder, StrictOrder]

theorem StrictLinearOrder.irreflexive (A r : Set)
  requires h : StrictLinearOrder(A, r)
  shows IrreflexiveOn(A, r)
proof
  simp [StrictLinearOrder, StrictOrder]

theorem StrictLinearOrder.transitive (A r : Set)
  requires h : StrictLinearOrder(A, r)
  shows TransitiveOn(A, r)
proof
  simp [StrictLinearOrder, StrictOrder]

theorem Ordinal.membership_irreflexive (α : Set)
  requires ordinal : α ∈ Ordinal
  shows IrreflexiveOn(α, membershipOn(α))
proof
  intros x hx related
  have member := membershipOn.relates with hx, hx
  apply membership.irreflexive at x
  apply member.forward
  exact related

theorem Ordinal.membership_transitive (α : Set)
  requires ordinal : α ∈ Ordinal
  shows TransitiveOn(α, membershipOn(α))
proof
  intros x hx y hy z hz xyRelated yzRelated
  have xy := membershipOn.relates with hx, hy
  have xInY := xy.forward with xyRelated
  have yz := membershipOn.relates with hy, hz
  have yInZ := yz.forward with yzRelated
  have zOrdinal := Ordinal.member with ordinal, hz
  have zTransitive := Ordinal.transitive with zOrdinal, y, yInZ
  have xInZ := zTransitive with xInY
  have xz := membershipOn.relates with hx, hz
  apply xz.backward
  exact xInZ

theorem Ordinal.membership_connected (α : Set)
  requires ordinal : α ∈ Ordinal
  shows ConnectedOn(α, membershipOn(α))
proof
  intros x hx y hy unequal
  have xOrdinal := Ordinal.member with ordinal, hx
  have yOrdinal := Ordinal.member with ordinal, hy
  have comparison := Ordinal.trichotomy with xOrdinal, y, yOrdinal
  cases comparison with xInY | rest
  . left
    have related := membershipOn.relates with hx, hy
    apply related.backward
    exact xInY
  . cases rest with equal | yInX
    . exfalso
      apply unequal
      exact equal
    . right
      have related := membershipOn.relates with hy, hx
      apply related.backward
      exact yInX

theorem Ordinal.membership_strict_linear (α : Set)
  requires ordinal : α ∈ Ordinal
  shows StrictLinearOrder(α, membershipOn(α))
proof
  constructor
    constructor
    . exact membershipOn.relation at α
    . constructor
      . exact Ordinal.membership_irreflexive at α
      . exact Ordinal.membership_transitive at α
  . exact Ordinal.membership_connected at α

theorem Ordinal.well_order (α : Set)
  requires ordinal : α ∈ Ordinal
  shows WellOrder(α, membershipOn(α))
proof
  simp [WellOrder, Ordinal.membership_strict_linear, membershipOn.wellFounded]

theorem Ordinal.member_initial_segment (α β : Set)
  requires ordinal : α ∈ Ordinal
  requires member : β ∈ α
  shows InitialSegment(α, membershipOn(α), β)
proof
  constructor
  . have transitive := Ordinal.transitive with ordinal
    exact transitive with β, member
  . intros x hx y hy related
    have alphaTransitive := Ordinal.transitive with ordinal, β, member
    have xInAlpha := alphaTransitive with hx
    have yx := membershipOn.relates with hy, xInAlpha
    have yInX := yx.forward with related
    have betaOrdinal := Ordinal.member with ordinal, member
    have betaTransitive := Ordinal.transitive with betaOrdinal, x, hx
    exact betaTransitive with y, yInX

theorem Ordinal.member_proper_initial_segment (α β : Set)
  requires ordinal : α ∈ Ordinal
  requires member : β ∈ α
  shows ProperInitialSegment(α, membershipOn(α), β)
proof
  constructor
  . have initial := Ordinal.member_initial_segment at α, β
    exact initial with member
  . intro equal
    rw equal at member
    exact membership.irreflexive with member

theorem Least.unique (A r S a b : Set)
  requires order : IsPartialOrder(A, r)
  requires ha : Least(A, r, S, a)
  requires hb : Least(A, r, S, b)
  shows a = b
proof
  rcases order with ⟨preorder, antisymmetric⟩
  rcases ha with ⟨haS, haA, hSA, haLe⟩
  rcases hb with ⟨hbS, hbA, hSB, hbLe⟩
  specialize haLe with b, hbS
  specialize hbLe with a, haS
  exact antisymmetric with a, haA, b, hbA, haLe, hbLe

theorem Greatest.unique (A r S a b : Set)
  requires order : IsPartialOrder(A, r)
  requires ha : Greatest(A, r, S, a)
  requires hb : Greatest(A, r, S, b)
  shows a = b
proof
  rcases order with ⟨preorder, antisymmetric⟩
  rcases ha with ⟨haS, haA, hSA, haGe⟩
  rcases hb with ⟨hbS, hbA, hSB, hbGe⟩
  specialize haGe with b, hbS
  specialize hbGe with a, haS
  exact antisymmetric with a, haA, b, hbA, hbGe, haGe

-- Inclusion is a partial order on any family of sets.
def inclusionOrder (F : Set) : Set :=
  {p ∈ F × F | ∃ C ∈ F, ∃ D ∈ F, p = (C, D) ∧ C ⊆ D}

theorem inclusionOrder.relates (F C D : Set)
  requires hC : C ∈ F
  requires hD : D ∈ F
  shows relates(inclusionOrder(F), C, D) ↔ C ⊆ D
proof
  constructor
  . intro related
    unfold relates at related
    obtain ⟨bounded, U, hU, V, hV, equal, subset⟩ := inclusionOrder.membership.forward with related
    obtain ⟨sameC, sameD⟩ := orderedPair.injective with equal
    rw sameC
    rwa sameD
  . intro subsetCD
    have pair := product.pair with hC, hD
    unfold relates
    exact inclusionOrder.membership.backward with ⟨pair, C, hC, D, hD, rfl, subsetCD⟩

theorem inclusionOrder.partial (F : Set)
  shows IsPartialOrder(F, inclusionOrder(F))
proof
  constructor
    constructor
    . settle with RelationBetween, Subset, inclusionOrder
    . constructor
        intros C hC
        exact inclusionOrder.relates.backward with hC, hC, (Subset.reflexive at C)
        intros C hC D hD E hE cd de
        have subsetCD := inclusionOrder.relates.forward with hC, hD, cd
        have subsetDE := inclusionOrder.relates.forward with hD, hE, de
        exact inclusionOrder.relates.backward with hC, hE, (Subset.transitive with subsetCD, subsetDE)
    intros C hC D hD cd dc
    have subsetCD := inclusionOrder.relates.forward with hC, hD, cd
    have subsetDC := inclusionOrder.relates.forward with hD, hC, dc
    exact Subset.antisymmetric with subsetCD, subsetDC

theorem Chain.adjoin_upper (A r C u : Set)
  requires order : IsPartialOrder(A, r)
  requires chain : Chain(A, r, C)
  requires bound : UpperBound(A, r, C, u)
  shows Chain(A, r, C ∪ {u})
proof
  have reflexive := IsPartialOrder.reflexive with order
  rcases chain with ⟨subsetC, comparable⟩
  rcases bound with ⟨uInA, boundedC, upper⟩
  have singletonSubset : {u} ⊆ A by simp
  have bounded := union2.subset with subsetC, singletonSubset
  constructor
  . exact bounded
  . intros x hx y hy
    have xCases := union2.membership.forward with hx
    have yCases := union2.membership.forward with hy
    cases xCases with xC | xu
    . cases yCases with yC | yu
      . exact comparable with x, xC, y, yC
      . obtain rfl := singleton.membership.forward with yu
        left
        exact upper with x, xC
    . obtain rfl := singleton.membership.forward with xu
      cases yCases with yC | yu
        right
        exact upper with y, yC
      . obtain rfl := singleton.membership.forward with yu
        left
        exact reflexive with u, uInA