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

/-!
# SEQUENCING WITH RELEASE TIMES AND DEADLINES

One processor, and every task with a length, an earliest start and a due date:
can they all be run in time? Garey–Johnson's [SS1], and Karp's JOB SEQUENCING.

Each task carries three numbers, so the instance is one list of **triples**
`(length, release, deadline)` rather than three parallel lists — the discipline
of `KnapsackInstance`, for the same reason: parallel lists would have to agree
in length, and the decoding convention admits no well-formedness condition.

Garey–Johnson state the one-processor condition as an injective start-time
function with `σ t > σ t' → σ t ≥ σ t' + l(t')`. Here it is a load bound of
one, which says the same thing about tasks of positive length — the two
formulations agree exactly when the lengths are positive, as they are in
Garey–Johnson — and, unlike injectivity, degenerates the right way for the
zero lengths this library's `ℕ` convention admits: a task occupying no instant
constrains nothing (`Scheduling/Defs.lean`, `Scheduling/Timing.lean`).

Hardness proof (in `Sequencing/`): from BIN PACKING (`FromBinPacking.lean`, the
enforcer construction of Garey–Johnson §4.2; certified in
`FromBinPacking/Code.lean` and `FromBinPacking/Adequacy.lean`), and hence from
3-PARTITION — Garey–Johnson's own source — by composition, in the strong sense.
-/

namespace Hardness

variable {α β : Type}

/-! ### Feasible schedules -/

/-- `σ` is a feasible one-processor schedule for tasks with lengths `l`, release
times `r` and deadlines `d`: nothing starts before it is released, nothing
finishes after it is due, and no instant carries two tasks.

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

/-- SEQUENCING WITH RELEASE TIMES AND DEADLINES: is there a feasible
one-processor schedule? -/
def SEQUENCING : Problem SequencingInstance := fun x ↦
  ∃ σ : Fin x.tasks.length → ℕ,
    IsSequencing (fun i ↦ x.tasks[i.1].1) (fun i ↦ x.tasks[i.1].2.1)
      (fun i ↦ x.tasks[i.1].2.2) σ

/-! ### Transport of schedules across reindexings

The renaming-invariance lemmas the entry owes its gadgets: feasibility along an
equivalence of task types, and — the form a gadget actually produces — along an
enumeration of tagged task names by the positions of a task list. -/

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

/-- Feasibility transports along an equivalence of task types — the
renaming-invariance lemma gadget constructions and the representation pair both
consume. -/
theorem exists_isSequencing_iff_map [Fintype α] [Fintype β] (e : α ≃ β)
    (l r d : α → ℕ) :
    (∃ σ, IsSequencing l r d σ) ↔
      ∃ σ, IsSequencing (fun b ↦ l (e.symm b)) (fun b ↦ r (e.symm b))
        (fun b ↦ d (e.symm b)) σ := 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⟩

/-- **Renaming invariance, in the form a gadget produces.** A tagged task type
with its three families schedules exactly when the instance whose task list
carries the same triples does — the correspondence being a hypothesis, an
enumeration of the tagged names by positions, rather than a bundled
isomorphism. Every reduction into this entry crosses this lemma twice, and the
certificate's adequacy crosses it with the *decoded* list.

The enumeration is stated at the *coerced* index `↑(e a)`, which is the form a
`Fin`-valued naming map produces and the form the `getElem` lemmas for appended
lists consume; rewriting a `getElem` index is what the phrasing avoids. -/
theorem sequencing_iff_of_enum {α : Type} [Fintype α] (l r d : α → ℕ)
    (x : SequencingInstance) (e : α ≃ Fin x.tasks.length)
    (henum : ∀ a, x.tasks[((e a) : ℕ)] = (l a, r a, d a)) :
    SEQUENCING x ↔ ∃ σ, IsSequencing l r d σ := by
  have hL : SEQUENCING x ↔ ∃ σ : Fin x.tasks.length → ℕ,
      IsSequencing (fun i ↦ x.tasks[i.1].1) (fun i ↦ x.tasks[i.1].2.1)
        (fun i ↦ x.tasks[i.1].2.2) σ := Iff.rfl
  rw [hL, exists_isSequencing_iff_map e.symm]
  simp only [Equiv.symm_symm]
  refine exists_congr fun σ ↦ ?_
  have h1 : (fun a ↦ x.tasks[((e a) : ℕ)].1) = l := funext fun a ↦ by rw [henum a]
  have h2 : (fun a ↦ x.tasks[((e a) : ℕ)].2.1) = r := funext fun a ↦ by rw [henum a]
  have h3 : (fun a ↦ x.tasks[((e a) : ℕ)].2.2) = d := funext fun a ↦ by rw [henum a]
  rw [h1, h2, h3]

end Hardness