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

Maximum lateness against deadlines

Lax434175.DeadlineSteps · concepts/Lax434175/DeadlineSteps.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 maximum lateness is at most DD exactly if some schedule meets the deadlines dˉj=dj+D\bar d_j = d_j + D; a schedule that meets them has makespan at most the largest of them. So the decision version of a problem minimizing the maximum lateness without deadlines reduces to that of the problem with the deadlines dj+Dd_j + D that minimizes the makespan, with the largest deadline as threshold. If some dj+Dd_j + D is negative, or there are no jobs and DD is negative, the threshold is −1-1.

    A specification ss of the family with operations, or of the batching family, reduces to tt through deadlines if ss minimizes the maximum lateness without deadlines and the specification obtained by giving it deadlines and the makespan as objective is field by field a special case of tt. The relation is decidable.

    Theorem. In both families, a specification that reduces to another through deadlines describes a problem whose decision version reduces to that of the other.

    Concept map
    35 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    Lean source view on GitHub

    1import Lax434175.OperationsFamily
    2import Lax434175.BatchFamily
    3
    4/-!
    5---
    6title: Maximum lateness against deadlines
    7type: theorem
    8---
    9The maximum lateness is at most DD exactly if some schedule meets the
    10deadlines dˉj=dj+D\bar d_j = d_j + D; a schedule that meets them has makespan at
    11most the largest of them. So the decision version of a problem minimizing the
    12maximum lateness without deadlines reduces to that of the problem with the
    13deadlines dj+Dd_j + D that minimizes the makespan, with the largest deadline as
    14threshold. If some dj+Dd_j + D is negative, or there are no jobs and DD is
    15negative, the threshold is −1-1.
    16
    17A specification ss of the family with operations, or of the batching family,
    18reduces to tt through deadlines if ss minimizes the maximum lateness without
    19deadlines and the specification obtained by giving it deadlines and the
    20makespan as objective is field by field a special case of tt. The relation is
    21decidable.
    22
    23**Theorem.** In both families, a specification that reduces to another through
    24deadlines describes a problem whose decision version reduces to that of the
    25other.
    26-/
    27
    28namespace Lax434175.DeadlineSteps
    29open Lax434175.Problems Lax434175.Assembly
    30open Lax434175
    31
    32/-- The value without deadlines. -/
    33def noDeadlines : Deadlines.Value → Bool
    34 | .none => true
    35 | _ => false
    36
    37/-- The specification with deadlines and the makespan as objective. -/
    38def opsWithDeadlines (s : Spec OperationsFamily.family) : Spec OperationsFamily.family where
    39 module
    40 | .deadlines => Deadlines.Value.deadlines
    41 | i => s.module i
    42 objective := .makespan
    43
    44/-- `s` minimizes the maximum lateness without deadlines, and with deadlines and
    45the makespan it is field by field a special case of `t`. -/
    46def OpsReducesThroughDeadlines (s t : Spec OperationsFamily.family) : Prop :=
    47 Thresholds.objectiveOf s = .lmax ∧ noDeadlines (s.module .deadlines) = true ∧ (opsWithDeadlines s).le t
    48
    49instance (s t : Spec OperationsFamily.family) : Decidable (OpsReducesThroughDeadlines s t) := by
    50 unfold OpsReducesThroughDeadlines
    51 infer_instance
    52
    53/-- The batching specification with deadlines and the makespan as objective. -/
    54def batchWithDeadlines (s : Spec BatchFamily.family) : Spec BatchFamily.family where
    55 module
    56 | .field .deadlines => Deadlines.Value.deadlines
    57 | i => s.module i
    58 objective := .makespan
    59
    60def BatchReducesThroughDeadlines (s t : Spec BatchFamily.family) : Prop :=
    61 Thresholds.objectiveOf s = .lmax ∧ noDeadlines (s.module (.field .deadlines)) = true ∧
    62 (batchWithDeadlines s).le t
    63
    64instance (s t : Spec BatchFamily.family) : Decidable (BatchReducesThroughDeadlines s t) := by
    65 unfold BatchReducesThroughDeadlines
    66 infer_instance
    67
    68axiom ops_reducible {s t : Spec OperationsFamily.family} :
    69 OpsReducesThroughDeadlines s t →
    70 Reducible (problem OperationsFamily.family s) (problem OperationsFamily.family t)
    71
    72axiom batch_reducible {s t : Spec BatchFamily.family} :
    73 BatchReducesThroughDeadlines s t →
    74 Reducible (problem BatchFamily.family s) (problem BatchFamily.family t)
    75
    76end Lax434175.DeadlineSteps
    77
    Show ProofShow Proof

    Discussion

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

    Loading discussion…