Lax Lean Archive

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

Optimization problems and embeddings

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

    An optimization problem consists of a type of instances, for every instance a type of candidate solutions, a feasibility predicate, and a rational cost to be minimized.

    An embedding of a problem AA into a problem BB maps every instance xx of AA to an instance of BB and translates solutions in both directions. It is sound if both translations preserve feasibility and neither increases the cost. A sound embedding shows that AA is a special case of BB: the two instances xx and its image have the same optimal cost.

    Restricting a problem to the instances satisfying a predicate yields again a problem, and the inclusion of the restricted instances is an embedding.

    Embeddings compose: the instance maps are composed, and so are the translations of solutions.

    Theorem. The composition of two sound embeddings is sound.

    The decision version of a problem asks, for an instance and a threshold, whether some feasible solution has cost at most the threshold. A reduction of the decision version of AA to that of BB maps every instance of AA and integral threshold to an instance of BB and an integral threshold with the same answer. Problem AA is reducible to BB if such a reduction exists.

    Theorem. A special case of a problem is reducible to it, and reducibility is transitive.

    Concept map
    1 concept
    100%
    Proven claimThis conceptDescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 comp_sound proven

    2 reducible_of_specialCase proven

    3 reducible_trans proven

    Lean source view on GitHub

    1import Mathlib.Algebra.Order.Field.Rat
    2
    3/-!
    4---
    5title: Optimization problems and embeddings
    6type: theorem
    7---
    8An optimization problem consists of a type of instances, for every instance a
    9type of candidate solutions, a feasibility predicate, and a rational cost to
    10be minimized.
    11
    12An embedding of a problem AA into a problem BB maps every instance xx of
    13AA to an instance of BB and translates solutions in both directions. It is
    14sound if both translations preserve feasibility and neither increases the
    15cost. A sound embedding shows that AA is a special case of BB: the two
    16instances xx and its image have the same optimal cost.
    17
    18Restricting a problem to the instances satisfying a predicate yields again a
    19problem, and the inclusion of the restricted instances is an embedding.
    20
    21Embeddings compose: the instance maps are composed, and so are the
    22translations of solutions.
    23
    24**Theorem.** The composition of two sound embeddings is sound.
    25
    26The decision version of a problem asks, for an instance and a threshold,
    27whether some feasible solution has cost at most the threshold. A reduction
    28of the decision version of AA to that of BB maps every instance of AA and
    29integral threshold to an instance of BB and an integral threshold with the
    30same answer. Problem AA is reducible to BB if such a reduction exists.
    31
    32**Theorem.** A special case of a problem is reducible to it, and
    33reducibility is transitive.
    34-/
    35
    36namespace Lax434175.Problems
    37
    38/-- A minimization problem. -/
    39structure Problem where
    40 /-- The instances. -/
    41 Inst : Type
    42 /-- The candidate solutions of an instance. -/
    43 Sched : Inst → Type
    44 /-- Which candidate solutions are feasible. -/
    45 feasible : (x : Inst) → Sched x → Prop
    46 /-- The cost of a candidate solution. -/
    47 cost : (x : Inst) → Sched x → ℚ
    48
    49/-- The data of an embedding of `A` into `B`: a map on instances and
    50translations of solutions in both directions. -/
    51structure Embedding (A B : Problem) where
    52 map : A.Inst → B.Inst
    53 forth : (x : A.Inst) → A.Sched x → B.Sched (map x)
    54 back : (x : A.Inst) → B.Sched (map x) → A.Sched x
    55
    56/-- An embedding is sound if both translations preserve feasibility and do
    57not increase the cost. -/
    58structure Embedding.Sound {A B : Problem} (e : Embedding A B) : Prop where
    59 forth_feasible : ∀ x σ, A.feasible x σ → B.feasible (e.map x) (e.forth x σ)
    60 forth_cost : ∀ x σ, A.feasible x σ → B.cost (e.map x) (e.forth x σ) ≤ A.cost x σ
    61 back_feasible : ∀ x τ, B.feasible (e.map x) τ → A.feasible x (e.back x τ)
    62 back_cost : ∀ x τ, B.feasible (e.map x) τ → A.cost x (e.back x τ) ≤ B.cost (e.map x) τ
    63
    64/-- `A` is a special case of `B`. -/
    65def SpecialCase (A B : Problem) : Prop := ∃ e : Embedding A B, e.Sound
    66
    67/-- The restriction of a problem to the instances satisfying `φ`. -/
    68def Problem.restrict (P : Problem) (φ : P.Inst → Prop) : Problem where
    69 Inst := { x : P.Inst // φ x }
    70 Sched x := P.Sched x.1
    71 feasible x σ := P.feasible x.1 σ
    72 cost x σ := P.cost x.1 σ
    73
    74/-- The inclusion of a restricted problem into the unrestricted one. -/
    75def Problem.inclusion (P : Problem) (φ : P.Inst → Prop) : Embedding (P.restrict φ) P where
    76 map x := x.1
    77 forth _ σ := σ
    78 back _ σ := σ
    79
    80/-- The composition of two embeddings. -/
    81def Embedding.comp {A B C : Problem} (e : Embedding A B) (f : Embedding B C) : Embedding A C where
    82 map x := f.map (e.map x)
    83 forth x σ := f.forth (e.map x) (e.forth x σ)
    84 back x τ := e.back x (f.back (e.map x) τ)
    85
    86axiom comp_sound {A B C : Problem} (e : Embedding A B) (f : Embedding B C) :
    87 e.Sound → f.Sound → (e.comp f).Sound
    88
    89/-- Some feasible solution of the instance has cost at most the threshold. -/
    90def Problem.Decides (P : Problem) (x : P.Inst) (D : ℚ) : Prop :=
    91 ∃ σ, P.feasible x σ ∧ P.cost x σ ≤ D
    92
    93/-- The data of a reduction between decision versions: an instance and a
    94threshold of `A` are mapped to an instance and a threshold of `B`. -/
    95structure DecisionReduction (A B : Problem) where
    96 map : A.Inst → ℤ → B.Inst
    97 threshold : A.Inst → ℤ → ℤ
    98
    99/-- A reduction is sound if it preserves the answer. -/
    100def DecisionReduction.Sound {A B : Problem} (r : DecisionReduction A B) : Prop :=
    101 ∀ x (D : ℤ), A.Decides x D ↔ B.Decides (r.map x D) (r.threshold x D)
    102
    103/-- The decision version of `A` reduces to that of `B`. -/
    104def Reducible (A B : Problem) : Prop := ∃ r : DecisionReduction A B, r.Sound
    105
    106axiom reducible_of_specialCase {A B : Problem} : SpecialCase A B → Reducible A B
    107
    108axiom reducible_trans {A B C : Problem} : Reducible A B → Reducible B C → Reducible A C
    109
    110end Lax434175.Problems
    111
    Show ProofShow ProofShow Proof
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…