ACMStaffing.lean

import Std

namespace ACMStaffing

/- Known-workload staffing with four declared candidates and at most four
   start slots. Concrete S1/S2 certificates use exact Rat values. Theorems
   range over every roster mask and every physically admitted route list;
   they do not infer recruitability or unknown-arrival performance. -/

abbrev Worker := Fin 4
abbrev Roster := Fin 16
abbrev Cell := Worker × Nat

inductive Kind where
  | a1 | b1 | a2 | b2 | ab
  deriving DecidableEq, Repr

inductive Route where
  | outside
  | solo (worker : Worker) (start : Fin 4)
  | pair (workerA workerB : Worker) (start : Fin 4)
  deriving DecidableEq, Repr

structure Job where
  kind : Kind
  release : Nat
  deadline : Nat
  value : Rat
  outside : Rat

structure Model where
  horizon : Nat
  skillA : Worker → Nat
  skillB : Worker → Nat
  available : Worker → Nat → Bool
  wage : Worker → Rat
  opportunity : Worker → Rat
  setup : Rat
  handoff : Nat
  pairExpense : Rat
  jobs : List Job

def workers : List Worker := [0,1,2,3]
def rosters : List Roster := [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]

theorem worker_mem : ∀ w : Worker, w ∈ workers := by decide +kernel

theorem roster_mem : ∀ r : Roster, r ∈ rosters := by decide +kernel

def routes : List Route := [.outside] ++
  workers.flatMap (fun w =>
    workers.map (fun t => .solo w t)) ++
  workers.flatMap (fun a =>
    workers.flatMap (fun b =>
      workers.map (fun t => .pair a b t)))

theorem every_route_enumerated (a : Route) : a ∈ routes := by
  cases a <;> simp [routes, worker_mem]

def selected (r : Roster) (w : Worker) : Bool := r.val.testBit w.val

def participants : Route → List Worker
  | .outside => []
  | .solo w _ => [w]
  | .pair a b _ => [a,b]

def start : Route → Nat
  | .outside => 0
  | .solo _ t | .pair _ _ t => t.val

def duration (m : Model) (j : Job) : Route → Nat
  | .outside => 0
  | .solo _ _ => if j.kind = .ab then 2 else 1
  | .pair _ _ _ => 1 + m.handoff

def cells (m : Model) (j : Job) (a : Route) : List Cell :=
  (participants a).flatMap (fun w =>
    (List.range (duration m j a)).map (fun k => (w,start a+k)))

def qualified (m : Model) (j : Job) : Route → Bool
  | .outside => true
  | .solo w _ => match j.kind with
    | .a1 => decide (1 ≤ m.skillA w)
    | .b1 => decide (1 ≤ m.skillB w)
    | .a2 => decide (2 ≤ m.skillA w)
    | .b2 => decide (2 ≤ m.skillB w)
    | .ab => decide (1 ≤ m.skillA w ∧ 1 ≤ m.skillB w)
  | .pair a b _ => decide (j.kind = .ab ∧ a ≠ b ∧
      1 ≤ m.skillA a ∧ 1 ≤ m.skillB b)

def legal (m : Model) (r : Roster) (j : Job) (a : Route) : Bool :=
  match a with
  | .outside => true
  | _ => qualified m j a &&
      (participants a).all (selected r) &&
      decide (j.release ≤ start a ∧ start a + duration m j a ≤ j.deadline ∧
        j.deadline ≤ m.horizon ∧ m.horizon ≤ 4) &&
      (cells m j a).all (fun c => m.available c.1 c.2)

def clear (fresh used : List Cell) : Bool :=
  fresh.all (fun c => !used.contains c)

def admitted (m : Model) (r : Roster) (j : Job) (used : List Cell) : List Route :=
  routes.filter (fun a => legal m r j a && clear (cells m j a) used)

theorem physically_legal_is_enumerated (m : Model) (r : Roster) (j : Job)
    (used : List Cell) (a : Route) (hl : legal m r j a = true)
    (hc : clear (cells m j a) used = true) : a ∈ admitted m r j used := by
  simp [admitted, every_route_enumerated, hl, hc]

def gain (m : Model) (j : Job) : Route → Rat
  | .outside => 0
  | .solo _ _ => j.value - j.outside
  | .pair _ _ _ => j.value - j.outside - m.pairExpense

def charge (m : Model) (r : Roster) : Rat :=
  (workers.map (fun w =>
    if selected r w then m.wage w + m.opportunity w else 0)).foldl (· + ·) 0 +
    if r.val = 0 then 0 else m.setup

/-- Physical feasibility, independently stated from the enumerator. Every
    job has exactly one route; the reservation list includes both pair members. -/
def Physical (m : Model) (r : Roster) : List Job → List Cell → List Route → Prop
  | [], _, [] => True
  | j :: js, used, a :: as => legal m r j a = true ∧
      clear (cells m j a) used = true ∧ Physical m r js (cells m j a ++ used) as
  | _, _, _ => False

