Lax Lean Archive

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

Forbidden times and input encodings

Lax434175.ForbiddenTimes · concepts/Lax434175/ForbiddenTimes.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 fields that apply to every kernel.

    The forbidden-times field has the values "none" and "forbidden times". With forbidden times, an instance carries a finite list of points in time, and no job may start or complete at one of them. An instance without forbidden times is read as one with the empty list.

    The encoding field has the values "standard" and "high multiplicity". It does not restrict the instances or the schedules: the value high multiplicity records that the input lists every kind of job once, with its multiplicity in binary, which concerns the size of the input only. The standard encoding is the special case in which every multiplicity is one.

    Theorem. Over every kernel, both fields are 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

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

    1 encoding_sound proven

    2 sound proven

    Lean source view on GitHub

    1import Mathlib.Data.NNRat.Defs
    2import Lax434175.Modules
    3
    4/-!
    5---
    6title: Forbidden times and input encodings
    7type: theorem
    8---
    9Two fields that apply to every kernel.
    10
    11The forbidden-times field has the values "none" and "forbidden times". With
    12forbidden times, an instance carries a finite list of points in time, and no
    13job may start or complete at one of them. An instance without forbidden
    14times is read as one with the empty list.
    15
    16The encoding field has the values "standard" and "high multiplicity". It
    17does not restrict the instances or the schedules: the value high
    18multiplicity records that the input lists every kind of job once, with its
    19multiplicity in binary, which concerns the size of the input only. The
    20standard encoding is the special case in which every multiplicity is one.
    21
    22**Theorem.** Over every kernel, both fields are sound.
    23-/
    24
    25namespace Lax434175.ForbiddenTimes
    26open Lax434175.Kernels Lax434175.Modules
    27
    28inductive Value
    29 | none
    30 | forbidden
    31
    32/-- No data without forbidden times; a list of points in time with them. -/
    33def Data : Value → Type
    34 | .none => Unit
    35 | .forbidden => List ℕ
    36
    37/-- The forbidden times; none when the field is absent. -/
    38def view : (v : Value) → Data v → List ℕ
    39 | .none, _ => []
    40 | .forbidden, l => l
    41
    42def le : Value → Value → Bool
    43 | .forbidden, .none => false
    44 | _, _ => true
    45
    46def embed : {v w : Value} → le v w = true → Data v → Data w
    47 | _, .none, _, _ => ()
    48 | v, .forbidden, _, d => view v d
    49
    50/-- The forbidden-times field over a kernel. -/
    51def module (K : Kernel) : Module K where
    52 Value := Value
    53 Data v _ := Data v
    54 admits _ _ _ := True
    55 constraint v x d σ := ∀ t ∈ view v d, ∀ j,
    56 K.start x σ j ≠ (t : NNRat) ∧ K.completion x σ j ≠ (t : NNRat)
    57 le := le
    58 embed h _ d := embed h d
    59
    60inductive Encoding
    61 | standard
    62 | highMultiplicity
    63 deriving DecidableEq
    64
    65/-- The encoding field over a kernel. -/
    66def encoding (K : Kernel) : Module K :=
    67 Module.ofRestriction Encoding (fun _ _ => True)
    68 (fun v w => decide (v = .standard ∨ v = w))
    69
    70axiom sound (K : Kernel) : (module K).Sound
    71
    72axiom encoding_sound (K : Kernel) : (encoding K).Sound
    73
    74end Lax434175.ForbiddenTimes
    75
    Show ProofShow 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…