Lax Lean Archive

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

Preemptive shop problems in three-field notation

Lax434175.PreemptiveShopProblems · concepts/Lax434175/PreemptiveShopProblems.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 preemptive shop problems has the constraint fields shop type, machines of the operations, number of machines, number of jobs, processing times, release dates, deadlines and precedence constraints between jobs, and the completion-time objectives.

    A problem α∣β∣γ\alpha \mid \beta \mid \gamma with α\alpha one of OO, FF, JJ whose β\beta contains pmtn\mathrm{pmtn} is one specification of this family. For example J2∣pmtn∣Cmax⁡J2 \mid \mathrm{pmtn} \mid C_{\max} is the specification below.

    Theorem. A specification that is field by field a special case of another describes a special case of the other's problem, and a specification 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 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.PreemptiveShops
    8
    9/-!
    10---
    11title: Preemptive shop problems in three-field notation
    12type: theorem
    13---
    14The family of preemptive shop problems has the constraint fields shop type,
    15machines of the operations, number of machines, number of jobs, processing
    16times, release dates, deadlines and precedence constraints between jobs,
    17and the completion-time objectives.
    18
    19A problem α∣β∣γ\alpha \mid \beta \mid \gamma with α\alpha one of OO, FF, JJ
    20whose β\beta contains pmtn\mathrm{pmtn} is one specification of this family.
    21For example J2∣pmtn∣Cmax⁡J2 \mid \mathrm{pmtn} \mid C_{\max} is the specification below.
    22
    23**Theorem.** A specification that is field by field a special case of
    24another describes a special case of the other's problem, and a specification
    25that reduces to another describes a problem whose decision version reduces
    26to that of the other.
    27-/
    28
    29namespace Lax434175.PreemptiveShopProblems
    30open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    31open Lax434175
    32
    33/-- The constraint fields of the family. -/
    34inductive FieldName
    35 | shopType
    36 | machineSets
    37 | machineCount
    38 | jobCount
    39 | processingTimes
    40 | releaseDates
    41 | deadlines
    42 | precedence
    43 deriving DecidableEq
    44
    45instance : Fintype FieldName where
    46 elems := {.shopType, .machineSets, .machineCount, .jobCount, .processingTimes, .releaseDates,
    47 .deadlines, .precedence}
    48 complete x := by cases x <;> decide
    49
    50/-- The preemptive shop problems. -/
    51abbrev family : Family PreemptiveShops.kernel :=
    52 Thresholds.family FieldName fun
    53 | .shopType => PreemptiveShops.shopType
    54 | .machineSets => PreemptiveShops.machineSets
    55 | .machineCount => Counts.module _ PreemptiveShops.machines 1
    56 | .jobCount => Counts.module _ PreemptiveShops.kernel.jobs
    57 | .processingTimes => PreemptiveShops.processingTimes
    58 | .releaseDates => ReleaseDates.module _
    59 | .deadlines => Deadlines.module _
    60 | .precedence => Precedence.module _ PreemptiveShops.machines
    61
    62/-- The specification `α | pmtn, β | γ` of a preemptive shop problem. -/
    63def spec (shopType : Shops.ShopType)
    64 (machineSets : Shops.Machines)
    65 (machineCount : Counts.Bound := .any)
    66 (jobCount : Counts.Bound := .any)
    67 (processingTimes : Shops.ProcessingTimes := .arbitrary)
    68 (release : ReleaseDates.Value := .none)
    69 (deadline : Deadlines.Value := .none)
    70 (precedence : Precedence.Value := .none)
    71 (objective : Objectives.Value) : Spec family where
    72 module
    73 | .shopType => shopType
    74 | .machineSets => machineSets
    75 | .machineCount => machineCount
    76 | .jobCount => jobCount
    77 | .processingTimes => processingTimes
    78 | .releaseDates => release
    79 | .deadlines => deadline
    80 | .precedence => precedence
    81 objective := objective
    82
    83/-- `J2 | pmtn | C_max` -/
    84def job2_makespan : Spec family :=
    85 spec (shopType := .job) (machineSets := .dedicated) (machineCount := .atMost 2)
    86 (objective := .makespan)
    87
    88axiom family_sound : family.Sound
    89
    90axiom specialCase_of_le {s t : Spec family} :
    91 s.le t → SpecialCase (problem family s) (problem family t)
    92
    93axiom reducible_of_reduces {s t : Spec family} :
    94 Thresholds.Reduces s t → Reducible (problem family s) (problem family t)
    95
    96end Lax434175.PreemptiveShopProblems
    97
    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…