Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

One family for serial and parallel batching

Lax434175.BatchFamily · concepts/Lax434175/BatchFamily.lean · lax-434175

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Serial and parallel batching share one machine model, in which a schedule partitions the jobs into numbered batches and gives every batch a start time and a processing time. All jobs of a batch start when the batch starts and complete when it completes, at its start plus its processing time. A schedule is feasible for this model if a setup precedes every batch, as in batch scheduling.

    The batching field has the values serial and parallel: the processing time of every batch is the sum, or the maximum, of the processing times of its jobs. The two values are incomparable. The other fields are those of batching.

    A batching problem in a mode determines the problem of this family with the same values and that mode.

    Theorem. The two problems are special cases of each other. The fields of the family are sound, so that a specification that is field by field a special case of another describes a special case of the other's problem, and one that reduces to another describes a problem whose decision version reduces to that of the other.

    Concept map
    14 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 faithful proven

    2 family_sound proven

    3 reducible_of_reduces proven

    4 specialCase_of_le proven

    Lean source view on GitHub

    1import Lax434175.BatchProblems
    2
    3/-!
    4---
    5title: One family for serial and parallel batching
    6type: theorem
    7---
    8Serial and parallel batching share one machine model, in which a schedule
    9partitions the jobs into numbered batches and gives every batch a start time
    10and a processing time. All jobs of a batch start when the batch starts and
    11complete when it completes, at its start plus its processing time. A
    12schedule is feasible for this model if a setup precedes every batch, as in
    13batch scheduling.
    14
    15The batching field has the values serial and parallel: the processing time of
    16every batch is the sum, or the maximum, of the processing times of its jobs.
    17The two values are incomparable. The other fields are those of batching.
    18
    19A batching problem in a mode determines the problem of this family with the
    20same values and that mode.
    21
    22**Theorem.** The two problems are special cases of each other. The fields of
    23the family are sound, so that a specification that is field by field a
    24special case of another describes a special case of the other's problem, and
    25one that reduces to another describes a problem whose decision version
    26reduces to that of the other.
    27-/
    28
    29namespace Lax434175.BatchFamily
    30open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    31open Lax434175
    32open Lax434175.Batching (Inst Capacity ProcessingTimes members)
    33
    34/-- A batch schedule with the processing time of every batch. -/
    35structure Sched (x : Inst) where
    36 /-- The number of the batch of a job. -/
    37 batch : Fin x.jobs → ℕ
    38 /-- The start time of a batch. -/
    39 start : ℕ → ℕ
    40 /-- The processing time of a batch. -/
    41 length : ℕ → ℕ
    42
    43/-- The batches and start times of a schedule. -/
    44def Sched.plain {x : Inst} (σ : Sched x) : Batching.Sched x := ⟨σ.batch, σ.start⟩
    45
    46/-- The completion time of a batch. -/
    47def finish {x : Inst} (σ : Sched x) (k : ℕ) : ℕ := σ.start k + σ.length k
    48
    49/-- A setup precedes every batch. -/
    50def feasible (x : Inst) (σ : Sched x) : Prop :=
    51 (∀ j, x.setup ≤ σ.start (σ.batch j)) ∧
    52 ∀ i j, σ.batch i < σ.batch j → finish σ (σ.batch i) + x.setup ≤ σ.start (σ.batch j)
    53
    54/-- The kernel of batch scheduling. -/
    55def kernel : Kernel where
    56 Inst := Inst
    57 jobs := Inst.jobs
    58 release := Inst.r
    59 Sched := Sched
    60 feasible := feasible
    61 start _ σ j := (σ.start (σ.batch j) : NNRat)
    62 completion _ σ j := (finish σ (σ.batch j) : NNRat)
    63
    64def modeLe : Batching.Mode → Batching.Mode → Bool
    65 | .serial, .serial | .parallel, .parallel => true
    66 | _, _ => false
    67
    68/-- The batching field. -/
    69def mode : Module kernel where
    70 Value := Batching.Mode
    71 Data _ _ := Unit
    72 admits _ _ _ := True
    73 constraint v x _ σ := ∀ k, σ.length k = Batching.length v x σ.plain k
    74 le := modeLe
    75 embed _ _ _ := ()
    76
    77/-- The capacity field. -/
    78def capacity : Module kernel where
    79 Value := Capacity
    80 Data := Capacity.Data
    81 admits _ _ _ := True
    82 constraint v _ d σ := ∀ k, ∑ j ∈ members σ.plain k, v.size d j ≤ v.bound d
    83 le := Capacity.le
    84 embed := Capacity.embed
    85
    86/-- The processing-time field. -/
    87def processingTimes : Module kernel :=
    88 Module.ofRestriction ProcessingTimes ProcessingTimes.holds
    89 (fun v w => decide (v.rank ≤ w.rank))
    90
    91/-- The fields of the family: batching and the fields of batch scheduling. -/
    92inductive FieldName
    93 | mode
    94 | field (i : BatchProblems.FieldName)
    95 deriving DecidableEq
    96
    97instance : Fintype FieldName where
    98 elems := {.mode, .field .capacity, .field .jobCount, .field .processingTimes,
    99 .field .releaseDates, .field .deadlines, .field .precedence}
    100 complete x := by
    101 cases x with
    102 | mode => decide
    103 | field i => cases i <;> decide
    104
    105/-- The batching problems. -/
    106abbrev family : Family kernel :=
    107 Thresholds.family FieldName fun
    108 | .mode => mode
    109 | .field .capacity => capacity
    110 | .field .jobCount => Counts.module _ kernel.jobs
    111 | .field .processingTimes => processingTimes
    112 | .field .releaseDates => ReleaseDates.module _
    113 | .field .deadlines => Deadlines.module _
    114 | .field .precedence => Precedence.oneMachine _
    115
    116instance : Fintype family.ModuleName :=
    117 inferInstanceAs (Fintype FieldName)
    118
    119/-- The specification `1 | β | γ` of a batching problem. -/
    120def spec (mode : Batching.Mode) (capacity : Capacity)
    121 (jobCount : Counts.Bound := .any)
    122 (processingTimes : ProcessingTimes := .arbitrary)
    123 (release : ReleaseDates.Value := .none)
    124 (deadline : Deadlines.Value := .none)
    125 (precedence : Precedence.Value := .none)
    126 (objective : Objectives.Value) : Spec family where
    127 module
    128 | .mode => mode
    129 | .field .capacity => capacity
    130 | .field .jobCount => jobCount
    131 | .field .processingTimes => processingTimes
    132 | .field .releaseDates => release
    133 | .field .deadlines => deadline
    134 | .field .precedence => precedence
    135 objective := objective
    136
    137/-- The specification of the family with the values of a batching problem in
    138a mode. -/
    139def ofSpec (m : Batching.Mode) (s : Spec (BatchProblems.family m)) : Spec family where
    140 module
    141 | .mode => m
    142 | .field .capacity => s.module .capacity
    143 | .field .jobCount => s.module .jobCount
    144 | .field .processingTimes => s.module .processingTimes
    145 | .field .releaseDates => s.module .releaseDates
    146 | .field .deadlines => s.module .deadlines
    147 | .field .precedence => s.module .precedence
    148 objective := s.objective
    149
    150axiom faithful (m : Batching.Mode) (s : Spec (BatchProblems.family m)) :
    151 SpecialCase (problem _ s) (problem family (ofSpec m s)) ∧
    152 SpecialCase (problem family (ofSpec m s)) (problem _ s)
    153
    154axiom family_sound : family.Sound
    155
    156axiom specialCase_of_le {s t : Spec family} :
    157 s.le t → SpecialCase (problem family s) (problem family t)
    158
    159axiom reducible_of_reduces {s t : Spec family} :
    160 Thresholds.Reduces s t → Reducible (problem family s) (problem family t)
    161
    162end Lax434175.BatchFamily
    163
    Show ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…