Deadlines

Lax434175.Deadlines · concepts/Lax434175/Deadlines.lean · lax-434175

proven

Loading review…

Natural Language Statement

Theorem

The deadline field has three values. With the value "none" an instance carries no deadlines. With the value "deadlines" it carries a deadline $\bar d_j$ for every job $j$ , which is a natural number or $\infty$ , and every job must complete by its deadline. With the value "common deadline" it carries one deadline $\bar d$ for all jobs.

An instance without deadlines is read as an instance with the common deadline $\infty$ , and a common deadline as the deadline of every job.

Theorem. Over every kernel, the deadline 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.

no assumptions

thm✓Lax434175.Deadlines

⊢Lax434175Proofs.Deadlines.sound

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.ENat.Basic
2	import Lax434175.Modules
3
4	/-!
5	---
6	title: Deadlines
7	type: theorem
8	---
9	The deadline field has three values. With the value "none" an instance
10	carries no deadlines. With the value "deadlines" it carries a deadline
11	$\bar d_j$ for every job $j$ , which is a natural number or $\infty$ , and every
12	job must complete by its deadline. With the value "common deadline" it
13	carries one deadline $\bar d$ for all jobs.
14
15	An instance without deadlines is read as an instance with the common
16	deadline $\infty$ , and a common deadline as the deadline of every job.
17
18	Theorem. Over every kernel, the deadline field is sound.
19	-/
20
21	namespace Lax434175.Deadlines
22	open Lax434175.Kernels Lax434175.Modules
23
24	inductive Value
25	\| none
26	\| common
27	\| deadlines
28
29	/-- No data without deadlines; one deadline per job with them. -/
30	def Data (K : Kernel) : Value → K.Inst → Type
31	\| .none, _ => Unit
32	\| .common, _ => ℕ∞
33	\| .deadlines, x => Fin (K.jobs x) → ℕ∞
34
35	/-- The deadline of a job; `∞` when the field is absent. -/
36	def view {K : Kernel} {x : K.Inst} : (v : Value) → Data K v x → Fin (K.jobs x) → ℕ∞
37	\| .none, _ => fun _ => ⊤
38	\| .common, d => fun _ => d
39	\| .deadlines, d => d
40
41	def le : Value → Value → Bool
42	\| .deadlines, .none \| .deadlines, .common \| .common, .none => false
43	\| _, _ => true
44
45	def embed {K : Kernel} : {v w : Value} → le v w = true → (x : K.Inst) → Data K v x → Data K w x
46	\| _, .none, _, _, _ => ()
47	\| .none, .common, _, _, _ => (⊤ : ℕ∞)
48	\| .common, .common, _, _, d => d
49	\| v, .deadlines, _, _, d => view v d
50	\| .deadlines, .common, h, _, _ => absurd h Bool.false_ne_true
51
52	/-- A time is within a deadline. -/
53	def Within (c : NNRat) : ℕ∞ → Prop
54	\| none => True
55	\| some d => c ≤ (d : NNRat)
56
57	/-- The deadline field over a kernel. -/
58	def module (K : Kernel) : Module K where
59	Value := Value
60	Data := Data K
61	admits _ _ _ := True
62	constraint v x d σ := ∀ j, Within (K.completion x σ j) (view v d j)
63	le := le
64	embed := embed
65
66	axiom sound (K : Kernel) : (module K).Sound
67
68	end Lax434175.Deadlines
69