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

Shop problems in three-field notation

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

proven

Loading review…

Sign in with ORCID

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 shop problems has the constraint fields shop type, machines of the operations, number of machines, number of jobs, processing times, no-wait, no-idle, transportation delays, a server, batch setups, 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, possibly followed by a number of machines, is one specification of this family. Without an entry on machine sets, the operations of an open shop or flow shop occupy the machines by position and those of a job shop occupy dedicated machines. For example F2∣∣Cmax⁡F2 \mid\mid C_{\max} and J∣rj∣Lmax⁡J \mid r_j \mid L_{\max} are the specifications below. The concept on one family for shops joins these problems and the preemptive shop problems into a single family with an interruption field.

    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. In particular F2∣∣Cmax⁡F2 \mid\mid C_{\max} is a special case of J∣rj∣Lmax⁡J \mid r_j \mid L_{\max}.

    Concept map
    17 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.

    2 flow2_makespan_specialCase proven

    3 reducible_of_reduces 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.Shops
    8import Lax434175.Transportation
    9import Lax434175.Servers
    10import Lax434175.ShopExtras
    11
    12/-!
    13---
    14title: Shop problems in three-field notation
    15type: theorem
    16---
    17The family of shop problems has the constraint fields shop type, machines of
    18the operations, number of machines, number of jobs, processing times, no-wait, no-idle, transportation
    19delays, a server, batch setups, release dates, deadlines and precedence constraints between jobs, and the completion-time objectives.
    20
    21A problem α∣β∣γ\alpha \mid \beta \mid \gamma with α\alpha one of OO, FF, JJ,
    22possibly followed by a number of machines, is one specification of this
    23family. Without an entry on machine sets, the operations of an open shop or
    24flow shop occupy the machines by position and those of a job shop occupy
    25dedicated machines. For example F2∣∣Cmax⁡F2 \mid\mid C_{\max} and
    26J∣rj∣Lmax⁡J \mid r_j \mid L_{\max} are the specifications below.
    27The concept on one family for shops joins these problems and the preemptive
    28shop problems into a single family with an interruption field.
    29
    30**Theorem.** A specification that is field by field a special case of
    31another describes a special case of the other's problem, and a specification
    32that reduces to another describes a problem whose decision version reduces
    33to that of the other. In particular
    34F2∣∣Cmax⁡F2 \mid\mid C_{\max} is a special case of J∣rj∣Lmax⁡J \mid r_j \mid L_{\max}.
    35-/
    36
    37namespace Lax434175.ShopProblems
    38open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    39open Lax434175
    40
    41/-- The constraint fields of the family. -/
    42inductive FieldName
    43 | shopType
    44 | machineSets
    45 | machineCount
    46 | jobCount
    47 | processingTimes
    48 | noWait
    49 | transportation
    50 | server
    51 | noIdle
    52 | batchSetups
    53 | releaseDates
    54 | deadlines
    55 | precedence
    56 deriving DecidableEq
    57
    58instance : Fintype FieldName where
    59 elems := {.shopType, .machineSets, .machineCount, .jobCount, .processingTimes, .noWait, .transportation, .server, .noIdle, .batchSetups, .releaseDates,
    60 .deadlines, .precedence}
    61 complete x := by cases x <;> decide
    62
    63/-- The shop problems. -/
    64abbrev family : Family Shops.kernel :=
    65 Thresholds.family FieldName fun
    66 | .shopType => Shops.shopType
    67 | .machineSets => Shops.machineSets
    68 | .machineCount => Counts.module _ Shops.machines 1
    69 | .jobCount => Counts.module _ Shops.kernel.jobs
    70 | .processingTimes => Shops.processingTimes
    71 | .noWait => Shops.noWait
    72 | .transportation => Transportation.module
    73 | .server => Servers.shop
    74 | .noIdle => ShopExtras.noIdle
    75 | .batchSetups => ShopExtras.batchSetups
    76 | .releaseDates => ReleaseDates.module _
    77 | .deadlines => Deadlines.module _
    78 | .precedence => Precedence.module _ Shops.machines
    79
    80instance : Fintype family.ModuleName := inferInstanceAs (Fintype FieldName)
    81
    82/-- The specification `α | β | γ` of a shop problem. -/
    83def spec (shopType : Shops.ShopType)
    84 (machineSets : Shops.Machines)
    85 (machineCount : Counts.Bound := .any)
    86 (jobCount : Counts.Bound := .any)
    87 (processingTimes : Shops.ProcessingTimes := .arbitrary)
    88 (waiting : Shops.NoWait := .none)
    89 (transportation : Transportation.Value := .none)
    90 (server : Servers.Value := .none)
    91 (idling : ShopExtras.NoIdle := .none)
    92 (setups : ShopExtras.BatchSetups := .none)
    93 (release : ReleaseDates.Value := .none)
    94 (deadline : Deadlines.Value := .none)
    95 (precedence : Precedence.Value := .none)
    96 (objective : Objectives.Value) : Spec family where
    97 module
    98 | .shopType => shopType
    99 | .machineSets => machineSets
    100 | .machineCount => machineCount
    101 | .jobCount => jobCount
    102 | .processingTimes => processingTimes
    103 | .noWait => waiting
    104 | .transportation => transportation
    105 | .server => server
    106 | .noIdle => idling
    107 | .batchSetups => setups
    108 | .releaseDates => release
    109 | .deadlines => deadline
    110 | .precedence => precedence
    111 objective := objective
    112
    113/-- `F2 || C_max` -/
    114def flow2_makespan : Spec family :=
    115 spec (shopType := .flow) (machineSets := .byPosition) (machineCount := .atMost 2) (objective := .makespan)
    116
    117/-- `J | r_j | L_max` -/
    118def job_release_lmax : Spec family :=
    119 spec (shopType := .job) (machineSets := .dedicated) (release := .releaseDates) (objective := .lmax)
    120
    121axiom family_sound : family.Sound
    122
    123axiom specialCase_of_le {s t : Spec family} :
    124 s.le t → SpecialCase (problem family s) (problem family t)
    125
    126axiom reducible_of_reduces {s t : Spec family} :
    127 Thresholds.Reduces s t → Reducible (problem family s) (problem family t)
    128
    129axiom flow2_makespan_specialCase :
    130 SpecialCase (problem family flow2_makespan) (problem family job_release_lmax)
    131
    132end Lax434175.ShopProblems
    133
    Show ProofShow ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…