Lax Lean Archive

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

No-idle shops and batch setup times

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

    Two further constraint fields of shops.

    The no-idle field has the values "none" and "no-idle". With no-idle, no machine is idle between two operations: every operation that occupies a machine is immediately followed on that machine by another operation, unless no operation on that machine completes later. The two values are incomparable.

    The batch-setup field has the values "none" and "batch setups". With batch setups, every job belongs to a batch and a setup time spqs_{pq} is given for every ordered pair of batches. Two operations of jobs of different batches that share a machine do not interleave, and if one follows the other on a machine, with no operation on that machine in between, the later one may not start before the completion of the earlier one plus the setup time from the batch of the earlier to the batch of the later. The setup is charged only between consecutive operations, as in the usual model of sequence-dependent setups ("when the machine switches"); setup times need not satisfy the triangle inequality. Without batch setups all jobs are read as one batch.

    Theorem. Both fields are sound.

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

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

    1 batchSetups_sound proven

    2 noIdle_sound proven

    Lean source view on GitHub

    1import Lax434175.Shops
    2
    3/-!
    4---
    5title: No-idle shops and batch setup times
    6type: theorem
    7---
    8Two further constraint fields of shops.
    9
    10The no-idle field has the values "none" and "no-idle". With no-idle, no
    11machine is idle between two operations: every operation that occupies a
    12machine is immediately followed on that machine by another operation, unless
    13no operation on that machine completes later. The two values are
    14incomparable.
    15
    16The batch-setup field has the values "none" and "batch setups". With batch
    17setups, every job belongs to a batch and a setup time spqs_{pq} is given for
    18every ordered pair of batches. Two operations of jobs of different batches
    19that share a machine do not interleave, and if one follows the other on a
    20machine, with no operation on that machine in between, the later one may not
    21start before the completion of the earlier one plus the setup time from the
    22batch of the earlier to the batch of the later. The setup is charged only
    23between consecutive operations, as in the usual model of sequence-dependent
    24setups ("when the machine switches"); setup times need not satisfy the
    25triangle inequality. Without batch setups all jobs are read as one batch.
    26
    27**Theorem.** Both fields are sound.
    28-/
    29
    30namespace Lax434175.ShopExtras
    31open Lax434175.Kernels Lax434175.Modules Lax434175.Shops
    32
    33inductive NoIdle
    34 | none
    35 | noIdle
    36 deriving DecidableEq
    37
    38/-- An operation occupies a machine. -/
    39def Occupies {x : Inst} (σ : Sched x) (o : Op x) (i : Fin x.machines) : Prop :=
    40 i ∈ σ.machines o.1 o.2
    41
    42/-- Every operation on a machine is immediately followed by another one on
    43that machine, unless none completes later. -/
    44def Contiguous (x : Inst) (σ : Sched x) : Prop :=
    45 ∀ i (a : Op x), Occupies σ a i →
    46 (∃ b : Op x, b ≠ a ∧ Occupies σ b i ∧ σ.start b.1 b.2 = finish x σ a) ∨
    47 ∀ b : Op x, Occupies σ b i → finish x σ b ≤ finish x σ a
    48
    49/-- The no-idle field. -/
    50def noIdle : Module kernel where
    51 Value := NoIdle
    52 Data _ _ := Unit
    53 admits _ _ _ := True
    54 constraint v x _ σ := v = .noIdle → Contiguous x σ
    55 le v w := decide (v = w)
    56 embed _ _ _ := ()
    57
    58inductive BatchSetups
    59 | none
    60 | batchSetups
    61
    62/-- The data of a value: the batch of every job and the setup times between
    63batches. -/
    64def BatchSetups.Data : BatchSetups → Inst → Type
    65 | .none, _ => Unit
    66 | .batchSetups, x => (Fin x.jobs → ℕ) × (ℕ → ℕ → ℕ)
    67
    68/-- The batch of a job; a single batch when the field is absent. -/
    69def BatchSetups.batch {x : Inst} : (v : BatchSetups) → v.Data x → Fin x.jobs → ℕ
    70 | .none, _ => fun _ => 0
    71 | .batchSetups, d => d.1
    72
    73/-- The setup time between two batches. -/
    74def BatchSetups.setup {x : Inst} : (v : BatchSetups) → v.Data x → ℕ → ℕ → ℕ
    75 | .none, _ => fun _ _ => 0
    76 | .batchSetups, d => d.2
    77
    78def BatchSetups.le : BatchSetups → BatchSetups → Bool
    79 | .batchSetups, .none => false
    80 | _, _ => true
    81
    82def BatchSetups.embed : {v w : BatchSetups} → BatchSetups.le v w = true → (x : Inst) →
    83 v.Data x → w.Data x
    84 | _, .none, _, _, _ => ()
    85 | v, .batchSetups, _, _, d => (v.batch d, v.setup d)
    86
    87/-- On some machine, operation `b` follows operation `a`: `b` starts after `a`
    88completes, and no other operation on that machine lies in between. -/
    89def Follows {x : Inst} (σ : Sched x) (a b : Op x) : Prop :=
    90 finish x σ a ≤ σ.start b.1 b.2 ∧ ∃ i, Occupies σ a i ∧ Occupies σ b i ∧
    91 ∀ c : Op x, c ≠ a → c ≠ b → Occupies σ c i →
    92 ¬ (finish x σ a ≤ σ.start c.1 c.2 ∧ finish x σ c ≤ σ.start b.1 b.2)
    93
    94/-- The batch-setup field. -/
    95def batchSetups : Module kernel where
    96 Value := BatchSetups
    97 Data := BatchSetups.Data
    98 admits _ _ _ := True
    99 constraint v x d σ := ∀ a b : Op x, v.batch d a.1 ≠ v.batch d b.1 →
    100 (¬ Disjoint (σ.machines a.1 a.2) (σ.machines b.1 b.2) →
    101 finish x σ a ≤ σ.start b.1 b.2 ∨ finish x σ b ≤ σ.start a.1 a.2) ∧
    102 (Follows σ a b → finish x σ a + v.setup d (v.batch d a.1) (v.batch d b.1) ≤ σ.start b.1 b.2)
    103 le := BatchSetups.le
    104 embed := BatchSetups.embed
    105
    106axiom noIdle_sound : noIdle.Sound
    107
    108axiom batchSetups_sound : batchSetups.Sound
    109
    110end Lax434175.ShopExtras
    111
    Show 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…