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

Time reversal

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

    Running a schedule backwards from a horizon HH turns a piece processing an operation during [a,b][a, b] into one processing it during [H−b,H−a][H - b, H - a]. A job that completes at CjC_j then starts at H−CjH - C_j, and a precedence constraint Ci+lij≤SjC_i + l_{ij} \le S_j becomes the constraint Cj′+lij≤Si′C'_j + l_{ij} \le S'_i of the reversed relation.

    Hence the maximum lateness without release dates and the makespan with release dates are equivalent:

    • Lmax⁡≤DL_{\max} \le D for due dates djd_j exactly if the reversed problem with release dates rj′=H−(dj+D)r'_j = H - (d_j + D), H=max⁡j(dj+D)H = \max_j (d_j + D), has makespan at most HH (if some dj+Dd_j + D is negative, or there are no jobs and DD is negative, the threshold is −1-1);
    • Cmax⁡≤DC_{\max} \le D for release dates rjr_j exactly if the reversed problem without release dates and with due dates D−rjD - r_j has maximum lateness at most 00 (if DD is negative or some rjr_j exceeds DD, the answer is no, and the reduction asks whether the maximum lateness for due dates 00 is at most −1-1).

    This is shown for the problems of the family with operations that have one operation per job, no restarts, a reversible precedence class, no deadlines, and none of the communication delays, server, forbidden times, transportation delays, no-idle and batch setups, whose meaning changes under reversal. The reversed specification has the reversed precedence class, the release dates or none, and the makespan or the maximum lateness.

    A specification ss reduces to tt by reversal if it is of this kind, and either minimizes the maximum lateness without release dates and its reversal with release dates and the makespan is field by field a special case of tt, or minimizes the makespan with release dates or none and its reversal without release dates and with the maximum lateness is so. The relation is decidable.

    Theorem. A specification that reduces to another by reversal describes a problem whose decision version reduces to that of the other.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax434175.DeadlineSteps
    2import Lax434175.PrecedenceReversal
    3
    4/-!
    5---
    6title: Time reversal
    7type: theorem
    8---
    9Running a schedule backwards from a horizon HH turns a piece processing an
    10operation during [a,b][a, b] into one processing it during [H−b,H−a][H - b, H - a]. A
    11job that completes at CjC_j then starts at H−CjH - C_j, and a precedence
    12constraint Ci+lij≤SjC_i + l_{ij} \le S_j becomes the constraint
    13Cj′+lij≤Si′C'_j + l_{ij} \le S'_i of the reversed relation.
    14
    15Hence the maximum lateness without release dates and the makespan with
    16release dates are equivalent:
    17
    18- Lmax⁡≤DL_{\max} \le D for due dates djd_j exactly if the reversed problem with
    19 release dates rj′=H−(dj+D)r'_j = H - (d_j + D), H=max⁡j(dj+D)H = \max_j (d_j + D), has makespan
    20 at most HH (if some dj+Dd_j + D is negative, or there are no jobs and DD is
    21 negative, the threshold is −1-1);
    22- Cmax⁡≤DC_{\max} \le D for release dates rjr_j exactly if the reversed problem
    23 without release dates and with due dates D−rjD - r_j has maximum lateness at
    24 most 00 (if DD is negative or some rjr_j exceeds DD, the answer is no,
    25 and the reduction asks whether the maximum lateness for due dates 00 is at
    26 most −1-1).
    27
    28This is shown for the problems of the family with operations that have one
    29operation per job, no restarts, a reversible precedence class, no deadlines,
    30and none of the communication delays, server, forbidden times, transportation
    31delays, no-idle and batch setups, whose meaning changes under reversal. The
    32reversed specification has the reversed precedence class, the release dates
    33or none, and the makespan or the maximum lateness.
    34
    35A specification ss reduces to tt by reversal if it is of this kind, and
    36either minimizes the maximum lateness without release dates and its reversal
    37with release dates and the makespan is field by field a special case of tt,
    38or minimizes the makespan with release dates or none and its reversal without
    39release dates and with the maximum lateness is so. The relation is decidable.
    40
    41**Theorem.** A specification that reduces to another by reversal describes a
    42problem whose decision version reduces to that of the other.
    43-/
    44
    45namespace Lax434175.TimeReversal
    46open Lax434175.Problems Lax434175.Assembly
    47open Lax434175 Lax434175.Operations Lax434175.OperationsFamily
    48
    49def isSingle : Structure → Bool
    50 | .single => true
    51 | _ => false
    52
    53def notRestarts : Interruption.Mode → Bool
    54 | .restarts => false
    55 | _ => true
    56
    57def noDelays : CommunicationDelays.Value → Bool
    58 | .none => true
    59 | _ => false
    60
    61def noServer : Servers.Value → Bool
    62 | .none => true
    63 | _ => false
    64
    65def noForbidden : ForbiddenTimes.Value → Bool
    66 | .none => true
    67 | _ => false
    68
    69def noTransport (v : Transportation.Value) : Bool :=
    70 (match v.shape with
    71 | .none => true
    72 | _ => false) && !v.robot
    73
    74def noIdling : ShopExtras.NoIdle → Bool
    75 | .none => true
    76 | _ => false
    77
    78def noSetups : ShopExtras.BatchSetups → Bool
    79 | .none => true
    80 | _ => false
    81
    82def releaseNone : ReleaseDates.Value → Bool
    83 | .none => true
    84 | _ => false
    85
    86def releaseKnown : ReleaseDates.Value → Bool
    87 | .online => false
    88 | _ => true
    89
    90/-- The specification can be reversed. -/
    91def Reversible (s : Spec family) : Bool :=
    92 notRestarts (s.module .interruption) && isSingle (s.module .jobStructure) &&
    93 PrecedenceReversal.reversible (s.module .precedence).order && DeadlineSteps.noDeadlines (s.module .deadlines) &&
    94 noDelays (s.module .communicationDelays) && noServer (s.module .server) &&
    95 noForbidden (s.module .forbiddenTimes) && noTransport (s.module .transportation) &&
    96 noIdling (s.module .noIdle) && noSetups (s.module .batchSetups)
    97
    98/-- The reversed specification, with given release dates and objective. -/
    99def reversed (s : Spec family) (release : ReleaseDates.Value) (objective : Objectives.Value) :
    100 Spec family where
    101 module
    102 | .precedence => (⟨PrecedenceReversal.reverse (s.module .precedence).order, (s.module .precedence).lags⟩ :
    103 Precedence.Value)
    104 | .releaseDates => release
    105 | i => s.module i
    106 objective := objective
    107
    108/-- `s` reduces to `t` by reversal. -/
    109def ReducesByReversal (s t : Spec family) : Prop :=
    110 Reversible s = true ∧
    111 ((Thresholds.objectiveOf s = .lmax ∧ releaseNone (s.module .releaseDates) = true ∧
    112 (reversed s .releaseDates .makespan).le t) ∨
    113 (Thresholds.objectiveOf s = .makespan ∧ releaseKnown (s.module .releaseDates) = true ∧
    114 (reversed s .none .lmax).le t))
    115
    116instance (s t : Spec family) : Decidable (ReducesByReversal s t) := by
    117 unfold ReducesByReversal
    118 infer_instance
    119
    120axiom reducible_of_reducesByReversal {s t : Spec family} :
    121 ReducesByReversal s t → Reducible (problem family s) (problem family t)
    122
    123end Lax434175.TimeReversal
    124
    Show Proof

    Discussion

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

    Loading discussion…