def service (m : Model) : List Job → List Route → Rat
  | j :: js, a :: as => gain m j a + service m js as
  | _, _ => 0

def net (m : Model) (r : Roster) (as : List Route) : Rat :=
  service m m.jobs as - charge m r

/-- An exhaustive finite upper-bound certificate. It checks every physically
    legal continuation, not merely the supplied attaining schedule. -/
def within (m : Model) (r : Roster) : List Job → List Cell → Rat → Bool
  | [], _, budget => decide (0 ≤ budget)
  | j :: js, used, budget => (admitted m r j used).all (fun a =>
      within m r js (cells m j a ++ used) (budget - gain m j a))

theorem certificate_bounds_every_schedule (m : Model) (r : Roster)
    (js : List Job) (used : List Cell) (budget : Rat) (as : List Route)
    (hc : within m r js used budget = true) (hp : Physical m r js used as) :
    service m js as ≤ budget := by
  induction js generalizing used budget as with
  | nil =>
    cases as with
    | nil => simpa [within, service] using hc
    | cons a as => exact False.elim hp
  | cons j js ih =>
    cases as with
    | nil => exact False.elim hp
    | cons a as =>
      obtain ⟨hl,hclear,ht⟩ := hp
      have ha := physically_legal_is_enumerated m r j used a hl hclear
      have hall := List.all_eq_true.mp hc
      have hb := hall a ha
      have hs := ih (cells m j a ++ used) (budget - gain m j a) as hb ht
      simp only [service]
      grind

def staffingCertificate (m : Model) (upper : Rat) : Bool :=
  rosters.all (fun r => within m r m.jobs [] (upper + charge m r))

theorem certificate_bounds_every_roster (m : Model) (upper : Rat)
    (hc : staffingCertificate m upper = true) (r : Roster) (as : List Route)
    (hp : Physical m r m.jobs [] as) : net m r as ≤ upper := by
  have hr : r ∈ rosters := roster_mem r
  have hb := List.all_eq_true.mp hc r hr
  have hs := certificate_bounds_every_schedule m r m.jobs [] (upper + charge m r) as hb hp
  simp only [net]
  grind

/-- Generic certificate plus witness is an optimum among all admitted rosters
    and physical schedules, including outside routes and redundant paid staff. -/
theorem attaining_certificate_is_global_optimum (m : Model) (upper : Rat)
    (hc : staffingCertificate m upper = true) (r : Roster) (as : List Route)
    (hp : Physical m r m.jobs [] as) (hv : net m r as = upper) :
    Physical m r m.jobs [] as ∧
      ∀ r' as', Physical m r' m.jobs [] as' → net m r' as' ≤ net m r as := by
  refine ⟨hp, ?_⟩
  intro r' as' h'
  rw [hv]
  exact certificate_bounds_every_roster m upper hc r' as' h'

/-- Optional access to additional selected workers preserves every physical
    schedule; existing skills, calendars and route technology are unchanged. -/
