import HardnessReductions.Core
import HardnessReductions.Scheduling.Defs
import HardnessReductions.Scheduling.Timing

/-!
# MULTIPROCESSOR SCHEDULING

Can the tasks be run on `m` processors so that all of them are finished by the
deadline? Garey–Johnson's [SS8], and the entry that opens their sequencing
section; Karp's JOB SEQUENCING is its neighbour.

The question is Garey–Johnson's, verbatim: a schedule is a **start time for
each task**, `σ : Fin lengths.length → ℕ`, subject to two demands — every task
finishes by the deadline, and at no instant are more than `m` tasks running.
The processors are not named anywhere. That they *could* be named is the
content of the reduction below, not part of the definition: stating the problem
as "split the tasks into `m` groups of total length at most `D`" would be
stating BIN PACKING, and would make the reduction from it true by `rfl`.

The time-line accounting the two demands are phrased with — what it means to be
running at an instant, and what a load bound does and does not force — is
`Scheduling/Timing.lean`, shared by the whole domain.

Hardness proof (in `MultiprocessorScheduling/`): from BIN PACKING
(`FromBinPacking.lean`, the schedule–packing equivalence; certified in
`FromBinPacking/Certified.lean`), and hence from PARTITION by composition.
-/

namespace Hardness

variable {α β : Type}

/-! ### Schedules -/

/-- `σ` is a schedule for the tasks of `α` with lengths `l`, on `m` processors
against the deadline `D`: every task finishes by `D`, and no instant carries
more than `m` running tasks.

Stated over an arbitrary indexed family `l : α → ℕ` so that gadget
constructions can work with tagged task names and transport to list positions
afterwards. -/
def IsSchedule [Fintype α] (l : α → ℕ) (m D : ℕ) (σ : α → ℕ) : Prop :=
  (∀ i, σ i + l i ≤ D) ∧ ∀ u, (running σ l Finset.univ u).card ≤ m

/-- MULTIPROCESSOR SCHEDULING: is there a schedule meeting the deadline? -/
def MULTIPROCESSOR_SCHEDULING : Problem MultiprocessorInstance := fun x ↦
  ∃ σ : Fin x.lengths.length → ℕ,
    IsSchedule (fun i ↦ x.lengths[i.1]) x.procs x.deadline σ

/-! ### Transport of schedules across reindexings

The renaming-invariance lemma the entry owes its gadgets: schedulability along
an equivalence of task types, which is what carries a construction over tagged
task names to the positions of the emitted list. The underlying fact about the
running set is `running_equiv` (`Scheduling/Timing.lean`). -/

/-- A schedule transports along an equivalence of task types. -/
theorem IsSchedule.map [Fintype α] [Fintype β] (e : α ≃ β)
    {l : α → ℕ} {m D : ℕ} {σ : α → ℕ} (h : IsSchedule l m D σ) :
    IsSchedule (fun b ↦ l (e.symm b)) m D (fun b ↦ σ (e.symm b)) := by
  refine ⟨fun b ↦ h.1 (e.symm b), fun u ↦ ?_⟩
  rw [running_equiv e σ l u, Finset.card_map]
  exact h.2 u

/-- Schedulability transports along an equivalence of task types — the
renaming-invariance lemma gadget constructions and the representation pair
both consume. -/
theorem exists_isSchedule_iff_map [Fintype α] [Fintype β] (e : α ≃ β)
    (l : α → ℕ) (m D : ℕ) :
    (∃ σ, IsSchedule l m D σ) ↔
      ∃ σ, IsSchedule (fun b ↦ l (e.symm b)) m D σ := by
  constructor
  · rintro ⟨σ, h⟩
    exact ⟨_, h.map e⟩
  · rintro ⟨σ, h⟩
    have := h.map e.symm
    simp only [Equiv.symm_symm, Equiv.symm_apply_apply] at this
    exact ⟨_, this⟩

end Hardness