Lax Lean Archive

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

Batching problems in three-field notation

Lax434175.BatchProblems · concepts/Lax434175/BatchProblems.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

    The family of batching problems in a mode has the constraint fields capacity, number of jobs, processing times, release dates, deadlines and precedence constraints, and the completion-time objectives.

    A problem 1∣β∣γ1 \mid \beta \mid \gamma whose β\beta contains s-batch or p-batch is one specification of the family of serial or of parallel batching. For example 1∣p-batch(∞)∣∑wjCj1 \mid \text{p-batch}(\infty) \mid \sum w_j C_j and 1∣p-batch,rj∣∑wjTj1 \mid \text{p-batch}, r_j \mid \sum w_j T_j are the specifications below. The concept on one family for batching joins the two modes into a single family with a batching field.

    Theorem. In both modes, a specification that reduces to another describes a problem whose decision version reduces to that of the other; if it is field by field a special case, it describes a special case.

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

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

    1 family_sound proven

    2 reducible_of_reduces proven

    3 specialCase_of_le proven

    Lean source view on GitHub

    1import Lax434175.Assembly
    2import Lax434175.Counts
    3import Lax434175.ReleaseDates
    4import Lax434175.Deadlines
    5import Lax434175.Precedence
    6import Lax434175.Thresholds
    7import Lax434175.Batching
    8
    9/-!
    10---
    11title: Batching problems in three-field notation
    12type: theorem
    13---
    14The family of batching problems in a mode has the constraint fields
    15capacity, number of jobs, processing times, release dates, deadlines and
    16precedence constraints, and the completion-time objectives.
    17
    18A problem 1∣β∣γ1 \mid \beta \mid \gamma whose β\beta contains s-batch or
    19p-batch is one specification of the family of serial or of parallel
    20batching. For example 1∣p-batch(∞)∣∑wjCj1 \mid \text{p-batch}(\infty) \mid \sum w_j C_j and
    211∣p-batch,rj∣∑wjTj1 \mid \text{p-batch}, r_j \mid \sum w_j T_j are the specifications below.
    22The concept on one family for batching joins the two modes into a single
    23family with a batching field.
    24
    25**Theorem.** In both modes, a specification that reduces to another
    26describes a problem whose decision version reduces to that of the other; if
    27it is field by field a special case, it describes a special case.
    28-/
    29
    30namespace Lax434175.BatchProblems
    31open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    32open Lax434175
    33
    34/-- The constraint fields of the family. -/
    35inductive FieldName
    36 | capacity
    37 | jobCount
    38 | processingTimes
    39 | releaseDates
    40 | deadlines
    41 | precedence
    42 deriving DecidableEq
    43
    44instance : Fintype FieldName where
    45 elems := {.capacity, .jobCount, .processingTimes, .releaseDates, .deadlines, .precedence}
    46 complete x := by cases x <;> decide
    47
    48/-- The batching problems of a mode. -/
    49abbrev family (mode : Batching.Mode) : Family (Batching.kernel mode) :=
    50 Thresholds.family FieldName fun
    51 | .capacity => Batching.capacity mode
    52 | .jobCount => Counts.module _ (Batching.kernel mode).jobs
    53 | .processingTimes => Batching.processingTimes mode
    54 | .releaseDates => ReleaseDates.module _
    55 | .deadlines => Deadlines.module _
    56 | .precedence => Precedence.oneMachine _
    57
    58/-- The specification `1 | β | γ` of a batching problem. -/
    59def spec (mode : Batching.Mode) (capacity : Batching.Capacity)
    60 (jobCount : Counts.Bound := .any)
    61 (processingTimes : Batching.ProcessingTimes := .arbitrary)
    62 (release : ReleaseDates.Value := .none)
    63 (deadline : Deadlines.Value := .none)
    64 (precedence : Precedence.Value := .none)
    65 (objective : Objectives.Value) : Spec (family mode) where
    66 module
    67 | .capacity => capacity
    68 | .jobCount => jobCount
    69 | .processingTimes => processingTimes
    70 | .releaseDates => release
    71 | .deadlines => deadline
    72 | .precedence => precedence
    73 objective := objective
    74
    75/-- `1 | p-batch(∞) | Σw_jC_j` -/
    76def parallel_unbounded_sumWC : Spec (family .parallel) :=
    77 spec _ (capacity := .unbounded) (objective := .sumWC)
    78
    79/-- `1 | p-batch, r_j | Σw_jT_j` -/
    80def parallel_bounded_release_sumWT : Spec (family .parallel) :=
    81 spec _ (capacity := .bounded) (release := .releaseDates) (objective := .sumWT)
    82
    83axiom family_sound (mode : Batching.Mode) : (family mode).Sound
    84
    85axiom specialCase_of_le (mode : Batching.Mode) {s t : Spec (family mode)} :
    86 s.le t → SpecialCase (problem (family mode) s) (problem (family mode) t)
    87
    88axiom reducible_of_reduces (mode : Batching.Mode) {s t : Spec (family mode)} :
    89 Thresholds.Reduces s t → Reducible (problem (family mode) s) (problem (family mode) t)
    90
    91end Lax434175.BatchProblems
    92
    Show 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…