Finite choice by capacity and priority

import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Lattice.Basic
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Prod.Lex
import Mathlib.Tactic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems

namespace AppliedModelingLib
namespace FiniteChoice

variable {α : Type*} [DecidableEq α]

/-- A finite choice rule maps every finite feasible set to a finite chosen set. -/
abbrev ChoiceRule (α : Type*) [DecidableEq α] := Finset α → Finset α

/-- Feasibility: the chosen set is always contained in the offered set. -/
def Feasible (C : ChoiceRule α) : Prop :=
  ∀ X, C X ⊆ X

/-- `q`-acceptance: choose as many alternatives as possible, up to capacity `q`. -/
def QAcceptant (q : ℕ) (C : ChoiceRule α) : Prop :=
  ∀ X, (C X).card = min q X.card

/-- Substitutability: shrinking the offered set does not hurt retained chosen elements. -/
def Substitutable (C : ChoiceRule α) : Prop :=
  ∀ {X₁ X₂}, X₁ ⊆ X₂ → X₁ ∩ C X₂ ⊆ C X₁

/-- A strict total order in the asymmetric/transitive/complete sense. -/
def StrictTotalOrder (r : α → α → Prop) : Prop :=
  (∀ x, ¬ r x x) ∧
    (∀ {x y z}, r x y → r y z → r x z) ∧
      (∀ {x y}, x ≠ y → r x y ∨ r y x)

/--
`C` is represented by a single priority order if it chooses only offered
applicants, is q-acceptant, and every chosen applicant is above every rejected
applicant in each finite pool.
-/
def QRepresentative (q : ℕ) (C : ChoiceRule α) : Prop :=
  ∃ r : α → α → Prop,
    StrictTotalOrder r ∧ Feasible C ∧ QAcceptant q C ∧
      ∀ {X x y}, x ∈ C X → y ∈ X → y ∉ C X → r x y

set_option linter.unusedSectionVars false in
/-- The irreflexive projection from a `StrictTotalOrder`. -/
theorem StrictTotalOrder.irrefl {r : α → α → Prop}
    (h : StrictTotalOrder r) (x : α) :
    ¬ r x x :=
  h.1 x

set_option linter.unusedSectionVars false in
/-- The transitive projection from a `StrictTotalOrder`. -/
theorem StrictTotalOrder.trans {r : α → α → Prop}
    (h : StrictTotalOrder r) {x y z : α} :
    r x y → r y z → r x z :=
  h.2.1

set_option linter.unusedSectionVars false in
/-- A strict total order is asymmetric. -/
theorem StrictTotalOrder.asymm {r : α → α → Prop}
    (h : StrictTotalOrder r) {x y : α} (hxy : r x y) :
    ¬ r y x := by
  intro hyx
  exact h.irrefl x (h.trans hxy hyx)

section LinearTopQChoice

variable [LinearOrder α]

/--
The q-acceptant rule that chooses the first `q` elements of the offered set in
the ambient linear order, or everyone if the pool has size below capacity.
-/
noncomputable def linearTopQChoice (q : ℕ) : ChoiceRule α :=
  fun X =>
    if h : q ≤ X.card then
      Finset.univ.image
        (fun i : Fin q =>
          ((X.orderIsoOfFin (by rfl)
            ⟨i.1, lt_of_lt_of_le i.2 h⟩ : X) : α))
    else
      X

/-- The linear top-q choice rule only chooses offered alternatives. -/
theorem linearTopQChoice_feasible (q : ℕ) :
    Feasible (linearTopQChoice (α := α) q) := by
  classical
  intro X x hx
  unfold linearTopQChoice at hx
  split_ifs at hx with h
  · rcases Finset.mem_image.mp hx with ⟨i, _hi, rfl⟩
    exact ((X.orderIsoOfFin (by rfl)
      ⟨i.1, lt_of_lt_of_le i.2 h⟩ : X)).2
  · exact hx