def RosterSubset (r r' : Roster) : Prop :=
  ∀ w, selected r w = true → selected r' w = true

theorem legal_mono (m : Model) (r r' : Roster) (j : Job) (a : Route)
    (hr : RosterSubset r r') (hl : legal m r j a = true) :
    legal m r' j a = true := by
  have hp : (participants a).all (selected r) = true := by
    cases a <;> simp_all [legal, Bool.and_eq_true, participants]
  have hp' : (participants a).all (selected r') = true := by
    apply List.all_eq_true.mpr
    intro w hw
    exact hr w (List.all_eq_true.mp hp w hw)
  cases a <;> simp_all [legal, Bool.and_eq_true]

theorem schedule_emulation (m : Model) (r r' : Roster)
    (hr : RosterSubset r r') (js : List Job) (used : List Cell) (as : List Route)
    (hp : Physical m r js used as) : Physical m r' js used as := by
  induction js generalizing used as with
  | nil => cases as <;> exact hp
  | cons j js ih =>
    cases as with
    | nil => exact hp
    | cons a as =>
      obtain ⟨hl,hc,ht⟩ := hp
      exact ⟨legal_mono m r r' j a hr hl, hc, ih _ _ ht⟩

theorem optimal_service_nondecreasing (m : Model) (r r' : Roster)
    (hr : RosterSubset r r') (old best : List Route)
    (ho : Physical m r m.jobs [] old)
    (hb : ∀ as, Physical m r' m.jobs [] as →
      service m m.jobs as ≤ service m m.jobs best) :
    service m m.jobs old ≤ service m m.jobs best := by
  exact hb old (schedule_emulation m r r' hr m.jobs [] old ho)

/-- Once each roster's schedule is optimized, this exact criterion separates
    productive capacity gains from mandatory reservation charges. -/
theorem net_expansion_break_even (m : Model) (r r' : Roster) (as as' : List Route) :
    net m r as < net m r' as' ↔
      charge m r' - charge m r < service m m.jobs as' - service m m.jobs as := by
  simp only [net]
  grind

/- Frozen base pool. P1=0, P2=1, SA=2, SB=3. All values are in the
   same exact rational units as the JavaScript fixtures, not doubled scores. -/
def base : Model where
  horizon := 2
  skillA := fun w => if w.val = 2 then 2 else if w.val = 3 then 0 else 1
  skillB := fun w => if w.val = 3 then 2 else if w.val = 2 then 0 else 1
  available := fun _ _ => true
  wage := fun w => if w.val < 2 then 2 else 1
  opportunity := fun w => if w.val < 2 then 1 else 1/2
  setup := 0
  handoff := 1
  pairExpense := 1
  jobs := []

def AB (deadline : Nat) : Job := ⟨.ab,0,deadline,8,2⟩
def A2 (deadline : Nat) : Job := ⟨.a2,0,deadline,8,2⟩
def B2 (deadline : Nat) : Job := ⟨.b2,0,deadline,8,2⟩
def S1 : Model := {base with jobs := [AB 2]}
def S2 : Model := {base with horizon := 1, jobs := [A2 1,B2 1]}

def coreRoster : Roster := 1
def coreWitness : List Route := [.solo 0 0]
def specialists : Roster := 12
def specialistWitness : List Route := [.solo 2 0,.solo 3 0]

theorem S1_certificate : staffingCertificate S1 3 = true := by decide +kernel
theorem S1_attains : Physical S1 coreRoster S1.jobs [] coreWitness ∧
    net S1 coreRoster coreWitness = 3 := by
  constructor
  · simp only [S1, coreWitness, Physical]; decide +kernel
  · decide +kernel

theorem S1_core_is_globally_optimal :
    Physical S1 coreRoster S1.jobs [] coreWitness ∧
      ∀ r as, Physical S1 r S1.jobs [] as → net S1 r as ≤ 3 := by
  exact ⟨S1_attains.1, fun r as hp => certificate_bounds_every_roster S1 3 S1_certificate r as hp⟩

theorem S2_certificate : staffingCertificate S2 9 = true := by decide +kernel
theorem S2_attains : Physical S2 specialists S2.jobs [] specialistWitness ∧
    net S2 specialists specialistWitness = 9 := by
  constructor
  · simp only [S2, specialistWitness, Physical]; decide +kernel
  · decide +kernel

theorem S2_specialists_are_globally_optimal :
    Physical S2 specialists S2.jobs [] specialistWitness ∧
      ∀ r as, Physical S2 r S2.jobs [] as → net S2 r as ≤ 9 := by
  exact ⟨S2_attains.1, fun r as hp => certificate_bounds_every_roster S2 9 S2_certificate r as hp⟩

/-- The broad workers cannot jointly manufacture the missing deep skill. -/
theorem S2_breadth_does_not_supply_depth :
    qualified S2 (A2 1) (.solo 0 0) = false ∧
    qualified S2 (A2 1) (.solo 1 0) = false ∧
    qualified S2 (A2 1) (.pair 0 1 0) = false := by decide +kernel

/- Further bounded certificates: the optimum can be hybrid, and the precise
   coordination boundary admits two distinct staffing compositions. -/
def S3 : Model := {base with jobs := [A2 2,AB 2]}
def hybridRoster : Roster := 5
def hybridWitness : List Route := [.solo 2 0,.solo 0 0]
theorem S3_certificate : staffingCertificate S3 (15/2) = true := by decide +kernel
theorem S3_attains : Physical S3 hybridRoster S3.jobs [] hybridWitness ∧
    net S3 hybridRoster hybridWitness = 15/2 := by
  constructor
  · simp only [S3, hybridWitness, Physical]; decide +kernel
  · decide +kernel
theorem S3_hybrid_is_globally_optimal :
    ∀ r as, Physical S3 r S3.jobs [] as → net S3 r as ≤ 15/2 :=
  fun r as hp => certificate_bounds_every_roster S3 (15/2) S3_certificate r as hp

def S8 : Model := {base with handoff := 0, pairExpense := 3/2, jobs := [AB 2,AB 2]}
def twoBroad : Roster := 3
def twoBroadWitness : List Route := [.solo 0 0,.solo 1 0]
def parallelPairWitness : List Route := [.pair 2 3 0,.pair 2 3 1]
theorem S8_certificate : staffingCertificate S8 6 = true := by decide +kernel
theorem S8_distinct_compositions_attain :
    Physical S8 twoBroad S8.jobs [] twoBroadWitness ∧
    Physical S8 specialists S8.jobs [] parallelPairWitness ∧
    net S8 twoBroad twoBroadWitness = 6 ∧
    net S8 specialists parallelPairWitness = 6 ∧ twoBroad ≠ specialists := by
  simp only [S8, twoBroadWitness, parallelPairWitness, Physical]
  decide +kernel
theorem S8_both_are_globally_optimal :
    ∀ r as, Physical S8 r S8.jobs [] as → net S8 r as ≤ 6 :=
  fun r as hp => certificate_bounds_every_roster S8 6 S8_certificate r as hp


end ACMStaffing