Lax Lean Archive

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

One family for parallel machines and shops

Lax434175.OperationsFamily · concepts/Lax434175/OperationsFamily.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 problems on parallel machines and the shop problems form one family over scheduling with operations, with the fields of scheduling with operations and the completion-time objectives.

    A problem of the family of parallel machines determines the problem of this family with one operation per job, the same values in the fields of parallel machines, its machine-set value as a value of the machine field, and the value none in the fields of shops. A shop problem determines the problem with its shop type as job structure, identical machines, its machine value, its processing-time value, the same values in the fields of shops, and the value none in the fields of parallel machines.

    Theorem. In both cases the two problems are special cases of each other. In the family, 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, directly or through flow time, describes a problem whose decision version reduces to that of the other.

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

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

    1 family_sound proven

    2 parallel_faithful proven

    3 reducible_of_reduces proven

    4 reducible_of_reducesThroughFlow proven

    5 shop_faithful proven

    6 specialCase_of_le proven

    Lean source view on GitHub

    1import Lax434175.Operations
    2import Lax434175.ParallelFamily
    3
    4/-!
    5---
    6title: One family for parallel machines and shops
    7type: theorem
    8---
    9The problems on parallel machines and the shop problems form one family over
    10scheduling with operations, with the fields of scheduling with operations and
    11the completion-time objectives.
    12
    13A problem of the family of parallel machines determines the problem of this
    14family with one operation per job, the same values in the fields of parallel
    15machines, its machine-set value as a value of the machine field, and the
    16value none in the fields of shops. A shop problem determines the problem with
    17its shop type as job structure, identical machines, its machine value, its
    18processing-time value, the same values in the fields of shops, and the value
    19none in the fields of parallel machines.
    20
    21**Theorem.** In both cases the two problems are special cases of each other.
    22In the family, a specification that is field by field a special case of
    23another describes a special case of the other's problem, and a specification
    24that reduces to another, directly or through flow time, describes a problem
    25whose decision version reduces to that of the other.
    26-/
    27
    28namespace Lax434175.OperationsFamily
    29open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    30open Lax434175 Lax434175.Operations
    31
    32/-- The fields of the family. -/
    33inductive FieldName
    34 | interruption
    35 | jobStructure
    36 | environment
    37 | machineCount
    38 | jobCount
    39 | processingTimes
    40 | machineSets
    41 | releaseDates
    42 | deadlines
    43 | precedence
    44 | communicationDelays
    45 | server
    46 | forbiddenTimes
    47 | encoding
    48 | noWait
    49 | transportation
    50 | noIdle
    51 | batchSetups
    52 deriving DecidableEq
    53
    54instance : Fintype FieldName where
    55 elems := {.interruption, .jobStructure, .environment, .machineCount, .jobCount,
    56 .processingTimes, .machineSets, .releaseDates, .deadlines, .precedence,
    57 .communicationDelays, .server, .forbiddenTimes, .encoding, .noWait, .transportation,
    58 .noIdle, .batchSetups}
    59 complete x := by cases x <;> decide
    60
    61/-- The problems on parallel machines and in shops. -/
    62abbrev family : Family Operations.kernel :=
    63 Thresholds.family FieldName fun
    64 | .interruption => Operations.interruption
    65 | .jobStructure => Operations.jobStructure
    66 | .environment => Operations.environment
    67 | .machineCount => Counts.module _ Operations.machines 1
    68 | .jobCount => Counts.module _ Operations.kernel.jobs
    69 | .processingTimes => Operations.processingTimes
    70 | .machineSets => Operations.machineSets
    71 | .releaseDates => ReleaseDates.module _
    72 | .deadlines => Deadlines.module _
    73 | .precedence => Precedence.module _ Operations.machines
    74 | .communicationDelays => CommunicationDelays.module Operations.model
    75 | .server => Operations.server
    76 | .forbiddenTimes => ForbiddenTimes.module _
    77 | .encoding => ForbiddenTimes.encoding _
    78 | .noWait => Operations.noWait
    79 | .transportation => Operations.transportation
    80 | .noIdle => Operations.noIdle
    81 | .batchSetups => Operations.batchSetups
    82
    83instance : Fintype family.ModuleName :=
    84 inferInstanceAs (Fintype FieldName)
    85
    86/-- The specification `α | β | γ`. -/
    87def spec (interruption : Interruption.Mode := .none)
    88 (shopType : Structure := .single)
    89 (environment : ParallelMachines.Environment := .identical)
    90 (machineCount : Counts.Bound := .any)
    91 (jobCount : Counts.Bound := .any)
    92 (processingTimes : ParallelMachines.ProcessingTimes := .arbitrary)
    93 (machineSets : Machines := .par .none)
    94 (release : ReleaseDates.Value := .none)
    95 (deadline : Deadlines.Value := .none)
    96 (precedence : Precedence.Value := .none)
    97 (communicationDelays : CommunicationDelays.Value := .none)
    98 (server : Servers.Value := .none)
    99 (forbiddenTimes : ForbiddenTimes.Value := .none)
    100 (encoding : ForbiddenTimes.Encoding := .standard)
    101 (waiting : Shops.NoWait := .none)
    102 (transportation : Transportation.Value := .none)
    103 (idling : ShopExtras.NoIdle := .none)
    104 (setups : ShopExtras.BatchSetups := .none)
    105 (objective : Objectives.Value) : Spec family where
    106 module
    107 | .interruption => interruption
    108 | .jobStructure => shopType
    109 | .environment => environment
    110 | .machineCount => machineCount
    111 | .jobCount => jobCount
    112 | .processingTimes => processingTimes
    113 | .machineSets => machineSets
    114 | .releaseDates => release
    115 | .deadlines => deadline
    116 | .precedence => precedence
    117 | .communicationDelays => communicationDelays
    118 | .server => server
    119 | .forbiddenTimes => forbiddenTimes
    120 | .encoding => encoding
    121 | .noWait => waiting
    122 | .transportation => transportation
    123 | .noIdle => idling
    124 | .batchSetups => setups
    125 objective := objective
    126
    127/-- The job structure of a shop type. -/
    128def ofShopType : Shops.ShopType → Structure
    129 | .open => .open
    130 | .flow => .flow
    131 | .job => .job
    132 | .flexibleFlow => .flexibleFlow
    133
    134/-- The processing-time value of a shop value. -/
    135def ofShopTimes : Shops.ProcessingTimes → ParallelMachines.ProcessingTimes
    136 | .unit => .unit
    137 | .equal => .equal
    138 | .arbitrary => .arbitrary
    139
    140/-- The specification of the family with the values of a problem on parallel
    141machines. -/
    142def ofParallel (s : Spec ParallelFamily.family) : Spec family where
    143 module
    144 | .interruption => s.module .interruption
    145 | .jobStructure => Structure.single
    146 | .environment => s.module (.field .environment)
    147 | .machineCount => s.module (.field .machineCount)
    148 | .jobCount => s.module (.field .jobCount)
    149 | .processingTimes => s.module (.field .processingTimes)
    150 | .machineSets => Machines.par (s.module (.field .machineSets))
    151 | .releaseDates => s.module (.field .releaseDates)
    152 | .deadlines => s.module (.field .deadlines)
    153 | .precedence => s.module (.field .precedence)
    154 | .communicationDelays => s.module (.field .communicationDelays)
    155 | .server => s.module (.field .server)
    156 | .forbiddenTimes => s.module (.field .forbiddenTimes)
    157 | .encoding => s.module (.field .encoding)
    158 | .noWait => Shops.NoWait.none
    159 | .transportation => Transportation.Value.none
    160 | .noIdle => ShopExtras.NoIdle.none
    161 | .batchSetups => ShopExtras.BatchSetups.none
    162 objective := s.objective
    163
    164/-- The specification of the family with the values of a shop problem. -/
    165def ofShop (s : Spec ShopFamily.family) : Spec family where
    166 module
    167 | .interruption => s.module .interruption
    168 | .jobStructure => ofShopType (s.module (.field .shopType))
    169 | .environment => ParallelMachines.Environment.identical
    170 | .machineCount => s.module (.field .machineCount)
    171 | .jobCount => s.module (.field .jobCount)
    172 | .processingTimes => ofShopTimes (s.module (.field .processingTimes))
    173 | .machineSets => Machines.shop (s.module (.field .machineSets))
    174 | .releaseDates => s.module (.field .releaseDates)
    175 | .deadlines => s.module (.field .deadlines)
    176 | .precedence => s.module (.field .precedence)
    177 | .communicationDelays => CommunicationDelays.Value.none
    178 | .server => s.module (.field .server)
    179 | .forbiddenTimes => ForbiddenTimes.Value.none
    180 | .encoding => ForbiddenTimes.Encoding.standard
    181 | .noWait => s.module (.field .noWait)
    182 | .transportation => s.module (.field .transportation)
    183 | .noIdle => s.module (.field .noIdle)
    184 | .batchSetups => s.module (.field .batchSetups)
    185 objective := s.objective
    186
    187axiom parallel_faithful (s : Spec ParallelFamily.family) :
    188 SpecialCase (problem _ s) (problem family (ofParallel s)) ∧
    189 SpecialCase (problem family (ofParallel s)) (problem _ s)
    190
    191axiom shop_faithful (s : Spec ShopFamily.family) :
    192 SpecialCase (problem _ s) (problem family (ofShop s)) ∧
    193 SpecialCase (problem family (ofShop s)) (problem _ s)
    194
    195axiom family_sound : family.Sound
    196
    197axiom specialCase_of_le {s t : Spec family} :
    198 s.le t → SpecialCase (problem family s) (problem family t)
    199
    200axiom reducible_of_reduces {s t : Spec family} :
    201 Thresholds.Reduces s t → Reducible (problem family s) (problem family t)
    202
    203axiom reducible_of_reducesThroughFlow {s t : Spec family} :
    204 Thresholds.ReducesThroughFlow s t → Reducible (problem family s) (problem family t)
    205
    206end Lax434175.OperationsFamily
    207
    Show ProofShow ProofShow 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…