/-- The linear top-q choice rule chooses exactly `min q X.card` alternatives. -/
theorem linearTopQChoice_qAcceptant (q : ℕ) :
    QAcceptant q (linearTopQChoice (α := α) q) := by
  classical
  intro X
  unfold linearTopQChoice
  by_cases h : q ≤ X.card
  · rw [dif_pos h]
    have hinj : Function.Injective
        (fun i : Fin q =>
          ((X.orderIsoOfFin (by rfl)
            ⟨i.1, lt_of_lt_of_le i.2 h⟩ : X) : α)) := by
      intro i j hij
      have hsub :
          (X.orderIsoOfFin (by rfl)
              ⟨i.1, lt_of_lt_of_le i.2 h⟩ : X) =
            (X.orderIsoOfFin (by rfl)
              ⟨j.1, lt_of_lt_of_le j.2 h⟩ : X) := by
        exact Subtype.ext hij
      have hfin :
          (⟨i.1, lt_of_lt_of_le i.2 h⟩ : Fin X.card) =
            ⟨j.1, lt_of_lt_of_le j.2 h⟩ := by
        exact (X.orderIsoOfFin (by rfl)).injective hsub
      exact Fin.ext (congrArg (fun k : Fin X.card => k.1) hfin)
    rw [Finset.card_image_of_injective _ hinj]
    simp [Nat.min_eq_left h]
  · rw [dif_neg h]
    have hle : X.card ≤ q := Nat.le_of_not_ge h
    rw [Nat.min_eq_right hle]

/-- The linear top-q choice rule is represented by the ambient linear order. -/
theorem linearTopQChoice_qRepresentative (q : ℕ) :
    QRepresentative q (linearTopQChoice (α := α) q) := by
  classical
  refine ⟨(· < ·), ?_, linearTopQChoice_feasible (α := α) q,
    linearTopQChoice_qAcceptant (α := α) q, ?_⟩
  · constructor
    · intro x
      exact lt_irrefl x
    · constructor
      · intro x y z hxy hyz
        exact lt_trans hxy hyz
      · intro x y hxy
        exact lt_or_gt_of_ne hxy
  · intro X x y hx hyX hyNot
    unfold linearTopQChoice at hx hyNot
    by_cases h : q ≤ X.card
    · rw [dif_pos h] at hx hyNot
      rcases Finset.mem_image.mp hx with ⟨i, _hi, rfl⟩
      have hySubtype : (⟨y, hyX⟩ : X) ∉
          Finset.univ.image
            (fun i : Fin q =>
              X.orderIsoOfFin (by rfl)
                ⟨i.1, lt_of_lt_of_le i.2 h⟩) := by
        intro hyImage
        apply hyNot
        rcases Finset.mem_image.mp hyImage with ⟨j, hj, hjEq⟩
        exact Finset.mem_image.mpr ⟨j, hj, congrArg Subtype.val hjEq⟩
      have hq_le_yidx :
          q ≤ ((X.orderIsoOfFin (by rfl)).symm ⟨y, hyX⟩).1 := by
        by_contra hlt
        have hlt' : ((X.orderIsoOfFin (by rfl)).symm ⟨y, hyX⟩).1 < q :=
          Nat.lt_of_not_ge hlt
        have hyImage : (⟨y, hyX⟩ : X) ∈
            Finset.univ.image
              (fun i : Fin q =>
                X.orderIsoOfFin (by rfl)
                  ⟨i.1, lt_of_lt_of_le i.2 h⟩) := by
          refine Finset.mem_image.mpr ⟨⟨_, hlt'⟩, Finset.mem_univ _, ?_⟩
          simp
        exact hySubtype hyImage
      have hi_lt_yidx :
          (⟨i.1, lt_of_lt_of_le i.2 h⟩ : Fin X.card) <
            (X.orderIsoOfFin (by rfl)).symm ⟨y, hyX⟩ := by
        exact Fin.mk_lt_mk.mpr (lt_of_lt_of_le i.2 hq_le_yidx)
      have hsub_lt :
          (X.orderIsoOfFin (by rfl)
            ⟨i.1, lt_of_lt_of_le i.2 h⟩ : X) < ⟨y, hyX⟩ := by
        simpa using
          (X.orderIsoOfFin (by rfl)).strictMono hi_lt_yidx
      exact hsub_lt
    · rw [dif_neg h] at hyNot
      exact False.elim (hyNot hyX)

end LinearTopQChoice

section RelabeledTopQChoice

variable {β : Type*} [DecidableEq β] [LinearOrder β]

end RelabeledTopQChoice

section LinearTopQChoiceCharacterization

variable [LinearOrder α]

end LinearTopQChoiceCharacterization

