Assembling problems from fields
Lax434175.Assembly · concepts/Lax434175/Assembly.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A family over a kernel is a collection of constraint modules and an objective. A specification chooses one value in every field of the family. It determines a problem: an instance is an instance of the kernel together with admissible data for every chosen module value and for the chosen objective value; a schedule is a schedule of the kernel; it is feasible if it is feasible for the kernel and satisfies every module constraint; its cost is given by the objective.
A specification is a special case of a specification if this holds field by field; for finitely many fields this is decidable. In that case the field-wise data maps combine into an embedding of the problem of into the problem of that leaves the kernel instance and the schedule unchanged.
Theorem. If every field of the family is sound, this embedding is sound.
Consequently a relation between two problems of a family never needs a proof of its own: it follows from the relations inside the fields.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.Basic |
| 2 | import Lax434175.Problems |
| 3 | import Lax434175.Modules |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Assembling problems from fields |
| 8 | type: theorem |
| 9 | --- |
| 10 | A family over a kernel is a collection of constraint modules and an |
| 11 | objective. A specification chooses one value in every field of the family. It |
| 12 | determines a problem: an instance is an instance of the kernel together with |
| 13 | admissible data for every chosen module value and for the chosen objective |
| 14 | value; a schedule is a schedule of the kernel; it is feasible if it |
| 15 | is feasible for the kernel and satisfies every module constraint; its cost is |
| 16 | given by the objective. |
| 17 | |
| 18 | A specification is a special case of a specification if this holds |
| 19 | field by field; for finitely many fields this is decidable. In that case the |
| 20 | field-wise data maps combine into an embedding of the problem of into the |
| 21 | problem of that leaves the kernel instance and the schedule unchanged. |
| 22 | |
| 23 | **Theorem.** If every field of the family is sound, this embedding is sound. |
| 24 | |
| 25 | Consequently a relation between two problems of a family never needs a proof |
| 26 | of its own: it follows from the relations inside the fields. |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax434175.Assembly |
| 30 | open Lax434175.Problems Lax434175.Kernels Lax434175.Modules |
| 31 | |
| 32 | /-- The fields from which problems over a kernel are assembled. -/ |
| 33 | structure Family (K : Kernel) where |
| 34 | /-- The names of the constraint fields. -/ |
| 35 | ModuleName : Type |
| 36 | module : ModuleName → Module K |
| 37 | objective : Objective K |
| 38 | |
| 39 | /-- A choice of one value in every field. -/ |
| 40 | structure Spec {K : Kernel} (F : Family K) where |
| 41 | module : (i : F.ModuleName) → (F.module i).Value |
| 42 | objective : F.objective.Value |
| 43 | |
| 44 | /-- An instance of the problem described by a specification. -/ |
| 45 | structure Inst {K : Kernel} (F : Family K) (s : Spec F) where |
| 46 | base : K.Inst |
| 47 | data : (i : F.ModuleName) → (F.module i).Data (s.module i) base |
| 48 | admitted : ∀ i, (F.module i).admits (s.module i) base (data i) |
| 49 | objectiveData : F.objective.Data s.objective base |
| 50 | objectiveAdmitted : F.objective.admits s.objective base objectiveData |
| 51 | |
| 52 | /-- The problem described by a specification. -/ |
| 53 | def problem {K : Kernel} (F : Family K) (s : Spec F) : Problem where |
| 54 | Inst := Inst F s |
| 55 | Sched x := K.Sched x.base |
| 56 | feasible x σ := |
| 57 | K.feasible x.base σ ∧ ∀ i, (F.module i).constraint (s.module i) x.base (x.data i) σ |
| 58 | cost x σ := F.objective.cost s.objective x.base x.objectiveData σ |
| 59 | |
| 60 | /-- Field-wise comparison of specifications. -/ |
| 61 | def Spec.le {K : Kernel} {F : Family K} (s t : Spec F) : Prop := |
| 62 | (∀ i, (F.module i).le (s.module i) (t.module i) = true) ∧ |
| 63 | F.objective.le s.objective t.objective = true |
| 64 | |
| 65 | instance {K : Kernel} {F : Family K} [Fintype F.ModuleName] (s t : Spec F) : |
| 66 | Decidable (s.le t) := by |
| 67 | unfold Spec.le |
| 68 | infer_instance |
| 69 | |
| 70 | /-- All fields of a family are sound. -/ |
| 71 | structure Family.Sound {K : Kernel} (F : Family K) : Prop where |
| 72 | module : ∀ i, (F.module i).Sound |
| 73 | objective : F.objective.Sound |
| 74 | |
| 75 | /-- The embedding induced by a field-wise comparison. The kernel instance and |
| 76 | the schedule are unchanged; the data of each field is read with the more |
| 77 | general value. -/ |
| 78 | def lift {K : Kernel} (F : Family K) (hF : F.Sound) {s t : Spec F} (h : s.le t) : |
| 79 | Embedding (problem F s) (problem F t) where |
| 80 | map x := |
| 81 | { base := x.base |
| 82 | data := fun i => (F.module i).embed (h.1 i) x.base (x.data i) |
| 83 | admitted := fun i => (hF.module i).admits _ _ (h.1 i) x.base (x.data i) (x.admitted i) |
| 84 | objectiveData := F.objective.embed h.2 x.base x.objectiveData |
| 85 | objectiveAdmitted := |
| 86 | hF.objective.admits _ _ h.2 x.base x.objectiveData x.objectiveAdmitted } |
| 87 | forth _ σ := σ |
| 88 | back _ σ := σ |
| 89 | |
| 90 | /-- The embedding induced by a field-wise comparison is sound. -/ |
| 91 | axiom lift_sound {K : Kernel} (F : Family K) (hF : F.Sound) {s t : Spec F} (h : s.le t) : |
| 92 | (lift F hF h).Sound |
| 93 | |
| 94 | end Lax434175.Assembly |
| 95 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments