Lax Lean Archive

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

Release dates

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

    Every job of every kernel has a release date rjr_j, and no job may start before its release date. The release-date field has the values

    • none: all release dates are 00;
    • release dates: arbitrary release dates;
    • online: arbitrary release dates; the value records that the jobs become known only at their release dates. This concerns the algorithms that are admitted, not the instances and schedules, which are those of the value release dates.

    The value none is a special case of the value release dates; the value online is comparable only with itself.

    The number of distinct release dates is a parameter of every kernel.

    Theorem. Over every kernel, the release-date field is sound.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Data.Fintype.Card
    2import Mathlib.Data.Finset.Image
    3import Lax434175.Modules
    4
    5/-!
    6---
    7title: Release dates
    8type: theorem
    9---
    10Every job of every kernel has a release date rjr_j, and no job may start
    11before its release date. The release-date field has the values
    12
    13- none: all release dates are 00;
    14- release dates: arbitrary release dates;
    15- online: arbitrary release dates; the value records that the jobs become
    16 known only at their release dates. This concerns the algorithms that are
    17 admitted, not the instances and schedules, which are those of the value
    18 release dates.
    19
    20The value none is a special case of the value release dates; the value
    21online is comparable only with itself.
    22
    23The number of distinct release dates is a parameter of every kernel.
    24
    25**Theorem.** Over every kernel, the release-date field is sound.
    26-/
    27
    28namespace Lax434175.ReleaseDates
    29open Lax434175.Kernels Lax434175.Modules
    30
    31inductive Value
    32 | none
    33 | releaseDates
    34 | online
    35 deriving DecidableEq
    36
    37/-- The instances of a value. -/
    38def Value.holds (K : Kernel) : Value → K.Inst → Prop
    39 | .none, x => ∀ j, K.release x j = 0
    40 | .releaseDates, _ => True
    41 | .online, _ => True
    42
    43def le : Value → Value → Bool
    44 | .none, .releaseDates => true
    45 | v, w => decide (v = w)
    46
    47/-- The release-date field over a kernel. -/
    48def module (K : Kernel) : Module K where
    49 Value := Value
    50 Data _ _ := Unit
    51 admits v x _ := v.holds K x
    52 constraint _ x _ σ := ∀ j, (K.release x j : NNRat) ≤ K.start x σ j
    53 le := le
    54 embed _ _ _ := ()
    55
    56/-- The number of distinct release dates. -/
    57def distinct (K : Kernel) : K.Inst → ℕ :=
    58 fun x => (Finset.univ.image (K.release x)).card
    59
    60axiom sound (K : Kernel) : (module K).Sound
    61
    62end Lax434175.ReleaseDates
    63
    Show Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…