section RankedTopQChoice

variable [LinearOrder α]

end RankedTopQChoice

/--
If two finite sets have the same cardinality and `B` has an element missing
from `A`, then `A` has a compensating element missing from `B`.
-/
theorem exists_mem_sdiff_of_card_eq_of_mem_sdiff
    {A B : Finset α} (hcard : A.card = B.card) {x : α}
    (hx : x ∈ B \ A) :
    ∃ y, y ∈ A \ B := by
  rcases Finset.mem_sdiff.mp hx with ⟨hxB, hxnotA⟩
  by_contra hnone
  have hsubset : A ⊆ B := by
    intro y hyA
    by_contra hyB
    exact hnone ⟨y, Finset.mem_sdiff.mpr ⟨hyA, hyB⟩⟩
  have hAB : A = B :=
    Finset.eq_of_subset_of_card_le hsubset (by omega)
  exact hxnotA (by simpa [hAB] using hxB)

/-- On any input of size at most `q`, a `q`-acceptant rule chooses equally many elements. -/
theorem QAcceptant.card_eq_of_card_le {q : ℕ} {C : ChoiceRule α}
    (haccept : QAcceptant q C) {X : Finset α} (hcard : X.card ≤ q) :
    (C X).card = X.card := by
  rw [haccept X, Nat.min_eq_right hcard]

/-- A feasible `q`-acceptant rule chooses every element of an input of size at most `q`. -/
theorem QAcceptant.eq_of_card_le {q : ℕ} {C : ChoiceRule α}
    (hfeasible : Feasible C) (haccept : QAcceptant q C)
    {X : Finset α} (hcard : X.card ≤ q) :
    C X = X := by
  exact Finset.eq_of_subset_of_card_le (hfeasible X)
    (by rw [QAcceptant.card_eq_of_card_le haccept hcard])

/--
Feasible q-representative choice rules are substitutable.  The fixed
representing order rules out an old rejected element becoming chosen: equal
q-acceptant cardinalities force some old chosen element to be displaced, which
would put the two elements above each other in the strict order.
-/
theorem substitutable_of_feasible_of_qRepresentative
    {q : ℕ} {C : ChoiceRule α}
    (hfeasible : Feasible C) (hrep : QRepresentative q C) :
    Substitutable C := by
  rcases hrep with ⟨r, hstrict, _hrep_feasible, haccept, hpriority⟩
  intro X₁ X₂ hsubset x hx
  rcases Finset.mem_inter.mp hx with ⟨hxX₁, hxCX₂⟩
  by_contra hxnotCX₁
  by_cases hX₁_le_q : X₁.card ≤ q
  · have hCX₁ : C X₁ = X₁ :=
      QAcceptant.eq_of_card_le hfeasible haccept hX₁_le_q
    exact hxnotCX₁ (by simpa [hCX₁] using hxX₁)
  · have hq_lt_X₁ : q < X₁.card := Nat.lt_of_not_ge hX₁_le_q
    have hq_le_X₁ : q ≤ X₁.card := le_of_lt hq_lt_X₁
    have hq_le_X₂ : q ≤ X₂.card :=
      hq_le_X₁.trans (Finset.card_le_card hsubset)
    have hcard_eq : (C X₁).card = (C X₂).card := by
      rw [haccept X₁, haccept X₂]
      rw [Nat.min_eq_left hq_le_X₁, Nat.min_eq_left hq_le_X₂]
    have hx_sdiff : x ∈ C X₂ \ C X₁ :=
      Finset.mem_sdiff.mpr ⟨hxCX₂, hxnotCX₁⟩
    rcases exists_mem_sdiff_of_card_eq_of_mem_sdiff hcard_eq hx_sdiff with
      ⟨y, hy_sdiff⟩
    rcases Finset.mem_sdiff.mp hy_sdiff with ⟨hyCX₁, hyNotCX₂⟩
    have hyX₁ : y ∈ X₁ := hfeasible X₁ hyCX₁
    have hyX₂ : y ∈ X₂ := hsubset hyX₁
    have hyx : r y x := hpriority hyCX₁ hxX₁ hxnotCX₁
    have hxy : r x y := hpriority hxCX₂ hyX₂ hyNotCX₂
    exact (hstrict.asymm hxy) hyx

end FiniteChoice
end AppliedModelingLib