diff --git a/lean/OMMXProof.lean b/lean/OMMXProof.lean index 0bb72ab6d..72cbf395a 100644 --- a/lean/OMMXProof.lean +++ b/lean/OMMXProof.lean @@ -14,8 +14,15 @@ import OMMXProof.Instance.Transform.IndicatorBigM.Formulation import OMMXProof.Instance.Transform.IndicatorBigM.Plan import OMMXProof.Instance.Transform.IndicatorBigM.Target import OMMXProof.Instance.Transform.SOS1BigM -import OMMXProof.Instance.Transform.SOS1BigM.Basic -import OMMXProof.Instance.Transform.SOS1BigM.Formulation -import OMMXProof.Instance.Transform.SOS1BigM.Plan -import OMMXProof.Instance.Transform.SOS1BigM.Target +import OMMXProof.Instance.Transform.SOS1BigM.Lowering +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Basic +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Plan +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Target +import OMMXProof.Instance.Transform.SOS1BigM.Promotion +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Basic +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Semantics +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Target +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Validation +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Witness +import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation import OMMXProof.State diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM.lean index f693150d5..1dc3d27a4 100644 --- a/lean/OMMXProof/Instance/Transform/SOS1BigM.lean +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM.lean @@ -1,35 +1,40 @@ -import OMMXProof.Instance.Transform.SOS1BigM.Basic -import OMMXProof.Instance.Transform.SOS1BigM.Formulation -import OMMXProof.Instance.Transform.SOS1BigM.Plan -import OMMXProof.Instance.Transform.SOS1BigM.Target +import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation +import OMMXProof.Instance.Transform.SOS1BigM.Lowering +import OMMXProof.Instance.Transform.SOS1BigM.Promotion /-! -# SOS1 Big-M lowering - -This module is the entrypoint for the SDK SOS1 conversion as an actual -`Instance.Transform`, including the formulation, validated plans, target -construction, encode/decode maps, and lowering correctness. - -## Terminology - -- An **SOS1 member** is a source decision-variable component named by the - selected SOS1 constraint. -- A **selector** is the binary value associated with an SOS1 member in the - at-most-one formulation. A selector value of zero forces its member to zero; - a value of one only permits the member to be nonzero. -- A **reused selector** is a binary SOS1 member used directly as its own - selector. -- A **fresh selector** is a new binary variable appended to the target instance - for a non-binary SOS1 member. -- The **canonical selector** is the deterministic selector used by `encode`: it - is zero exactly when its member is zero. -- A **link constraint** is a Big-M inequality connecting a non-binary member - `vᵢ` to its fresh selector `sᵢ`. For finite bounds `lᵢ ≤ vᵢ ≤ uᵢ`, the - generated sides are `vᵢ ≤ uᵢ sᵢ` when `0 < uᵢ` and - `lᵢ sᵢ ≤ vᵢ` when `lᵢ < 0`. -- The **cardinality constraint** is the at-most-one inequality over all reused - and fresh selectors. -- A **plan** selects the occurrence of the source SOS1 constraint to lower. A - **validated plan** additionally proves that every member has finite bounds, - so all required Big-M coefficients can be constructed. +# SOS1 Big-M transformations + +This module collects both directions of the SOS1 Big-M formulation: + +## Shared layers + +- `SOS1BigM.SelectorFormulation` defines the direction-independent selector + formulation. It owns the abstract mixed reused/fresh selector semantics, the + concrete retained-prefix/fresh-selector-suffix layout, and the canonical + Big-M link and cardinality rows. It proves both the relation to SOS1 and the + equivalence between the generated rows and the abstract semantics. + +## Transformation directions + +- `SOS1BigM.lowering` replaces one first-class SOS1 constraint with binary + selectors, Big-M links, and a selector-cardinality row. +- `SOS1BigM.promotion` recognizes that standard Big-M layout and replaces it + with one first-class SOS1 constraint while preserving existing special + constraints which do not reference the removed selectors. + +The primary source-to-target interpretations use the shared layers in opposite +orders, and the reverse feasibility arguments traverse the same bridge backwards: + +- Lowering constructs canonical selector semantics from SOS1 and realizes those + semantics as target rows. For the reverse feasibility implication, it + interprets the target rows and projects the resulting selector semantics to + SOS1. +- Promotion recognizes and interprets the source row suffix, then projects the + resulting selector semantics to the promoted SOS1 constraint. Its canonical + decoding argument proceeds from SOS1 back to the source rows. + +The promotion checker deliberately accepts a conservative sufficient +condition. Other valid formulations of SOS1 remain outside this Big-M-specific +transform family. -/ diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Formulation.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Formulation.lean deleted file mode 100644 index 8daacb3eb..000000000 --- a/lean/OMMXProof/Instance/Transform/SOS1BigM/Formulation.lean +++ /dev/null @@ -1,247 +0,0 @@ -import OMMXProof.Constraint.SOS1 -import OMMXProof.Domain -import Mathlib.Tactic - -/-! -# SOS1 Big-M selector formulation - -This module gives the intermediate semantics used to prove the SOS1 Big-M -lowering. The formulation may reuse binary SOS1 members as selectors, introduce -fresh selectors for the remaining members, and omit a link side whose bound is -zero. --/ - -namespace OMMXProof - -namespace Instance - -namespace SOS1BigM - -def GenericBinaryOn (members : Finset ι) (state : ι → Rat) : Prop := - ∀ i ∈ members, state i ∈ Domain.binary - -def genericSupport [DecidableEq ι] - (members : Finset ι) (state : ι → Rat) : Finset ι := - members.filter fun i => state i ≠ 0 - -def GenericSOS1 [Fintype ι] [DecidableEq ι] (members : ι → Rat) : Prop := - (genericSupport Finset.univ members).card ≤ 1 - -/-- The sum of binary member values equals the cardinality of their nonzero support. -/ -theorem generic_binary_sum_eq_support_card [DecidableEq ι] - (members : Finset ι) (state : ι → Rat) - (hbinary : GenericBinaryOn members state) : - ∑ i ∈ members, state i = ((genericSupport members state).card : Rat) := by - classical - induction members using Finset.induction_on with - | empty => simp [genericSupport] - | @insert index rest hnotmem ih => - have htail : GenericBinaryOn rest state := by - intro i hi - exact hbinary i (Finset.mem_insert_of_mem hi) - rcases hbinary index (Finset.mem_insert_self index rest) with hzero | hone - · have hsupport : - genericSupport (insert index rest) state = - genericSupport rest state := by - ext i - simp only [genericSupport, Finset.mem_filter, Finset.mem_insert] - constructor - · rintro ⟨hi | hi, hne⟩ - · exact False.elim (hne (hi ▸ hzero)) - · exact ⟨hi, hne⟩ - · rintro ⟨hi, hne⟩ - exact ⟨Or.inr hi, hne⟩ - rw [Finset.sum_insert hnotmem, hzero, zero_add, ih htail, hsupport] - · have hsupport : - genericSupport (insert index rest) state = - insert index (genericSupport rest state) := by - ext i - simp only [genericSupport, Finset.mem_filter, Finset.mem_insert] - constructor - · rintro ⟨hi | hi, hne⟩ - · exact Or.inl hi - · exact Or.inr ⟨hi, hne⟩ - · rintro (hi | ⟨hi, hne⟩) - · exact ⟨Or.inl hi, by subst i; simp [hone]⟩ - · exact ⟨Or.inr hi, hne⟩ - have hnotSupport : index ∉ genericSupport rest state := by - intro hmem - exact hnotmem (Finset.mem_filter.mp hmem).1 - rw [Finset.sum_insert hnotmem, hone, ih htail, hsupport, - Finset.card_insert_of_notMem hnotSupport] - push_cast - ring - -structure SelectorBounds (ι : Type*) where - lower : ι → Rat - upper : ι → Rat - -def WithinSelectorBounds (bounds : SelectorBounds ι) (members : ι → Rat) : Prop := - ∀ i, bounds.lower i ≤ members i ∧ members i ≤ bounds.upper i - -def canonicalSelector (members : ι → Rat) : ι → Rat := - fun i => if members i = 0 then 0 else 1 - -/-- Every canonical selector is binary. -/ -theorem canonicalSelector_binary (members : ι → Rat) (i : ι) : - canonicalSelector members i ∈ Domain.binary := by - by_cases hzero : members i = 0 <;> - simp [canonicalSelector, Membership.mem, Domain.Holds, hzero] - -/-- Canonical selectors have the same nonzero support as their members. -/ -theorem canonicalSelector_support [Fintype ι] [DecidableEq ι] - (members : ι → Rat) : - genericSupport Finset.univ (canonicalSelector members) = - genericSupport Finset.univ members := by - ext i - simp [genericSupport, canonicalSelector] - -def plannedSelector [DecidableEq ι] (reused : Finset ι) - (members freshSelectors : ι → Rat) : ι → Rat := - fun i => if i ∈ reused then members i else freshSelectors i - -def OptionalUpperLink (upper member selector : Rat) : Prop := - 0 < upper → member ≤ upper * selector - -def OptionalLowerLink (lower member selector : Rat) : Prop := - lower < 0 → lower * selector ≤ member - -/-- Semantic satisfaction predicate for the mixed reused/fresh selector -formulation used by SOS1 Big-M lowering. - -With valid member bounds, this formulation projects to `GenericSOS1`. -Conversely, every bounded SOS1 state whose reused members are binary satisfies -it under the canonical selector assignment. Generated linear constraints are -shown separately to be equivalent to this predicate. -/ -structure PlannedSelectorFormulationHolds [Fintype ι] [DecidableEq ι] - (reused : Finset ι) (bounds : SelectorBounds ι) - (members freshSelectors : ι → Rat) : Prop where - allSelectorsAreBinary : - GenericBinaryOn Finset.univ (plannedSelector reused members freshSelectors) - nonReusedHaveLinkedSelectors : - ∀ i, i ∉ reused → - OptionalUpperLink (bounds.upper i) (members i) (freshSelectors i) ∧ - OptionalLowerLink (bounds.lower i) (members i) (freshSelectors i) - selectorsSumLe1 : - ∑ i, plannedSelector reused members freshSelectors i ≤ 1 - -instance [Fintype ι] [DecidableEq ι] (reused : Finset ι) - (bounds : SelectorBounds ι) (members freshSelectors : ι → Rat) : - Decidable - (PlannedSelectorFormulationHolds reused bounds members freshSelectors) := by - let proposition := - GenericBinaryOn Finset.univ (plannedSelector reused members freshSelectors) ∧ - (∀ i, i ∉ reused → - OptionalUpperLink (bounds.upper i) (members i) (freshSelectors i) ∧ - OptionalLowerLink (bounds.lower i) (members i) (freshSelectors i)) ∧ - ∑ i, plannedSelector reused members freshSelectors i ≤ 1 - letI : Decidable proposition := by - dsimp only [proposition] - unfold GenericBinaryOn OptionalUpperLink OptionalLowerLink - infer_instance - exact decidable_of_iff proposition - ⟨fun h => ⟨h.1, h.2.1, h.2.2⟩, - fun h => ⟨h.allSelectorsAreBinary, h.nonReusedHaveLinkedSelectors, - h.selectorsSumLe1⟩⟩ - -/-- A linked member is zero whenever its fresh selector is zero. -/ -theorem member_eq_zero_of_fresh_selector_eq_zero [DecidableEq ι] - {bounds : SelectorBounds ι} - {members freshSelectors : ι → Rat} {i : ι} - (hbound : WithinSelectorBounds bounds members) - (hlinks : - OptionalUpperLink (bounds.upper i) (members i) (freshSelectors i) ∧ - OptionalLowerLink (bounds.lower i) (members i) (freshSelectors i)) - (hselector : freshSelectors i = 0) : - members i = 0 := by - have hupper : members i ≤ 0 := by - by_cases hemitted : 0 < bounds.upper i - · have h := hlinks.1 - simpa [hselector] using h hemitted - · exact le_trans (hbound i).2 (le_of_not_gt hemitted) - have hlower : 0 ≤ members i := by - by_cases hemitted : bounds.lower i < 0 - · have h := hlinks.2 - simpa [hselector] using h hemitted - · exact le_trans (le_of_not_gt hemitted) (hbound i).1 - exact le_antisymm hupper hlower - -/-- Projecting a valid mixed selector formulation recovers the original SOS1 condition. -/ -theorem plannedSelectorFormulation_project_sos1 - [Fintype ι] [DecidableEq ι] - (reused : Finset ι) (bounds : SelectorBounds ι) - (members freshSelectors : ι → Rat) - (hbound : WithinSelectorBounds bounds members) - (hformulation : - PlannedSelectorFormulationHolds reused bounds members freshSelectors) : - GenericSOS1 members := by - have hselectorSOS1 : GenericSOS1 (plannedSelector reused members freshSelectors) := by - unfold GenericSOS1 - have hcardRat : - ((genericSupport Finset.univ - (plannedSelector reused members freshSelectors)).card : Rat) ≤ 1 := by - rw [← generic_binary_sum_eq_support_card Finset.univ - (plannedSelector reused members freshSelectors) - hformulation.allSelectorsAreBinary] - exact hformulation.selectorsSumLe1 - exact_mod_cast hcardRat - have hsubset : - genericSupport Finset.univ members ⊆ - genericSupport Finset.univ (plannedSelector reused members freshSelectors) := by - intro i hi - simp only [genericSupport, Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢ - by_cases hreused : i ∈ reused - · simpa [plannedSelector, hreused] using hi - · simp only [plannedSelector, hreused, ↓reduceIte] - intro hselector - exact hi (member_eq_zero_of_fresh_selector_eq_zero hbound - (hformulation.nonReusedHaveLinkedSelectors i hreused) hselector) - exact le_trans (Finset.card_le_card hsubset) hselectorSOS1 - -/-- Reusing binary members agrees with the canonical selector on every member. -/ -theorem plannedSelector_canonical [Fintype ι] [DecidableEq ι] - (reused : Finset ι) (members : ι → Rat) - (hreusedBinary : GenericBinaryOn reused members) : - plannedSelector reused members (canonicalSelector members) = - canonicalSelector members := by - funext i - by_cases hreused : i ∈ reused - · rcases hreusedBinary i hreused with hzero | hone - · simp [plannedSelector, canonicalSelector, hreused, hzero] - · simp [plannedSelector, canonicalSelector, hreused, hone] - · simp [plannedSelector, hreused] - -/-- Canonical selectors realize the planned formulation of a bounded SOS1 state. -/ -theorem canonicalSelector_plannedFormulation [Fintype ι] [DecidableEq ι] - (reused : Finset ι) (bounds : SelectorBounds ι) (members : ι → Rat) - (hbound : WithinSelectorBounds bounds members) - (hreusedBinary : GenericBinaryOn reused members) - (hsos1 : GenericSOS1 members) : - PlannedSelectorFormulationHolds reused bounds members - (canonicalSelector members) := by - have hplanned := plannedSelector_canonical reused members hreusedBinary - refine { - allSelectorsAreBinary := ?_ - nonReusedHaveLinkedSelectors := ?_ - selectorsSumLe1 := ?_ - } - · rw [hplanned] - intro i _ - exact canonicalSelector_binary members i - · intro i hfresh - by_cases hmember : members i = 0 - · simp [OptionalUpperLink, OptionalLowerLink, canonicalSelector, hmember] - · have hb := hbound i - simp [OptionalUpperLink, OptionalLowerLink, canonicalSelector, hmember, - hb.1, hb.2] - · rw [hplanned] - rw [generic_binary_sum_eq_support_card Finset.univ - (canonicalSelector members) (fun i _ => canonicalSelector_binary members i)] - rw [canonicalSelector_support] - exact_mod_cast hsos1 - -end SOS1BigM - -end Instance - -end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering.lean new file mode 100644 index 000000000..a5a5c9815 --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering.lean @@ -0,0 +1,10 @@ +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Basic +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Plan +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Target + +/-! +# SOS1 Big-M lowering + +This module is the entrypoint for complete SOS1 Big-M lowering: plan validation, +target construction, encode/decode maps, and transformation correctness. +-/ diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Basic.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Basic.lean similarity index 84% rename from lean/OMMXProof/Instance/Transform/SOS1BigM/Basic.lean rename to lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Basic.lean index caa3908d4..941b1353d 100644 --- a/lean/OMMXProof/Instance/Transform/SOS1BigM/Basic.lean +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Basic.lean @@ -1,12 +1,37 @@ import OMMXProof.Instance.Transform.Basic -import OMMXProof.Instance.Transform.SOS1BigM.Target +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Target import Mathlib.Tactic /-! # SOS1 Big-M lowering implementation -This module defines the concrete `Instance.Transform` and proves its lowering -properties from a validated SOS1 Big-M plan. +This module writes the SDK SOS1 conversion as an actual `Instance.Transform`, +which consists of a target instance and encode/decode maps between the source +and target state spaces. + +## Terminology + +- An **SOS1 member** is a source decision-variable component named by the + selected SOS1 constraint. +- A **selector** is the binary value associated with an SOS1 member in the + at-most-one formulation. A selector value of zero forces its member to zero; + a value of one only permits the member to be nonzero. +- A **reused selector** is a binary SOS1 member used directly as its own + selector. +- A **fresh selector** is a new binary variable appended to the target instance + for a non-binary SOS1 member. +- The **canonical selector** is the deterministic selector used by `encode`: it + is zero exactly when its member is zero. +- A **link constraint** is a Big-M inequality connecting a non-binary member + `vᵢ` to its fresh selector `sᵢ`. For finite bounds `lᵢ ≤ vᵢ ≤ uᵢ`, the + generated sides are `vᵢ ≤ uᵢ sᵢ` when `0 < uᵢ` and + `lᵢ sᵢ ≤ vᵢ` when `lᵢ < 0`. +- The **cardinality constraint** is the at-most-one inequality over all reused + and fresh selectors. +- A **plan** selects the occurrence of the source SOS1 constraint to lower. A + **validated plan** additionally proves that every member has finite bounds, + so all required Big-M coefficients can be constructed. + -/ namespace OMMXProof @@ -128,10 +153,7 @@ theorem lowering_isRelaxation {source : Instance n} (plan : Plan source) have hselectors : plan.freshSelectorState sourceState selectors = canonicalSelector (plan.memberState sourceState) := by - funext i - by_cases hi : i ∈ plan.freshMembers - · simp [Plan.freshSelectorState, selectors, hi] - · simp [Plan.freshSelectorState, hi] + exact plan.selectorLayout.freshSelectorState_canonical sourceState rw [hselectors] exact canonicalSelector_plannedFormulation plan.reusedMembers validated.bounds (plan.memberState sourceState) diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Plan.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Plan.lean similarity index 74% rename from lean/OMMXProof/Instance/Transform/SOS1BigM/Plan.lean rename to lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Plan.lean index 1fbed7012..715343063 100644 --- a/lean/OMMXProof/Instance/Transform/SOS1BigM/Plan.lean +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Plan.lean @@ -1,5 +1,5 @@ import OMMXProof.Instance -import OMMXProof.Instance.Transform.SOS1BigM.Formulation +import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation import Mathlib.Tactic /-! @@ -24,20 +24,30 @@ namespace Plan def constraint {source : Instance n} (plan : Plan source) : SOS1Constraint n := source.sos1Constraints.get plan.constraintIndex +/-- The shared selector layout induced by the selected source constraint. + +Binary source members are reused directly; every other member receives a fresh +selector in the order determined by the resulting `Finset`. -/ +def selectorLayout {source : Instance n} (plan : Plan source) : + SelectorLayout n where + members := plan.constraint.members + freshMembers := + (Finset.univ.filter fun i => source.domains i = .binary)ᶜ + abbrev Member {source : Instance n} (plan : Plan source) := - {i // i ∈ plan.constraint.members} + plan.selectorLayout.Member def memberState {source : Instance n} (plan : Plan source) (state : State n) : plan.Member → Rat := - fun i => state i + plan.selectorLayout.memberState state def reusedMembers {source : Instance n} (plan : Plan source) : Finset plan.Member := - Finset.univ.filter fun i => source.domains i = .binary + plan.selectorLayout.reusedMembers def freshMembers {source : Instance n} (plan : Plan source) : Finset plan.Member := - plan.reusedMembersᶜ + plan.selectorLayout.freshMembers /-- Exact validation performed before rational selector bounds are extracted. -/ def Valid {source : Instance n} (plan : Plan source) : Prop := @@ -90,9 +100,14 @@ theorem reusedBinary_of_domains {source : Instance n} (plan : Plan source) {state : State n} (hdomains : ∀ i, state i ∈ source.domains i) : GenericBinaryOn plan.reusedMembers (plan.memberState state) := by intro i hi - have hdomain : source.domains i = .binary := - (Finset.mem_filter.mp hi).2 - simpa [memberState, hdomain] using hdomains i + have hdomain : source.domains i = .binary := by + have hmem := hi + change + i ∈ ((Finset.univ.filter + fun i : plan.Member => source.domains i = .binary)ᶜ)ᶜ at hmem + rw [compl_compl] at hmem + exact (Finset.mem_filter.mp hmem).2 + simpa [memberState, SelectorLayout.memberState, hdomain] using hdomains i theorem genericSOS1_memberState_iff_holds {source : Instance n} (plan : Plan source) (state : State n) : @@ -103,43 +118,41 @@ theorem genericSOS1_memberState_iff_holds {source : Instance n} constructor · intro h i hi j hj hine hjne have hij : - (⟨i, hi⟩ : plan.Member) = (⟨j, hj⟩ : plan.Member) := by + (⟨i, hi⟩ : plan.Member) = (⟨j, hj⟩ : plan.Member) := by apply h - · simpa [memberState] using hine - · simpa [memberState] using hjne + · simpa [memberState, SelectorLayout.memberState] using hine + · simpa [memberState, SelectorLayout.memberState] using hjne exact congrArg Subtype.val hij · intro h i hi j hj apply Subtype.ext apply h i.val i.property j.val j.property - · simpa [memberState] using hi - · simpa [memberState] using hj + · simpa [memberState, SelectorLayout.memberState] using hi + · simpa [memberState, SelectorLayout.memberState] using hj abbrev freshCount {source : Instance n} (plan : Plan source) : Nat := - plan.freshMembers.card + plan.selectorLayout.freshCount def freshMember {source : Instance n} (plan : Plan source) (j : Fin plan.freshCount) : plan.Member := - (plan.freshMembers.orderIsoOfFin rfl j).val + plan.selectorLayout.freshMember j def freshIndex {source : Instance n} (plan : Plan source) (i : plan.Member) (hi : i ∈ plan.freshMembers) : Fin plan.freshCount := - (plan.freshMembers.orderIsoOfFin rfl).symm ⟨i, hi⟩ + plan.selectorLayout.freshIndex i hi @[simp] theorem freshMember_freshIndex {source : Instance n} (plan : Plan source) (i : plan.Member) (hi : i ∈ plan.freshMembers) : plan.freshMember (plan.freshIndex i hi) = i := by - simp [freshMember, freshIndex] + exact plan.selectorLayout.freshMember_freshIndex i hi @[simp] theorem freshIndex_freshMember {source : Instance n} (plan : Plan source) (j : Fin plan.freshCount) : plan.freshIndex (plan.freshMember j) (by exact (plan.freshMembers.orderIsoOfFin rfl j).property) = j := by - change (plan.freshMembers.orderIsoOfFin rfl).symm - ((plan.freshMembers.orderIsoOfFin rfl) j) = j - exact (plan.freshMembers.orderIsoOfFin rfl).symm_apply_apply j + exact plan.selectorLayout.freshIndex_freshMember j end Plan diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Target.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Target.lean new file mode 100644 index 000000000..3d9fb462d --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Lowering/Target.lean @@ -0,0 +1,206 @@ +import OMMXProof.Instance.Extend +import OMMXProof.Instance.Transform.SOS1BigM.Lowering.Plan +import Mathlib.Tactic + +/-! +# Target construction for SOS1 Big-M lowering + +This module instantiates the shared canonical Big-M rows for a validated +lowering plan, builds the target `Instance`, and relates target feasibility to +the reused/fresh selector formulation. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +namespace Plan + +/-- The shared virtual selector tuple exposed through the lowering plan API. -/ +def freshSelectorState {source : Instance n} (plan : Plan source) + (members : State n) (fresh : State plan.freshCount) : + plan.Member → Rat := + plan.selectorLayout.freshSelectorState members fresh + +namespace Validated + +/-- The canonical link and cardinality rows instantiated with validated bounds. -/ +def generatedConstraints {source : Instance n} {plan : Plan source} + (validated : plan.Validated) : + List (LinearConstraint (n + plan.freshCount)) := + plan.selectorLayout.canonicalRows validated.bounds + +/-- The generated rows denote exactly the shared selector formulation whenever +the retained reused members and fresh selectors satisfy their binary domains. -/ +theorem generatedConstraints_hold_iff_plannedSelectorFormulation + {source : Instance n} {plan : Plan source} (validated : plan.Validated) + (state : State n) (selectors : State plan.freshCount) + (hsourceDomains : ∀ i, state i ∈ source.domains i) + (hselectorDomains : ∀ j, selectors j ∈ Domain.binary) : + (∀ constraint ∈ validated.generatedConstraints, + constraint.Holds (State.append state selectors)) ↔ + PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds + (plan.memberState state) + (plan.freshSelectorState state selectors) := by + exact + plan.selectorLayout.canonicalRows_hold_iff_plannedSelectorFormulation + validated.bounds state selectors + (plan.reusedBinary_of_domains hsourceDomains) hselectorDomains + +theorem freshSelectors_binary_of_plannedSelectorFormulation + {source : Instance n} {plan : Plan source} (validated : plan.Validated) + (state : State n) (selectors : State plan.freshCount) + (hformulation : + PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds + (plan.memberState state) + (plan.freshSelectorState state selectors)) : + ∀ j, selectors j ∈ Domain.binary := by + exact + plan.selectorLayout.freshSelectors_binary_of_plannedSelectorFormulation + validated.bounds state selectors hformulation + +theorem selectedHolds_of_plannedSelectorFormulation + {source : Instance n} {plan : Plan source} (validated : plan.Validated) + {state : State n} + {selectors : State plan.freshCount} + (hdomains : ∀ i, state i ∈ source.domains i) + (hformulation : + PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds + (plan.memberState state) + (plan.freshSelectorState state selectors)) : + plan.constraint.Holds state := by + apply (plan.genericSOS1_memberState_iff_holds state).mp + exact plannedSelectorFormulation_project_sos1 + plan.reusedMembers validated.bounds + (plan.memberState state) + (plan.freshSelectorState state selectors) + (validated.withinBounds_of_domains hdomains) hformulation + +end Validated + +def BaseFeasible {source : Instance n} (plan : Plan source) + (state : State n) : Prop := + (∀ i, state i ∈ source.domains i) ∧ + (∀ constraint ∈ source.constraints, constraint.Holds state) ∧ + (∀ constraint ∈ source.oneHotConstraints, constraint.Holds state) ∧ + (∀ constraint ∈ source.sos1Constraints.eraseIdx plan.constraintIndex.val, + constraint.Holds state) ∧ + ∀ constraint ∈ source.indicatorConstraints, constraint.Holds state + +theorem allSOS1_iff_erased_and_selected {source : Instance n} + (plan : Plan source) (state : State n) : + (∀ constraint ∈ source.sos1Constraints, constraint.Holds state) ↔ + (∀ constraint ∈ + source.sos1Constraints.eraseIdx plan.constraintIndex.val, + constraint.Holds state) ∧ + plan.constraint.Holds state := by + constructor + · intro hall + constructor + · intro constraint hconstraint + exact hall constraint (List.mem_of_mem_eraseIdx hconstraint) + · exact hall plan.constraint (List.get_mem _ plan.constraintIndex) + · rintro ⟨herased, hselected⟩ constraint hconstraint + have hperm := List.getElem_cons_eraseIdx_perm + (l := source.sos1Constraints) plan.constraintIndex.isLt + have hleft : + constraint ∈ + plan.constraint :: + source.sos1Constraints.eraseIdx plan.constraintIndex.val := by + exact hperm.symm.subset hconstraint + rcases List.mem_cons.mp hleft with hsame | herasedMem + · simpa [hsame] using hselected + · exact herased constraint herasedMem + +theorem source_feasible_iff_base_and_selected {source : Instance n} + (plan : Plan source) (state : State n) : + source.Feasible state ↔ + plan.BaseFeasible state ∧ plan.constraint.Holds state := by + unfold Instance.Feasible BaseFeasible + rw [plan.allSOS1_iff_erased_and_selected state] + aesop + +namespace Validated + +def target {source : Instance n} {plan : Plan source} + (validated : plan.Validated) : + Instance (n + plan.freshCount) where + domains := Domain.append source.domains (fun _ => .binary) + constraints := + (source.constraints.map fun constraint => + constraint.extend plan.freshCount) ++ validated.generatedConstraints + oneHotConstraints := + source.oneHotConstraints.map fun constraint => + constraint.castAdd plan.freshCount + sos1Constraints := + (source.sos1Constraints.eraseIdx plan.constraintIndex.val).map + fun constraint => constraint.castAdd plan.freshCount + indicatorConstraints := + source.indicatorConstraints.map fun constraint => + constraint.extend plan.freshCount + objective := source.objective.extend plan.freshCount + sense := source.sense + +theorem target_feasible_append_iff_base_and_formulation + {source : Instance n} {plan : Plan source} (validated : plan.Validated) + (state : State n) (selectors : State plan.freshCount) : + validated.target.Feasible (State.append state selectors) ↔ + plan.BaseFeasible state ∧ + PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds + (plan.memberState state) + (plan.freshSelectorState state selectors) := by + have hsourceAt (i : Fin n) : + State.append state selectors (Fin.castAdd plan.freshCount i) = state i := by + simp [State.append] + have hfreshAt (j : Fin plan.freshCount) : + State.append state selectors (Fin.natAdd n j) = selectors j := by + simp [State.append] + simp only [Instance.Feasible, target, Domain.append, + Fin.forall_fin_add, hsourceAt, hfreshAt, Fin.append_left, + Fin.append_right, List.forall_mem_append, List.forall_mem_map, + LinearConstraint.holds_extend_append, + OneHotConstraint.holds_castAdd_append, SOS1Constraint.holds_castAdd_append, + IndicatorConstraint.holds_extend_append, BaseFeasible] + constructor + · rintro ⟨⟨hdomains, hselectors⟩, + ⟨holdConstraints, hgenerated⟩, honeHot, hsos1, hindicator⟩ + have hformulation := + (validated.generatedConstraints_hold_iff_plannedSelectorFormulation + state selectors hdomains hselectors).mp hgenerated + exact ⟨⟨hdomains, holdConstraints, honeHot, hsos1, hindicator⟩, + hformulation⟩ + · rintro ⟨⟨hdomains, holdConstraints, honeHot, hsos1, hindicator⟩, + hformulation⟩ + have hselectors := + validated.freshSelectors_binary_of_plannedSelectorFormulation + state selectors hformulation + have hgenerated := + (validated.generatedConstraints_hold_iff_plannedSelectorFormulation + state selectors hdomains hselectors).mpr hformulation + exact ⟨⟨hdomains, hselectors⟩, + ⟨holdConstraints, hgenerated⟩, honeHot, hsos1, hindicator⟩ + +theorem target_feasible_iff_base_and_formulation + {source : Instance n} {plan : Plan source} (validated : plan.Validated) + (state : State (n + plan.freshCount)) : + validated.target.Feasible state ↔ + plan.BaseFeasible (State.source state) ∧ + PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds + (plan.memberState (State.source state)) + (plan.freshSelectorState (State.source state) + (State.extendedPart state)) := by + simpa only [State.append_source_extendedPart] using + validated.target_feasible_append_iff_base_and_formulation + (State.source state) (State.extendedPart state) + +end Validated + +end Plan + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion.lean new file mode 100644 index 000000000..5e9ebcb6f --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion.lean @@ -0,0 +1,13 @@ +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Basic +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Semantics +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Target +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Validation +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Witness + +/-! +# SOS1 Big-M promotion + +This module is the entrypoint for complete witnessed SOS1 Big-M promotion: witness data, +target construction, conservative validation, semantic characterizations, and the concrete +transform with its correctness theorems. +-/ diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Basic.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Basic.lean new file mode 100644 index 000000000..d6ddb1754 --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Basic.lean @@ -0,0 +1,285 @@ +import OMMXProof.Instance.Transform.Basic +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Semantics + +/-! +# SOS1 Big-M promotion implementation + +SOS1 Big-M promotion recognizes a standard Big-M selector formulation in a +flat source Instance and replaces it with one first-class SOS1 constraint. In +the initial supported layout, retained variables and regular constraints +occupy prefixes, while fresh selectors and their link/cardinality rows occupy +suffixes. Existing special constraints are preserved when they do not +reference fresh selectors. + +## Submodules + +The implementation follows a one-way dependency through these submodules: + +- `SOS1BigM.SelectorFormulation` defines the direction-independent selector + semantics, layout, canonical Big-M rows, and their exact relationship; +- `Promotion.Witness` defines the untrusted retained/fresh suffix layout; +- `Promotion.Target` projects retained data and constructs the promoted Instance; +- `Promotion.Validation` checks the supported source rows directly against the + shared canonical row specification and derives structural source equalities; +- `Promotion.Semantics` derives feasibility, canonical-selector, and objective + characterizations from validated evidence. + +This implementation module consumes those characterizations to package the transform and prove +its reduction, relaxation, round-trip, and objective-preservation properties. + +The transform itself is total for every untrusted `Witness`: + +- `encode` projects a flat source state to its retained prefix; +- `decode` appends canonical selectors to a promoted target state. + +Semantic properties are established separately from a validated +`StandardBigMForm`. Thus rejection by the conservative validator means only +that this initial implementation does not recognize the source shape. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +/-- +# SOS1 Big-M promotion + +## Promotion rule + +- Retain the decision-variable and regular-constraint prefixes selected by the witness. +- Retain existing OneHot, SOS1, and Indicator constraints which do not use fresh selectors. +- Remove the fresh-selector suffix and its exact Big-M link/cardinality rows. +- Add one first-class SOS1 constraint over the witnessed members. +- `promotion` itself is total. The reduction, relaxation, and objective-preservation + theorems require `witness.validate source` to succeed. + +## Sufficient condition and executable check + +The sufficient condition is the proposition +`witness.StandardBigMForm source`. It requires: + +- finite declared bounds for every promoted SOS1 member; +- reused selectors to be exactly the retained binary members; +- every fresh selector in the source suffix to be binary; +- a valid retained-constraint prefix whose rows do not depend on fresh selectors; +- the remaining ordered regular-constraint suffix to equal the canonical Big-M + link/cardinality rows generated from the witness and declared bounds; +- every existing OneHot and SOS1 constraint to contain only retained members; +- every existing Indicator constraint to have a retained trigger and a body independent + of fresh selectors; and +- the objective to be independent of fresh selectors. + +This proposition is decidable. `witness.validate source` is its executable checker and +returns the proposition bundled as `Witness.Validated`. The theorem +`Witness.validate_isSome_iff_standardBigMForm` states the exact checker contract: + +``` +(witness.validate source).isSome ↔ witness.StandardBigMForm source +``` + +Correspondingly, `Witness.validate_eq_none_iff_not_standardBigMForm` characterizes +rejection. The reduction, relaxation, and objective-preservation theorems consume the +returned `Witness.Validated`; rejection does not prove that promotion is semantically +incorrect outside this sufficient-condition recognizer. + +## Example + +For example, `x, z ∈ Binary, y ∈ [0, 2], x + z ≤ 1, y ≤ 2z` is promoted to +`x ∈ Binary, y ∈ [0, 2], SOS1(x, y)`. + +This uses a `Witness 2` with the following data: + +- The retained prefix has dimension `2`, with component `0` named `x` and component `1` + named `y`. +- `members = {x, y}` selects both retained components for the promoted SOS1 constraint. +- `freshMembers = {y}` declares that `y` uses a fresh selector. Consequently `x` is the + reused selector, `freshCount = 1`, and the appended source component is named `z`. +- `retainedConstraintCount = 0` declares that no regular row is retained. The entire + ordered constraint list is therefore the generated suffix `[y ≤ 2z, x + z ≤ 1]`. + +Under this witness: + +- `y ≤ 2z` is recognized as the upper link obtained from the upper bound `2` and + removed. No lower link is expected because the lower bound of `y` is zero. +- `x + z ≤ 1` is recognized as the selector-cardinality row and removed. +- `SOS1(x, y)` is added to the promoted target. +- `(x, y, z)` is the flat source state and `(x, y)` is the promoted target state. +- `encode` discards `z`: `(x, y, z) ↦ (x, y)`. +- `decode` restores the canonical selector, + `z = if y = 0 then 0 else 1`. + +When `x = y = 0`, both `z = 0` and `z = 1` are feasible in the flat source. +Encoding `(0, 0, 1)` and then decoding yields `(0, 0, 0)`, so the transform is not +`SourceRoundTrip`. Target round-trip does hold because decoding always chooses the canonical +selector and encoding immediately discards it. + +## Validation failures + +The untrusted witness always constructs a transform, but `witness.validate source` returns +`none` unless the source has the initial supported standard form. For example: + +- Replacing `x + z ≤ 1` with `x + z ≤ 2` is rejected. This row does not enforce the + at-most-one selector condition and can project to a state violating `SOS1(x, y)`. +- Replacing `y ≤ 2z` with `y ≤ 3z` is also rejected. Given `y ∈ [0, 2]`, this looser + coefficient can still describe a valid formulation, but the initial checker deliberately + requires the canonical row generated from the declared upper bound. +- Making an existing OneHot or SOS1 constraint contain `z`, or using `z` as an Indicator + trigger or in its body, is rejected because that constraint cannot be preserved after + removing `z`. +- Making the source objective depend on `z` is rejected because removing `z` would not + preserve objective values. + +Thus validation failure means that this conservative Big-M recognizer does not certify the +input, not that no mathematically correct SOS1 promotion exists. +-/ +def promotion (witness : Witness n) + (source : Instance (n + witness.freshCount)) : + Instance.Transform source where + targetDimension := n + target := witness.target source + encode := fun state => some (State.source state) + decode := fun state => + some (State.append state fun j => + canonicalSelector (witness.memberState state) (witness.freshMember j)) + +/-- A feasible promoted state has a feasible canonical flat representation. + +Target feasibility supplies the retained constraints and the promoted SOS1 +condition. Canonical selectors realize the validated link/cardinality suffix, +so appending them yields a feasible flat source state. -/ +theorem promotion_isReduction {witness : Witness n} + {source : Instance (n + witness.freshCount)} + (validated : witness.Validated source) : + (promotion witness source).IsReduction := by + intro promotedState htarget + change State n at promotedState + change (witness.target source).Feasible promotedState at htarget + let selectors : State witness.freshCount := + fun j => + canonicalSelector (witness.memberState promotedState) + (witness.freshMember j) + refine ⟨State.append promotedState selectors, rfl, ?_⟩ + apply + (Witness.Validated.source_feasible_append_iff_base_and_formulation + (witness := witness) (source := source) validated + promotedState selectors).mpr + rcases + (witness.target_feasible_iff_base_and_selected + source promotedState).mp htarget with + ⟨hbase, hselected⟩ + refine ⟨hbase, ?_⟩ + have hselectors : + witness.freshSelectorState promotedState selectors = + canonicalSelector (witness.memberState promotedState) := by + exact witness.selectorLayout.freshSelectorState_canonical promotedState + rw [hselectors] + exact + Witness.Validated.canonicalSelectorFormulation_of_selected + (witness := witness) (source := source) validated + hbase.1 hselected + +/-- Projecting a feasible flat state yields a feasible promoted SOS1 state. + +Validated source feasibility exposes the selector formulation. Projecting +that formulation proves the first-class SOS1 condition, while the prefix +retains every domain and regular-constraint fact in the promoted target. -/ +theorem promotion_isRelaxation {witness : Witness n} + {source : Instance (n + witness.freshCount)} + (validated : witness.Validated source) : + (promotion witness source).IsRelaxation := by + intro flatState hsource + refine ⟨State.source flatState, rfl, ?_⟩ + apply + (witness.target_feasible_iff_base_and_selected + source (State.source flatState)).mpr + rcases + (Witness.Validated.source_feasible_iff_base_and_formulation + (witness := witness) (source := source) validated flatState).mp + hsource with + ⟨hbase, hformulation⟩ + exact + ⟨hbase, + Witness.Validated.selectedHolds_of_plannedSelectorFormulation + (witness := witness) (source := source) validated + hbase.1 hformulation⟩ + +/-- Promotion preserves the optimization sense by construction. -/ +theorem promotion_sensePreserving (witness : Witness n) + (source : Instance (n + witness.freshCount)) : + (promotion witness source).SensePreserving := by + rfl + +/-- Projecting a feasible flat state preserves its objective value. + +The validator requires the source objective to be independent of the fresh +selector suffix. -/ +theorem promotion_sourceObjectiveValuePreserving + {witness : Witness n} + {source : Instance (n + witness.freshCount)} + (validated : witness.Validated source) : + (promotion witness source).SourceObjectiveValuePreserving := by + intro flatState _ + simp only [promotion, Option.map_some, Option.some.injEq] + simpa only [State.append_source_extendedPart] using + (Witness.Validated.sourceObjectiveValue_append_eq_target + (witness := witness) (source := source) validated + (State.source flatState) (State.extendedPart flatState)).symm + +/-- Canonically decoding a feasible promoted state preserves its objective. -/ +theorem promotion_targetObjectiveValuePreserving + {witness : Witness n} + {source : Instance (n + witness.freshCount)} + (validated : witness.Validated source) : + (promotion witness source).TargetObjectiveValuePreserving := by + intro promotedState _ + change State n at promotedState + let selectors : State witness.freshCount := + fun j => + canonicalSelector (witness.memberState promotedState) + (witness.freshMember j) + simp only [promotion, Option.map_some, Option.some.injEq] + change + source.ObjectiveValue (State.append promotedState selectors) = + (witness.target source).ObjectiveValue promotedState + exact + Witness.Validated.sourceObjectiveValue_append_eq_target + (witness := witness) (source := source) validated + promotedState selectors + +/-- Promotion preserves both optimization sense and objective value when +viewed from feasible flat source states. -/ +theorem promotion_sourceObjectivePreserving + {witness : Witness n} + {source : Instance (n + witness.freshCount)} + (validated : witness.Validated source) : + (promotion witness source).SourceObjectivePreserving := + ⟨promotion_sensePreserving witness source, + promotion_sourceObjectiveValuePreserving validated⟩ + +/-- Promotion preserves both optimization sense and objective value when +viewed from feasible promoted target states. -/ +theorem promotion_targetObjectivePreserving + {witness : Witness n} + {source : Instance (n + witness.freshCount)} + (validated : witness.Validated source) : + (promotion witness source).TargetObjectivePreserving := + ⟨promotion_sensePreserving witness source, + promotion_targetObjectiveValuePreserving validated⟩ + +/-- Decoding a promoted state and encoding it again recovers that state. + +This round trip is unconditional because `decode` only appends a suffix and +`encode` immediately projects back to the retained prefix. -/ +theorem promotion_targetRoundTrip (witness : Witness n) + (source : Instance (n + witness.freshCount)) : + (promotion witness source).TargetRoundTrip := by + intro targetState _ + simp [promotion] + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Semantics.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Semantics.lean new file mode 100644 index 000000000..e11c0b520 --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Semantics.lean @@ -0,0 +1,216 @@ +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Validation + +/-! +# Semantics of validated SOS1 Big-M promotion + +This module characterizes source feasibility, canonical selector construction, +and objective values under the sufficient conditions established by +`Witness.Validated`. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +namespace Witness + +section Source + +variable (witness : Witness n) +variable (source : Instance (n + witness.freshCount)) + +theorem withinSelectorBounds_of_domains + (hfinite : witness.FiniteMemberBounds source) + {state : State n} + (hdomains : ∀ i, state i ∈ (witness.target source).domains i) : + WithinSelectorBounds (witness.selectorBounds source) + (witness.memberState state) := by + intro i + exact + ⟨Domain.finite_lower_le (hdomains i) + (witness.selectorBounds_exact source hfinite i).1, + Domain.le_finite_upper (hdomains i) + (witness.selectorBounds_exact source hfinite i).2⟩ + +theorem reusedBinary_of_domains + (hlayout : witness.ReusedMembersMatchDomains source) + {state : State n} + (hdomains : ∀ i, state i ∈ (witness.target source).domains i) : + GenericBinaryOn witness.reusedMembers (witness.memberState state) := by + intro i hi + have hdomain : (witness.target source).domains i = .binary := + (hlayout i).mp hi + simpa [Witness.memberState, SelectorLayout.memberState, hdomain] using + hdomains i + +theorem genericSOS1_memberState_iff_holds (state : State n) : + GenericSOS1 (witness.memberState state) ↔ + witness.promotedConstraint.Holds state := by + classical + rw [GenericSOS1, Finset.card_le_one] + simp only [genericSupport, Finset.mem_filter, Finset.mem_univ, true_and] + constructor + · intro h i hi j hj hine hjne + have hij : + (⟨i, hi⟩ : witness.Member) = (⟨j, hj⟩ : witness.Member) := by + apply h + · simpa [Witness.memberState, SelectorLayout.memberState] using hine + · simpa [Witness.memberState, SelectorLayout.memberState] using hjne + exact congrArg Subtype.val hij + · intro h i hi j hj + apply Subtype.ext + apply h i.val i.property j.val j.property + · simpa [Witness.memberState, SelectorLayout.memberState] using hi + · simpa [Witness.memberState, SelectorLayout.memberState] using hj + +theorem selectedHolds_of_plannedSelectorFormulation + (hfinite : witness.FiniteMemberBounds source) + {state : State n} {selectors : State witness.freshCount} + (hdomains : ∀ i, state i ∈ (witness.target source).domains i) + (hformulation : + PlannedSelectorFormulationHolds witness.reusedMembers + (witness.selectorBounds source) + (witness.memberState state) + (witness.freshSelectorState state selectors)) : + witness.promotedConstraint.Holds state := by + apply (witness.genericSOS1_memberState_iff_holds state).mp + exact plannedSelectorFormulation_project_sos1 + witness.reusedMembers (witness.selectorBounds source) + (witness.memberState state) + (witness.freshSelectorState state selectors) + (witness.withinSelectorBounds_of_domains source hfinite hdomains) + hformulation + +theorem canonicalSelectorFormulation_of_selected + (hfinite : witness.FiniteMemberBounds source) + (hlayout : witness.ReusedMembersMatchDomains source) + {state : State n} + (hdomains : ∀ i, state i ∈ (witness.target source).domains i) + (hselected : witness.promotedConstraint.Holds state) : + PlannedSelectorFormulationHolds witness.reusedMembers + (witness.selectorBounds source) + (witness.memberState state) + (canonicalSelector (witness.memberState state)) := by + apply canonicalSelector_plannedFormulation + · exact witness.withinSelectorBounds_of_domains source hfinite hdomains + · exact witness.reusedBinary_of_domains source hlayout hdomains + · exact (witness.genericSOS1_memberState_iff_holds state).mpr hselected + +namespace Validated + +theorem source_feasible_append_iff_base_and_formulation + (validated : witness.Validated source) + (state : State n) (selectors : State witness.freshCount) : + source.Feasible (State.append state selectors) ↔ + witness.BaseFeasible source state ∧ + PlannedSelectorFormulationHolds witness.reusedMembers + (witness.selectorBounds source) + (witness.memberState state) + (witness.freshSelectorState state selectors) := by + have hretainedAt (i : Fin n) : + State.append state selectors (Fin.castAdd witness.freshCount i) = + state i := by + simp [State.append] + have hfreshAt (j : Fin witness.freshCount) : + State.append state selectors (Fin.natAdd n j) = selectors j := by + simp [State.append] + simp only [Instance.Feasible, validated.sourceDomains_eq, + validated.sourceConstraints_eq, + validated.sourceOneHotConstraints_eq, + validated.sourceSOS1Constraints_eq, + validated.sourceIndicatorConstraints_eq, + Domain.append, Fin.forall_fin_add, hretainedAt, hfreshAt, + Fin.append_left, Fin.append_right, List.forall_mem_append, + List.forall_mem_map, LinearConstraint.holds_extend_append, + OneHotConstraint.holds_castAdd_append, SOS1Constraint.holds_castAdd_append, + IndicatorConstraint.holds_extend_append, BaseFeasible] + constructor + · rintro ⟨⟨hdomains, hselectors⟩, + ⟨hretained, hgenerated⟩, honeHot, hsos1, hindicator⟩ + have hformulation := + (witness.selectorLayout.canonicalRows_hold_iff_plannedSelectorFormulation + (witness.selectorBounds source) state selectors + (witness.reusedBinary_of_domains source + validated.standardBigMForm.reusedMembersMatchDomains hdomains) + hselectors).mp hgenerated + exact + ⟨⟨hdomains, hretained, honeHot, hsos1, hindicator⟩, hformulation⟩ + · rintro + ⟨⟨hdomains, hretained, honeHot, hsos1, hindicator⟩, hformulation⟩ + have hselectors := + witness.selectorLayout.freshSelectors_binary_of_plannedSelectorFormulation + (witness.selectorBounds source) state selectors hformulation + have hgenerated := + (witness.selectorLayout.canonicalRows_hold_iff_plannedSelectorFormulation + (witness.selectorBounds source) state selectors + (witness.reusedBinary_of_domains source + validated.standardBigMForm.reusedMembersMatchDomains hdomains) + hselectors).mpr hformulation + exact + ⟨⟨hdomains, hselectors⟩, ⟨hretained, hgenerated⟩, + honeHot, hsos1, hindicator⟩ + +theorem source_feasible_iff_base_and_formulation + (validated : witness.Validated source) + (flatState : State (n + witness.freshCount)) : + source.Feasible flatState ↔ + witness.BaseFeasible source (State.source flatState) ∧ + PlannedSelectorFormulationHolds witness.reusedMembers + (witness.selectorBounds source) + (witness.memberState (State.source flatState)) + (witness.freshSelectorState (State.source flatState) + (State.extendedPart flatState)) := by + simpa only [State.append_source_extendedPart] using + source_feasible_append_iff_base_and_formulation + (witness := witness) (source := source) validated + (State.source flatState) (State.extendedPart flatState) + +theorem selectedHolds_of_plannedSelectorFormulation + (validated : witness.Validated source) + {state : State n} {selectors : State witness.freshCount} + (hdomains : ∀ i, state i ∈ (witness.target source).domains i) + (hformulation : + PlannedSelectorFormulationHolds witness.reusedMembers + (witness.selectorBounds source) + (witness.memberState state) + (witness.freshSelectorState state selectors)) : + witness.promotedConstraint.Holds state := + witness.selectedHolds_of_plannedSelectorFormulation source + validated.standardBigMForm.finiteMemberBounds hdomains hformulation + +theorem canonicalSelectorFormulation_of_selected + (validated : witness.Validated source) + {state : State n} + (hdomains : ∀ i, state i ∈ (witness.target source).domains i) + (hselected : witness.promotedConstraint.Holds state) : + PlannedSelectorFormulationHolds witness.reusedMembers + (witness.selectorBounds source) + (witness.memberState state) + (canonicalSelector (witness.memberState state)) := + witness.canonicalSelectorFormulation_of_selected source + validated.standardBigMForm.finiteMemberBounds + validated.standardBigMForm.reusedMembersMatchDomains + hdomains hselected + +theorem sourceObjectiveValue_append_eq_target + (validated : witness.Validated source) + (state : State n) (selectors : State witness.freshCount) : + source.ObjectiveValue (State.append state selectors) = + (witness.target source).ObjectiveValue state := by + rw [Instance.ObjectiveValue, Instance.ObjectiveValue, + validated.sourceObjective_eq] + exact Affine.eval_extend_append _ _ _ + +end Validated + +end Source + +end Witness + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Target.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Target.lean new file mode 100644 index 000000000..b08c32d88 --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Target.lean @@ -0,0 +1,382 @@ +import OMMXProof.Instance.Extend +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Witness +import Mathlib.Tactic + +/-! +# Promoted SOS1 target + +This module projects the retained prefix of a flat Big-M Instance to the target +Instance and characterizes target feasibility as the retained feasibility facts +together with the promoted SOS1 constraint. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +namespace Witness + +section Source + +variable (witness : Witness n) +variable (source : Instance (n + witness.freshCount)) + +/-- Restrict an affine expression to the retained left block. -/ +def prefixAffine (expr : Affine (n + witness.freshCount)) : Affine n where + coeff := fun i => expr.coeff (Fin.castAdd witness.freshCount i) + constant := expr.constant + +/-- Restrict a regular constraint to the retained left block. -/ +def prefixConstraint + (constraint : LinearConstraint (n + witness.freshCount)) : + LinearConstraint n where + expr := witness.prefixAffine constraint.expr + sense := constraint.sense + +/-- An affine expression is independent of every fresh selector component. -/ +def FreshIndependent + (expr : Affine (n + witness.freshCount)) : Prop := + ∀ j, expr.coeff (Fin.natAdd n j) = 0 + +instance (expr : Affine (n + witness.freshCount)) : + Decidable (witness.FreshIndependent expr) := by + unfold FreshIndependent + infer_instance + +@[simp] +theorem prefixAffine_extend + (expr : Affine n) : + witness.prefixAffine (expr.extend witness.freshCount) = expr := by + cases expr + simp [prefixAffine, Affine.extend] + +theorem extend_prefixAffine_of_freshIndependent + {expr : Affine (n + witness.freshCount)} + (h : witness.FreshIndependent expr) : + (witness.prefixAffine expr).extend witness.freshCount = expr := by + cases expr with + | mk coeff constant => + have hcoeff : + Fin.append + (fun i => coeff (Fin.castAdd witness.freshCount i)) + (fun _ : Fin witness.freshCount => 0) = + coeff := by + funext i + refine Fin.addCases ?_ ?_ i + · intro j + simp + · intro j + simpa [FreshIndependent] using (h j).symm + change + Affine.mk + (Fin.append + (fun i => coeff (Fin.castAdd witness.freshCount i)) + (fun _ : Fin witness.freshCount => 0)) + constant = + Affine.mk coeff constant + rw [hcoeff] + +@[simp] +theorem prefixConstraint_extend + (constraint : LinearConstraint n) : + witness.prefixConstraint (constraint.extend witness.freshCount) = + constraint := by + cases constraint + simp [prefixConstraint, LinearConstraint.extend] + +theorem extend_prefixConstraint_of_freshIndependent + {constraint : LinearConstraint (n + witness.freshCount)} + (h : witness.FreshIndependent constraint.expr) : + (witness.prefixConstraint constraint).extend witness.freshCount = + constraint := by + cases constraint with + | mk expr sense => + simp only [prefixConstraint, LinearConstraint.extend] + rw [witness.extend_prefixAffine_of_freshIndependent h] + +@[simp] +theorem eval_prefixAffine_append_of_freshIndependent + {expr : Affine (n + witness.freshCount)} + (h : witness.FreshIndependent expr) + (state : State n) (selectors : State witness.freshCount) : + expr.eval (State.append state selectors) = + (witness.prefixAffine expr).eval state := by + simp only [Affine.eval, prefixAffine, State.append, Fin.sum_univ_add, + Fin.append_left, Fin.append_right] + have hfresh : + ∑ j, expr.coeff (Fin.natAdd n j) * selectors j = 0 := by + apply Finset.sum_eq_zero + intro j _ + rw [h j, zero_mul] + rw [hfresh, add_zero] + +theorem holds_prefixConstraint_append_of_freshIndependent + {constraint : LinearConstraint (n + witness.freshCount)} + (h : witness.FreshIndependent constraint.expr) + (state : State n) (selectors : State witness.freshCount) : + constraint.Holds (State.append state selectors) ↔ + (witness.prefixConstraint constraint).Holds state := by + cases constraint with + | mk expr sense => + cases sense <;> + simp [LinearConstraint.Holds, prefixConstraint, + witness.eval_prefixAffine_append_of_freshIndependent h] + +/-- Restrict a special-constraint member set to the retained left block. -/ +def prefixMembers + (members : Finset (Fin (n + witness.freshCount))) : Finset (Fin n) := + Finset.univ.filter fun i ↦ Fin.castAdd witness.freshCount i ∈ members + +/-- A special-constraint member set does not reference fresh selectors. -/ +def MembersFreshIndependent + (members : Finset (Fin (n + witness.freshCount))) : Prop := + ∀ j, Fin.natAdd n j ∉ members + +instance (members : Finset (Fin (n + witness.freshCount))) : + Decidable (witness.MembersFreshIndependent members) := by + unfold MembersFreshIndependent + infer_instance + +@[simp] +theorem mem_prefixMembers + (members : Finset (Fin (n + witness.freshCount))) (i : Fin n) : + i ∈ witness.prefixMembers members ↔ + Fin.castAdd witness.freshCount i ∈ members := by + simp [prefixMembers] + +theorem castAdd_prefixMembers_of_freshIndependent + {members : Finset (Fin (n + witness.freshCount))} + (h : witness.MembersFreshIndependent members) : + castAddFinsetFin (witness.prefixMembers members) witness.freshCount = members := by + ext i + refine Fin.addCases ?_ ?_ i + · intro j + simp [prefixMembers] + · intro j + constructor + · intro hmember + simp only [castAddFinsetFin, Finset.mem_map] at hmember + rcases hmember with ⟨i, _, heq⟩ + have hval := congrArg Fin.val heq + simp at hval + omega + · exact fun hmember ↦ (h j hmember).elim + +/-- A OneHot constraint does not reference fresh selectors. -/ +def OneHotFreshIndependent + (constraint : OneHotConstraint (n + witness.freshCount)) : Prop := + witness.MembersFreshIndependent constraint.members + +instance (constraint : OneHotConstraint (n + witness.freshCount)) : + Decidable (witness.OneHotFreshIndependent constraint) := by + unfold OneHotFreshIndependent + infer_instance + +/-- Project a fresh-independent OneHot constraint to the retained block. -/ +def prefixOneHot? + (constraint : OneHotConstraint (n + witness.freshCount)) : + Option (OneHotConstraint n) := + if witness.OneHotFreshIndependent constraint then + some { members := witness.prefixMembers constraint.members } + else + none + +theorem prefixOneHot?_eq_some + {constraint : OneHotConstraint (n + witness.freshCount)} + (h : witness.OneHotFreshIndependent constraint) : + witness.prefixOneHot? constraint = + some { members := witness.prefixMembers constraint.members } := by + simp [prefixOneHot?, h] + +theorem castAdd_prefixOneHot_of_freshIndependent + {constraint : OneHotConstraint (n + witness.freshCount)} + (h : witness.OneHotFreshIndependent constraint) : + ({ members := witness.prefixMembers constraint.members } : OneHotConstraint n).castAdd + witness.freshCount = constraint := by + cases constraint + simp only [OneHotConstraint.castAdd, OneHotFreshIndependent] at h ⊢ + rw [witness.castAdd_prefixMembers_of_freshIndependent h] + +theorem map_castAdd_filterMap_prefixOneHot + {constraints : List (OneHotConstraint (n + witness.freshCount))} + (h : constraints.Forall witness.OneHotFreshIndependent) : + (constraints.filterMap witness.prefixOneHot?).map + (fun constraint ↦ constraint.castAdd witness.freshCount) = constraints := by + induction constraints with + | nil => rfl + | cons head tail ih => + simp only [List.forall_cons] at h + simp [witness.prefixOneHot?_eq_some h.1, + witness.castAdd_prefixOneHot_of_freshIndependent h.1, ih h.2] + +/-- An SOS1 constraint does not reference fresh selectors. -/ +def SOS1FreshIndependent + (constraint : SOS1Constraint (n + witness.freshCount)) : Prop := + witness.MembersFreshIndependent constraint.members + +instance (constraint : SOS1Constraint (n + witness.freshCount)) : + Decidable (witness.SOS1FreshIndependent constraint) := by + unfold SOS1FreshIndependent + infer_instance + +/-- Project a fresh-independent SOS1 constraint to the retained block. -/ +def prefixSOS1? + (constraint : SOS1Constraint (n + witness.freshCount)) : + Option (SOS1Constraint n) := + if witness.SOS1FreshIndependent constraint then + some { members := witness.prefixMembers constraint.members } + else + none + +theorem prefixSOS1?_eq_some + {constraint : SOS1Constraint (n + witness.freshCount)} + (h : witness.SOS1FreshIndependent constraint) : + witness.prefixSOS1? constraint = + some { members := witness.prefixMembers constraint.members } := by + simp [prefixSOS1?, h] + +theorem castAdd_prefixSOS1_of_freshIndependent + {constraint : SOS1Constraint (n + witness.freshCount)} + (h : witness.SOS1FreshIndependent constraint) : + ({ members := witness.prefixMembers constraint.members } : SOS1Constraint n).castAdd + witness.freshCount = constraint := by + cases constraint + simp only [SOS1Constraint.castAdd, SOS1FreshIndependent] at h ⊢ + rw [witness.castAdd_prefixMembers_of_freshIndependent h] + +theorem map_castAdd_filterMap_prefixSOS1 + {constraints : List (SOS1Constraint (n + witness.freshCount))} + (h : constraints.Forall witness.SOS1FreshIndependent) : + (constraints.filterMap witness.prefixSOS1?).map + (fun constraint ↦ constraint.castAdd witness.freshCount) = constraints := by + induction constraints with + | nil => rfl + | cons head tail ih => + simp only [List.forall_cons] at h + simp [witness.prefixSOS1?_eq_some h.1, + witness.castAdd_prefixSOS1_of_freshIndependent h.1, ih h.2] + +/-- An Indicator constraint has a retained trigger and a fresh-independent body. -/ +def IndicatorFreshIndependent + (constraint : IndicatorConstraint (n + witness.freshCount)) : Prop := + constraint.trigger.val < n ∧ + witness.FreshIndependent constraint.body.expr + +instance (constraint : IndicatorConstraint (n + witness.freshCount)) : + Decidable (witness.IndicatorFreshIndependent constraint) := by + unfold IndicatorFreshIndependent + infer_instance + +/-- Project a fresh-independent Indicator constraint to the retained block. -/ +def prefixIndicator? + (constraint : IndicatorConstraint (n + witness.freshCount)) : + Option (IndicatorConstraint n) := + if h : witness.IndicatorFreshIndependent constraint then + some + { trigger := ⟨constraint.trigger.val, h.1⟩ + polarity := constraint.polarity + body := witness.prefixConstraint constraint.body } + else + none + +theorem prefixIndicator?_eq_some + {constraint : IndicatorConstraint (n + witness.freshCount)} + (h : witness.IndicatorFreshIndependent constraint) : + witness.prefixIndicator? constraint = some + { trigger := ⟨constraint.trigger.val, h.1⟩ + polarity := constraint.polarity + body := witness.prefixConstraint constraint.body } := by + simp [prefixIndicator?, h] + +theorem extend_prefixIndicator_of_freshIndependent + {constraint : IndicatorConstraint (n + witness.freshCount)} + (h : witness.IndicatorFreshIndependent constraint) : + ({ trigger := ⟨constraint.trigger.val, h.1⟩ + polarity := constraint.polarity + body := witness.prefixConstraint constraint.body } : IndicatorConstraint n).extend + witness.freshCount = constraint := by + cases constraint with + | mk trigger polarity body => + simp only [IndicatorConstraint.extend] + have htrigger : + Fin.castAdd witness.freshCount ⟨trigger.val, h.1⟩ = trigger := by + apply Fin.ext + rfl + rw [htrigger] + rw [witness.extend_prefixConstraint_of_freshIndependent h.2] + +theorem map_extend_filterMap_prefixIndicator + {constraints : List (IndicatorConstraint (n + witness.freshCount))} + (h : constraints.Forall witness.IndicatorFreshIndependent) : + (constraints.filterMap witness.prefixIndicator?).map + (fun constraint ↦ constraint.extend witness.freshCount) = constraints := by + induction constraints with + | nil => rfl + | cons head tail ih => + simp only [List.forall_cons] at h + simp [witness.prefixIndicator?_eq_some h.1, + witness.extend_prefixIndicator_of_freshIndependent h.1, ih h.2] + +/-- Existing OneHot constraints projected to the retained block. -/ +def retainedOneHotConstraints : List (OneHotConstraint n) := + source.oneHotConstraints.filterMap witness.prefixOneHot? + +/-- Existing SOS1 constraints projected to the retained block. -/ +def retainedSOS1Constraints : List (SOS1Constraint n) := + source.sos1Constraints.filterMap witness.prefixSOS1? + +/-- Existing Indicator constraints projected to the retained block. -/ +def retainedIndicatorConstraints : List (IndicatorConstraint n) := + source.indicatorConstraints.filterMap witness.prefixIndicator? + +/-- The first-class SOS1 constraint created by this promotion. -/ +def promotedConstraint : SOS1Constraint n where + members := witness.members + +/-- The promoted target Instance determined unconditionally by the witness. + +Invalid witnesses still determine a target. Correctness properties are proved +only from `StandardBigMForm`. -/ +def target : Instance n where + domains := fun i => source.domains (Fin.castAdd witness.freshCount i) + constraints := + (source.constraints.take witness.retainedConstraintCount).map + witness.prefixConstraint + oneHotConstraints := witness.retainedOneHotConstraints source + sos1Constraints := + witness.retainedSOS1Constraints source ++ [witness.promotedConstraint] + indicatorConstraints := witness.retainedIndicatorConstraints source + objective := witness.prefixAffine source.objective + sense := source.sense + +/-- Feasibility facts retained by promotion before adding the new SOS1 condition. -/ +def BaseFeasible (state : State n) : Prop := + (∀ i, state i ∈ (witness.target source).domains i) ∧ + (∀ constraint ∈ (witness.target source).constraints, + constraint.Holds state) ∧ + (∀ constraint ∈ witness.retainedOneHotConstraints source, + constraint.Holds state) ∧ + (∀ constraint ∈ witness.retainedSOS1Constraints source, + constraint.Holds state) ∧ + ∀ constraint ∈ witness.retainedIndicatorConstraints source, + constraint.Holds state + +theorem target_feasible_iff_base_and_selected (state : State n) : + (witness.target source).Feasible state ↔ + witness.BaseFeasible source state ∧ + witness.promotedConstraint.Holds state := by + simp only [Instance.Feasible, target, BaseFeasible, + List.forall_mem_append, List.forall_mem_singleton] + aesop + +end Source + +end Witness + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Validation.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Validation.lean new file mode 100644 index 000000000..577d476c0 --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Validation.lean @@ -0,0 +1,361 @@ +import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation +import OMMXProof.Instance.Transform.SOS1BigM.Promotion.Target +import Mathlib.Tactic + +/-! +# Sufficient validation for SOS1 Big-M promotion + +This module defines the conservative, decidable sufficient conditions accepted +by SOS1 Big-M promotion and derives the structural equalities available from a +validated witness. The initial accepted shape is deliberately conservative: + +- retained variables and regular constraints form left/prefix blocks, +- fresh binary selectors and selector-formulation constraints form right/suffix + blocks, +- every selected member has finite declared bounds, +- the suffix is the standard upper/lower Big-M links followed by one + cardinality constraint, +- retained affine expressions do not depend on fresh selectors, and +- every pre-existing special constraint is independent of fresh selectors and + can therefore be preserved in the promoted Instance. + +These are sufficient, not necessary, conditions. Rejection by this initial +checker does not imply that no correct promotion exists through a broader +Big-M recognizer or another SOS1 formulation. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +namespace Witness + +section Source + +variable (witness : Witness n) +variable (source : Instance (n + witness.freshCount)) + +/-! ## Source-dependent inputs to the canonical row specification -/ + +/-- Finite declared bounds for every promoted SOS1 member. -/ +def FiniteMemberBounds : Prop := + ∀ i : witness.Member, ((witness.target source).domains i).bound.IsFinite + +instance : Decidable (witness.FiniteMemberBounds source) := by + unfold FiniteMemberBounds + infer_instance + +/-- Bounds extracted from the retained member domains. + +The fallback zero keeps the expected-row specification total for untrusted +witnesses. `StandardBigMForm.finiteMemberBounds` proves that it is unreachable +for every accepted promotion. -/ +def selectorBounds : SelectorBounds witness.Member where + lower := fun i => + if h : ((witness.target source).domains i).bound.IsFinite then + ((witness.target source).domains i).bound.finiteLower h + else 0 + upper := fun i => + if h : ((witness.target source).domains i).bound.IsFinite then + ((witness.target source).domains i).bound.finiteUpper h + else 0 + +theorem selectorBounds_exact + (hfinite : witness.FiniteMemberBounds source) + (i : witness.Member) : + ((witness.target source).domains i).bound.lower = + .finite ((witness.selectorBounds source).lower i) ∧ + ((witness.target source).domains i).bound.upper = + .finite ((witness.selectorBounds source).upper i) := by + have hi := hfinite i + simp only [selectorBounds, hi, ↓reduceDIte] + exact ⟨Bound.lower_eq_finiteLower _ hi, + Bound.upper_eq_finiteUpper _ hi⟩ + +/-- The witness classifies reused members exactly as retained binary members. -/ +def ReusedMembersMatchDomains : Prop := + ∀ i : witness.Member, + i ∈ witness.reusedMembers ↔ (witness.target source).domains i = .binary + +instance : Decidable (witness.ReusedMembersMatchDomains source) := by + unfold ReusedMembersMatchDomains + infer_instance + +/-! ## Conservative validation of the flat source shape -/ + +/-- Pointwise, computable equality for regular constraint rows. + +`LinearConstraint` does not have a global `DecidableEq` instance because its +coefficient vector is a function. Promotion only needs equality over the +finite current dimension, so validation compares the sense, constant, and +every coefficient explicitly. -/ +def SameRow (lhs rhs : LinearConstraint m) : Prop := + lhs.sense = rhs.sense ∧ + lhs.expr.constant = rhs.expr.constant ∧ + ∀ i, lhs.expr.coeff i = rhs.expr.coeff i + +instance (lhs rhs : LinearConstraint m) : Decidable (SameRow lhs rhs) := by + unfold SameRow + infer_instance + +theorem sameRow_iff_eq {lhs rhs : LinearConstraint m} : + SameRow lhs rhs ↔ lhs = rhs := by + constructor + · rcases lhs with ⟨⟨lhsCoeff, lhsConstant⟩, lhsSense⟩ + rcases rhs with ⟨⟨rhsCoeff, rhsConstant⟩, rhsSense⟩ + rintro ⟨hsense, hconstant, hcoeff⟩ + simp only at hsense hconstant hcoeff + subst rhsSense + subst rhsConstant + have hcoefficients : lhsCoeff = rhsCoeff := funext hcoeff + subst rhsCoeff + rfl + · rintro rfl + exact ⟨rfl, rfl, fun _ => rfl⟩ + +/-- A computable row-by-row comparison for two ordered constraint blocks. -/ +def RowsMatch (actual expected : List (LinearConstraint m)) : Prop := + List.Forall₂ SameRow actual expected + +instance (actual expected : List (LinearConstraint m)) : + Decidable (RowsMatch actual expected) := by + unfold RowsMatch + infer_instance + +theorem rowsMatch_iff_eq {actual expected : List (LinearConstraint m)} : + RowsMatch actual expected ↔ actual = expected := by + constructor + · intro h + induction h with + | nil => rfl + | cons hrow _ ih => + rw [sameRow_iff_eq] at hrow + simp [hrow, ih] + · rintro rfl + induction actual with + | nil => exact .nil + | cons head tail ih => + exact .cons (sameRow_iff_eq.mpr rfl) ih + +/-- Initial sufficient conditions recognized by SOS1 Big-M promotion. + +The condition deliberately fixes a prefix/suffix layout. It is not intended +to characterize every flat formulation equivalent to an SOS1 constraint. +Failure therefore means "unsupported by this validator", not that the proposed +promotion is mathematically invalid. -/ +structure StandardBigMForm : Prop where + finiteMemberBounds : witness.FiniteMemberBounds source + reusedMembersMatchDomains : witness.ReusedMembersMatchDomains source + freshSelectorDomains : + ∀ j, source.domains (Fin.natAdd n j) = .binary + retainedConstraintCount_le : + witness.retainedConstraintCount ≤ source.constraints.length + retainedConstraintsFreshIndependent : + (source.constraints.take witness.retainedConstraintCount).Forall + fun constraint => witness.FreshIndependent constraint.expr + formulationSuffixMatches : + RowsMatch + (source.constraints.drop witness.retainedConstraintCount) + (witness.selectorLayout.canonicalRows (witness.selectorBounds source)) + oneHotConstraintsFreshIndependent : + source.oneHotConstraints.Forall witness.OneHotFreshIndependent + sos1ConstraintsFreshIndependent : + source.sos1Constraints.Forall witness.SOS1FreshIndependent + indicatorConstraintsFreshIndependent : + source.indicatorConstraints.Forall witness.IndicatorFreshIndependent + objectiveFreshIndependent : + witness.FreshIndependent source.objective + +private def standardBigMFormConditions : Prop := + witness.FiniteMemberBounds source ∧ + witness.ReusedMembersMatchDomains source ∧ + (∀ j, source.domains (Fin.natAdd n j) = .binary) ∧ + witness.retainedConstraintCount ≤ source.constraints.length ∧ + (source.constraints.take witness.retainedConstraintCount).Forall + (fun constraint => witness.FreshIndependent constraint.expr) ∧ + RowsMatch + (source.constraints.drop witness.retainedConstraintCount) + (witness.selectorLayout.canonicalRows (witness.selectorBounds source)) ∧ + source.oneHotConstraints.Forall witness.OneHotFreshIndependent ∧ + source.sos1Constraints.Forall witness.SOS1FreshIndependent ∧ + source.indicatorConstraints.Forall witness.IndicatorFreshIndependent ∧ + witness.FreshIndependent source.objective + +private instance : Decidable (witness.standardBigMFormConditions source) := by + unfold standardBigMFormConditions + infer_instance + +private theorem standardBigMForm_iff_conditions : + witness.StandardBigMForm source ↔ + witness.standardBigMFormConditions source := by + constructor + · intro h + exact ⟨h.finiteMemberBounds, h.reusedMembersMatchDomains, + h.freshSelectorDomains, h.retainedConstraintCount_le, + h.retainedConstraintsFreshIndependent, h.formulationSuffixMatches, + h.oneHotConstraintsFreshIndependent, h.sos1ConstraintsFreshIndependent, + h.indicatorConstraintsFreshIndependent, h.objectiveFreshIndependent⟩ + · rintro ⟨hfinite, hlayout, hfreshDomains, hcount, hretained, + hsuffix, honeHot, hsos1, hindicator, hobjective⟩ + exact + { finiteMemberBounds := hfinite + reusedMembersMatchDomains := hlayout + freshSelectorDomains := hfreshDomains + retainedConstraintCount_le := hcount + retainedConstraintsFreshIndependent := hretained + formulationSuffixMatches := hsuffix + oneHotConstraintsFreshIndependent := honeHot + sos1ConstraintsFreshIndependent := hsos1 + indicatorConstraintsFreshIndependent := hindicator + objectiveFreshIndependent := hobjective } + +instance : Decidable (witness.StandardBigMForm source) := + decidable_of_iff (witness.standardBigMFormConditions source) + (witness.standardBigMForm_iff_conditions source).symm + +/-- A witness bundled with evidence that the current flat source has the +initial supported selector-formulation shape. -/ +structure Validated : Type where + standardBigMForm : witness.StandardBigMForm source + +/-- Check the current flat Instance against the conservative supported shape. -/ +def validate : Option (witness.Validated source) := + if hvalid : witness.StandardBigMForm source then + some ⟨hvalid⟩ + else + none + +@[simp] +theorem validate_isSome_iff_standardBigMForm : + (witness.validate source).isSome ↔ + witness.StandardBigMForm source := by + simp [validate] + +@[simp] +theorem validate_eq_none_iff_not_standardBigMForm : + witness.validate source = none ↔ + ¬witness.StandardBigMForm source := by + simp [validate] + +namespace Validated + +theorem extendedPrefixConstraints_eq + (validated : witness.Validated source) : + ((source.constraints.take witness.retainedConstraintCount).map + witness.prefixConstraint).map + (fun constraint => constraint.extend witness.freshCount) = + source.constraints.take witness.retainedConstraintCount := by + rw [List.map_map] + calc + List.map + ((fun constraint => constraint.extend witness.freshCount) ∘ + witness.prefixConstraint) + (source.constraints.take witness.retainedConstraintCount) = + List.map id + (source.constraints.take witness.retainedConstraintCount) := by + rw [List.map_eq_map_iff] + intro constraint hconstraint + apply witness.extend_prefixConstraint_of_freshIndependent + exact + (List.forall_iff_forall_mem.mp + validated.standardBigMForm.retainedConstraintsFreshIndependent) + constraint hconstraint + _ = source.constraints.take witness.retainedConstraintCount := + List.map_id _ + +theorem formulationSuffix_eq + (validated : witness.Validated source) : + source.constraints.drop witness.retainedConstraintCount = + witness.selectorLayout.canonicalRows (witness.selectorBounds source) := by + exact rowsMatch_iff_eq.mp + validated.standardBigMForm.formulationSuffixMatches + +theorem sourceDomains_eq + (validated : witness.Validated source) : + source.domains = + Domain.append (witness.target source).domains (fun _ => .binary) := by + funext i + refine Fin.addCases ?_ ?_ i + · intro j + simp [target, Domain.append] + · intro j + simp [Domain.append, + validated.standardBigMForm.freshSelectorDomains j] + +theorem sourceConstraints_eq + (validated : witness.Validated source) : + source.constraints = + ((witness.target source).constraints.map + fun constraint => constraint.extend witness.freshCount) ++ + witness.selectorLayout.canonicalRows + (witness.selectorBounds source) := by + calc + source.constraints = + source.constraints.take witness.retainedConstraintCount ++ + source.constraints.drop witness.retainedConstraintCount := + (List.take_append_drop witness.retainedConstraintCount + source.constraints).symm + _ = + source.constraints.take witness.retainedConstraintCount ++ + witness.selectorLayout.canonicalRows + (witness.selectorBounds source) := by + rw [validated.formulationSuffix_eq] + _ = + ((witness.target source).constraints.map + fun constraint => constraint.extend witness.freshCount) ++ + witness.selectorLayout.canonicalRows + (witness.selectorBounds source) := by + rw [target, validated.extendedPrefixConstraints_eq] + +theorem sourceOneHotConstraints_eq + (validated : witness.Validated source) : + source.oneHotConstraints = + (witness.retainedOneHotConstraints source).map + (fun constraint ↦ constraint.castAdd witness.freshCount) := by + symm + simpa [retainedOneHotConstraints] using + witness.map_castAdd_filterMap_prefixOneHot + validated.standardBigMForm.oneHotConstraintsFreshIndependent + +theorem sourceSOS1Constraints_eq + (validated : witness.Validated source) : + source.sos1Constraints = + (witness.retainedSOS1Constraints source).map + (fun constraint ↦ constraint.castAdd witness.freshCount) := by + symm + simpa [retainedSOS1Constraints] using + witness.map_castAdd_filterMap_prefixSOS1 + validated.standardBigMForm.sos1ConstraintsFreshIndependent + +theorem sourceIndicatorConstraints_eq + (validated : witness.Validated source) : + source.indicatorConstraints = + (witness.retainedIndicatorConstraints source).map + (fun constraint ↦ constraint.extend witness.freshCount) := by + symm + simpa [retainedIndicatorConstraints] using + witness.map_extend_filterMap_prefixIndicator + validated.standardBigMForm.indicatorConstraintsFreshIndependent + +theorem sourceObjective_eq + (validated : witness.Validated source) : + source.objective = + (witness.target source).objective.extend witness.freshCount := by + symm + simpa [target] using + witness.extend_prefixAffine_of_freshIndependent + validated.standardBigMForm.objectiveFreshIndependent + +end Validated + +end Source + +end Witness + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Witness.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Witness.lean new file mode 100644 index 000000000..42e0bc04b --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/Promotion/Witness.lean @@ -0,0 +1,97 @@ +import OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation +import Mathlib.Tactic + +/-! +# Witness data for SOS1 Big-M promotion + +An `SOS1BigM.Witness n` describes one standard Big-M selector formulation whose +retained decision variables occupy the left `n` components of a flat Instance. +Fresh selectors occupy the right block, and the regular constraints retained by +the promotion precede the selector-formulation constraints. + +The witness is intentionally untrusted. It determines a promoted target and +state maps unconditionally; `StandardBigMForm` in the validation module +records a conservative sufficient condition under which those maps preserve +feasibility and objective values. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +/-- Untrusted layout data for promoting one regular selector formulation to SOS1. + +`freshMembers` records exactly those SOS1 members which the witness claims use +fresh selectors. Their order determines the order of the right selector block. +Members outside `freshMembers` are claimed to be reused selectors. + +`retainedConstraintCount` splits the regular-constraint list into a retained +prefix and a selector-formulation suffix. -/ +structure Witness (n : Nat) where + members : Finset (Fin n) + freshMembers : Finset {i // i ∈ members} + retainedConstraintCount : Nat + +namespace Witness + +/-- The direction-independent selector layout described by this witness. -/ +def selectorLayout (witness : Witness n) : SelectorLayout n where + members := witness.members + freshMembers := witness.freshMembers + +/-- An SOS1 member selected by the witness. -/ +abbrev Member (witness : Witness n) := + witness.selectorLayout.Member + +/-- Restrict a retained state to the witnessed SOS1 members. -/ +def memberState (witness : Witness n) + (state : State n) : witness.Member → Rat := + witness.selectorLayout.memberState state + +/-- Members which the witness claims are reused directly as binary selectors. -/ +def reusedMembers (witness : Witness n) : Finset witness.Member := + witness.selectorLayout.reusedMembers + +/-- Number of fresh selector variables in the flat source Instance. -/ +abbrev freshCount (witness : Witness n) : Nat := + witness.selectorLayout.freshCount + +/-- The member corresponding to one fresh selector in the right block. -/ +def freshMember (witness : Witness n) + (j : Fin witness.freshCount) : witness.Member := + witness.selectorLayout.freshMember j + +/-- The right-block selector index corresponding to one fresh member. -/ +def freshIndex (witness : Witness n) + (i : witness.Member) (hi : i ∈ witness.freshMembers) : + Fin witness.freshCount := + witness.selectorLayout.freshIndex i hi + +/-- A virtual selector tuple indexed by every witnessed SOS1 member. -/ +def freshSelectorState (witness : Witness n) + (members : State n) (fresh : State witness.freshCount) : + witness.Member → Rat := + witness.selectorLayout.freshSelectorState members fresh + +@[simp] +theorem freshMember_freshIndex (witness : Witness n) + (i : witness.Member) (hi : i ∈ witness.freshMembers) : + witness.freshMember (witness.freshIndex i hi) = i := by + exact witness.selectorLayout.freshMember_freshIndex i hi + +@[simp] +theorem freshIndex_freshMember (witness : Witness n) + (j : Fin witness.freshCount) : + witness.freshIndex (witness.freshMember j) (by + exact (witness.selectorLayout.freshMembers.orderIsoOfFin rfl j).property) = j := by + exact witness.selectorLayout.freshIndex_freshMember j + +end Witness + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/SelectorFormulation.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/SelectorFormulation.lean new file mode 100644 index 000000000..59feeeef2 --- /dev/null +++ b/lean/OMMXProof/Instance/Transform/SOS1BigM/SelectorFormulation.lean @@ -0,0 +1,642 @@ +import OMMXProof.Constraint.SOS1 +import OMMXProof.Domain +import OMMXProof.Instance.Extend +import Mathlib.Tactic + +/-! +# SOS1 Big-M selector formulation + +This module defines the complete selector formulation shared by SOS1 Big-M +lowering and promotion. It includes the member-indexed semantics, the concrete +retained-prefix/fresh-selector-suffix layout, the canonical link and cardinality +rows, and the equivalence between those rows and the semantic formulation. + +The formulation may reuse binary SOS1 members as selectors, introduce fresh +selectors for the remaining members, and omit a link side whose bound is zero. +-/ + +namespace OMMXProof + +namespace Instance + +namespace SOS1BigM + +def GenericBinaryOn (members : Finset ι) (state : ι → Rat) : Prop := + ∀ i ∈ members, state i ∈ Domain.binary + +def genericSupport [DecidableEq ι] + (members : Finset ι) (state : ι → Rat) : Finset ι := + members.filter fun i => state i ≠ 0 + +def GenericSOS1 [Fintype ι] [DecidableEq ι] (members : ι → Rat) : Prop := + (genericSupport Finset.univ members).card ≤ 1 + +/-- The sum of binary member values equals the cardinality of their nonzero support. -/ +theorem generic_binary_sum_eq_support_card [DecidableEq ι] + (members : Finset ι) (state : ι → Rat) + (hbinary : GenericBinaryOn members state) : + ∑ i ∈ members, state i = ((genericSupport members state).card : Rat) := by + classical + induction members using Finset.induction_on with + | empty => simp [genericSupport] + | @insert index rest hnotmem ih => + have htail : GenericBinaryOn rest state := by + intro i hi + exact hbinary i (Finset.mem_insert_of_mem hi) + rcases hbinary index (Finset.mem_insert_self index rest) with hzero | hone + · have hsupport : + genericSupport (insert index rest) state = + genericSupport rest state := by + ext i + simp only [genericSupport, Finset.mem_filter, Finset.mem_insert] + constructor + · rintro ⟨hi | hi, hne⟩ + · exact False.elim (hne (hi ▸ hzero)) + · exact ⟨hi, hne⟩ + · rintro ⟨hi, hne⟩ + exact ⟨Or.inr hi, hne⟩ + rw [Finset.sum_insert hnotmem, hzero, zero_add, ih htail, hsupport] + · have hsupport : + genericSupport (insert index rest) state = + insert index (genericSupport rest state) := by + ext i + simp only [genericSupport, Finset.mem_filter, Finset.mem_insert] + constructor + · rintro ⟨hi | hi, hne⟩ + · exact Or.inl hi + · exact Or.inr ⟨hi, hne⟩ + · rintro (hi | ⟨hi, hne⟩) + · exact ⟨Or.inl hi, by subst i; simp [hone]⟩ + · exact ⟨Or.inr hi, hne⟩ + have hnotSupport : index ∉ genericSupport rest state := by + intro hmem + exact hnotmem (Finset.mem_filter.mp hmem).1 + rw [Finset.sum_insert hnotmem, hone, ih htail, hsupport, + Finset.card_insert_of_notMem hnotSupport] + push_cast + ring + +structure SelectorBounds (ι : Type*) where + lower : ι → Rat + upper : ι → Rat + +def WithinSelectorBounds (bounds : SelectorBounds ι) (members : ι → Rat) : Prop := + ∀ i, bounds.lower i ≤ members i ∧ members i ≤ bounds.upper i + +def canonicalSelector (members : ι → Rat) : ι → Rat := + fun i => if members i = 0 then 0 else 1 + +/-- Every canonical selector is binary. -/ +theorem canonicalSelector_binary (members : ι → Rat) (i : ι) : + canonicalSelector members i ∈ Domain.binary := by + by_cases hzero : members i = 0 <;> + simp [canonicalSelector, Membership.mem, Domain.Holds, hzero] + +/-- Canonical selectors have the same nonzero support as their members. -/ +theorem canonicalSelector_support [Fintype ι] [DecidableEq ι] + (members : ι → Rat) : + genericSupport Finset.univ (canonicalSelector members) = + genericSupport Finset.univ members := by + ext i + simp [genericSupport, canonicalSelector] + +def plannedSelector [DecidableEq ι] (reused : Finset ι) + (members freshSelectors : ι → Rat) : ι → Rat := + fun i => if i ∈ reused then members i else freshSelectors i + +def OptionalUpperLink (upper member selector : Rat) : Prop := + 0 < upper → member ≤ upper * selector + +def OptionalLowerLink (lower member selector : Rat) : Prop := + lower < 0 → lower * selector ≤ member + +/-- Semantic satisfaction predicate for the mixed reused/fresh selector +formulation shared by SOS1 Big-M lowering and promotion. + +With valid member bounds, this formulation projects to `GenericSOS1`. +Conversely, every bounded SOS1 state whose reused members are binary satisfies +it under the canonical selector assignment. The concrete layout and canonical +linear rows defined below are equivalent to this predicate. -/ +structure PlannedSelectorFormulationHolds [Fintype ι] [DecidableEq ι] + (reused : Finset ι) (bounds : SelectorBounds ι) + (members freshSelectors : ι → Rat) : Prop where + allSelectorsAreBinary : + GenericBinaryOn Finset.univ (plannedSelector reused members freshSelectors) + nonReusedHaveLinkedSelectors : + ∀ i, i ∉ reused → + OptionalUpperLink (bounds.upper i) (members i) (freshSelectors i) ∧ + OptionalLowerLink (bounds.lower i) (members i) (freshSelectors i) + selectorsSumLe1 : + ∑ i, plannedSelector reused members freshSelectors i ≤ 1 + +instance [Fintype ι] [DecidableEq ι] (reused : Finset ι) + (bounds : SelectorBounds ι) (members freshSelectors : ι → Rat) : + Decidable + (PlannedSelectorFormulationHolds reused bounds members freshSelectors) := by + let proposition := + GenericBinaryOn Finset.univ (plannedSelector reused members freshSelectors) ∧ + (∀ i, i ∉ reused → + OptionalUpperLink (bounds.upper i) (members i) (freshSelectors i) ∧ + OptionalLowerLink (bounds.lower i) (members i) (freshSelectors i)) ∧ + ∑ i, plannedSelector reused members freshSelectors i ≤ 1 + letI : Decidable proposition := by + dsimp only [proposition] + unfold GenericBinaryOn OptionalUpperLink OptionalLowerLink + infer_instance + exact decidable_of_iff proposition + ⟨fun h => ⟨h.1, h.2.1, h.2.2⟩, + fun h => ⟨h.allSelectorsAreBinary, h.nonReusedHaveLinkedSelectors, + h.selectorsSumLe1⟩⟩ + +/-- A linked member is zero whenever its fresh selector is zero. -/ +theorem member_eq_zero_of_fresh_selector_eq_zero [DecidableEq ι] + {bounds : SelectorBounds ι} + {members freshSelectors : ι → Rat} {i : ι} + (hbound : WithinSelectorBounds bounds members) + (hlinks : + OptionalUpperLink (bounds.upper i) (members i) (freshSelectors i) ∧ + OptionalLowerLink (bounds.lower i) (members i) (freshSelectors i)) + (hselector : freshSelectors i = 0) : + members i = 0 := by + have hupper : members i ≤ 0 := by + by_cases hemitted : 0 < bounds.upper i + · have h := hlinks.1 + simpa [hselector] using h hemitted + · exact le_trans (hbound i).2 (le_of_not_gt hemitted) + have hlower : 0 ≤ members i := by + by_cases hemitted : bounds.lower i < 0 + · have h := hlinks.2 + simpa [hselector] using h hemitted + · exact le_trans (le_of_not_gt hemitted) (hbound i).1 + exact le_antisymm hupper hlower + +/-- Projecting a valid mixed selector formulation recovers the original SOS1 condition. -/ +theorem plannedSelectorFormulation_project_sos1 + [Fintype ι] [DecidableEq ι] + (reused : Finset ι) (bounds : SelectorBounds ι) + (members freshSelectors : ι → Rat) + (hbound : WithinSelectorBounds bounds members) + (hformulation : + PlannedSelectorFormulationHolds reused bounds members freshSelectors) : + GenericSOS1 members := by + have hselectorSOS1 : GenericSOS1 (plannedSelector reused members freshSelectors) := by + unfold GenericSOS1 + have hcardRat : + ((genericSupport Finset.univ + (plannedSelector reused members freshSelectors)).card : Rat) ≤ 1 := by + rw [← generic_binary_sum_eq_support_card Finset.univ + (plannedSelector reused members freshSelectors) + hformulation.allSelectorsAreBinary] + exact hformulation.selectorsSumLe1 + exact_mod_cast hcardRat + have hsubset : + genericSupport Finset.univ members ⊆ + genericSupport Finset.univ (plannedSelector reused members freshSelectors) := by + intro i hi + simp only [genericSupport, Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢ + by_cases hreused : i ∈ reused + · simpa [plannedSelector, hreused] using hi + · simp only [plannedSelector, hreused, ↓reduceIte] + intro hselector + exact hi (member_eq_zero_of_fresh_selector_eq_zero hbound + (hformulation.nonReusedHaveLinkedSelectors i hreused) hselector) + exact le_trans (Finset.card_le_card hsubset) hselectorSOS1 + +/-- Reusing binary members agrees with the canonical selector on every member. -/ +theorem plannedSelector_canonical [Fintype ι] [DecidableEq ι] + (reused : Finset ι) (members : ι → Rat) + (hreusedBinary : GenericBinaryOn reused members) : + plannedSelector reused members (canonicalSelector members) = + canonicalSelector members := by + funext i + by_cases hreused : i ∈ reused + · rcases hreusedBinary i hreused with hzero | hone + · simp [plannedSelector, canonicalSelector, hreused, hzero] + · simp [plannedSelector, canonicalSelector, hreused, hone] + · simp [plannedSelector, hreused] + +/-- Canonical selectors realize the planned formulation of a bounded SOS1 state. -/ +theorem canonicalSelector_plannedFormulation [Fintype ι] [DecidableEq ι] + (reused : Finset ι) (bounds : SelectorBounds ι) (members : ι → Rat) + (hbound : WithinSelectorBounds bounds members) + (hreusedBinary : GenericBinaryOn reused members) + (hsos1 : GenericSOS1 members) : + PlannedSelectorFormulationHolds reused bounds members + (canonicalSelector members) := by + have hplanned := plannedSelector_canonical reused members hreusedBinary + refine { + allSelectorsAreBinary := ?_ + nonReusedHaveLinkedSelectors := ?_ + selectorsSumLe1 := ?_ + } + · rw [hplanned] + intro i _ + exact canonicalSelector_binary members i + · intro i hfresh + by_cases hmember : members i = 0 + · simp [OptionalUpperLink, OptionalLowerLink, canonicalSelector, hmember] + · have hb := hbound i + simp [OptionalUpperLink, OptionalLowerLink, canonicalSelector, hmember, + hb.1, hb.2] + · rw [hplanned] + rw [generic_binary_sum_eq_support_card Finset.univ + (canonicalSelector members) (fun i _ => canonicalSelector_binary members i)] + rw [canonicalSelector_support] + exact_mod_cast hsos1 + +/-! ## Concrete selector layout and canonical rows -/ + +/-- A direction-independent layout of reused members and fresh selectors. + +`freshMembers` is ordered as a `Finset`; that order determines the right-hand +selector block. Every member outside `freshMembers` is reused as its own +selector. -/ +structure SelectorLayout (n : Nat) where + members : Finset (Fin n) + freshMembers : Finset {i // i ∈ members} + +namespace SelectorLayout + +/-- An SOS1 member in this layout. -/ +abbrev Member (layout : SelectorLayout n) := + {i // i ∈ layout.members} + +/-- Members reused directly as binary selectors. -/ +def reusedMembers (layout : SelectorLayout n) : Finset layout.Member := + layout.freshMembersᶜ + +/-- Number of fresh selector variables in the right block. -/ +abbrev freshCount (layout : SelectorLayout n) : Nat := + layout.freshMembers.card + +/-- The member corresponding to one fresh selector in the right block. -/ +def freshMember (layout : SelectorLayout n) + (j : Fin layout.freshCount) : layout.Member := + (layout.freshMembers.orderIsoOfFin rfl j).val + +/-- The right-block selector index corresponding to one fresh member. -/ +def freshIndex (layout : SelectorLayout n) + (i : layout.Member) (hi : i ∈ layout.freshMembers) : + Fin layout.freshCount := + (layout.freshMembers.orderIsoOfFin rfl).symm ⟨i, hi⟩ + +@[simp] +theorem freshMember_freshIndex (layout : SelectorLayout n) + (i : layout.Member) (hi : i ∈ layout.freshMembers) : + layout.freshMember (layout.freshIndex i hi) = i := by + simp [freshMember, freshIndex] + +@[simp] +theorem freshIndex_freshMember (layout : SelectorLayout n) + (j : Fin layout.freshCount) : + layout.freshIndex (layout.freshMember j) (by + exact (layout.freshMembers.orderIsoOfFin rfl j).property) = j := by + change (layout.freshMembers.orderIsoOfFin rfl).symm + ((layout.freshMembers.orderIsoOfFin rfl) j) = j + exact (layout.freshMembers.orderIsoOfFin rfl).symm_apply_apply j + +/-- Restrict a retained state to the SOS1 members. -/ +def memberState (layout : SelectorLayout n) + (state : State n) : layout.Member → Rat := + fun i => state i + +/-- A virtual selector tuple indexed by every SOS1 member. + +At a reused member its value is ignored by `plannedSelector`; choosing the +canonical value makes the lowering encode lemma exact. -/ +def freshSelectorState (layout : SelectorLayout n) + (members : State n) (fresh : State layout.freshCount) : + layout.Member → Rat := + fun i => + if hi : i ∈ layout.freshMembers then + fresh (layout.freshIndex i hi) + else + canonicalSelector (layout.memberState members) i + +/-- Filling the fresh block with canonical member indicators gives the +canonical selector tuple on the entire layout. -/ +theorem freshSelectorState_canonical (layout : SelectorLayout n) + (members : State n) : + layout.freshSelectorState members + (fun j => + canonicalSelector (layout.memberState members) + (layout.freshMember j)) = + canonicalSelector (layout.memberState members) := by + funext i + by_cases hi : i ∈ layout.freshMembers + · simp [freshSelectorState, hi] + · simp [freshSelectorState, hi] + +/-- Retained coordinates which are reused directly as selectors. -/ +def reusedIndices (layout : SelectorLayout n) : Finset (Fin n) := + layout.reusedMembers.map ⟨Subtype.val, Subtype.val_injective⟩ + +/-! ## Canonical link rows -/ + +def upperLink (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (j : Fin layout.freshCount) : + LinearConstraint (n + layout.freshCount) where + expr := Affine.sub + (Affine.coordinate + (Fin.castAdd layout.freshCount (layout.freshMember j).val)) + (Affine.scale (bounds.upper (layout.freshMember j)) + (Affine.coordinate (Fin.natAdd n j))) + sense := .lessEqual + +def lowerLink (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (j : Fin layout.freshCount) : + LinearConstraint (n + layout.freshCount) where + expr := Affine.sub + (Affine.scale (bounds.lower (layout.freshMember j)) + (Affine.coordinate (Fin.natAdd n j))) + (Affine.coordinate + (Fin.castAdd layout.freshCount (layout.freshMember j).val)) + sense := .lessEqual + +@[simp] +theorem upperLink_holds (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (j : Fin layout.freshCount) (state : State n) + (selectors : State layout.freshCount) : + (layout.upperLink bounds j).Holds (State.append state selectors) ↔ + state (layout.freshMember j).val ≤ + bounds.upper (layout.freshMember j) * selectors j := by + simp [upperLink, LinearConstraint.Holds, State.append] + +@[simp] +theorem lowerLink_holds (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (j : Fin layout.freshCount) (state : State n) + (selectors : State layout.freshCount) : + (layout.lowerLink bounds j).Holds (State.append state selectors) ↔ + bounds.lower (layout.freshMember j) * selectors j ≤ + state (layout.freshMember j).val := by + simp [lowerLink, LinearConstraint.Holds, State.append] + +def linksFor (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (j : Fin layout.freshCount) : + List (LinearConstraint (n + layout.freshCount)) := + (if 0 < bounds.upper (layout.freshMember j) then + [layout.upperLink bounds j] + else []) ++ + if bounds.lower (layout.freshMember j) < 0 then + [layout.lowerLink bounds j] + else [] + +def linkConstraints (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) : + List (LinearConstraint (n + layout.freshCount)) := + (List.ofFn fun j => layout.linksFor bounds j).flatten + +theorem linkConstraints_hold_iff (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (state : State n) (selectors : State layout.freshCount) : + (∀ constraint ∈ layout.linkConstraints bounds, + constraint.Holds (State.append state selectors)) ↔ + ∀ j, + OptionalUpperLink (bounds.upper (layout.freshMember j)) + (state (layout.freshMember j).val) (selectors j) ∧ + OptionalLowerLink (bounds.lower (layout.freshMember j)) + (state (layout.freshMember j).val) (selectors j) := by + simp only [linkConstraints, List.forall_mem_flatten, + List.forall_mem_ofFn_iff] + constructor + · intro h j + have hj := h j + by_cases hu : 0 < bounds.upper (layout.freshMember j) + <;> by_cases hl : bounds.lower (layout.freshMember j) < 0 + <;> simp [linksFor, hu, hl, OptionalUpperLink, OptionalLowerLink] at hj ⊢ + <;> exact hj + · intro h j + have hj := h j + by_cases hu : 0 < bounds.upper (layout.freshMember j) + <;> by_cases hl : bounds.lower (layout.freshMember j) < 0 + <;> simp [linksFor, hu, hl, OptionalUpperLink, OptionalLowerLink] at hj ⊢ + <;> exact hj + +/-! ## Canonical cardinality row -/ + +/-- Coefficients of the mixed cardinality row. Reused members remain in the +retained block, and every fresh selector contributes in the suffix block. -/ +def cardinalityExpr (layout : SelectorLayout n) : + Affine (n + layout.freshCount) where + coeff := Fin.append + (fun i => if i ∈ layout.reusedIndices then 1 else 0) + (fun _ => 1) + constant := -1 + +def cardinalityConstraint (layout : SelectorLayout n) : + LinearConstraint (n + layout.freshCount) where + expr := layout.cardinalityExpr + sense := .lessEqual + +def selectorSum (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) : Rat := + (∑ i ∈ layout.reusedIndices, state i) + ∑ j, selectors j + +def reusedContribution (layout : SelectorLayout n) + (state : State n) (i : layout.Member) : Rat := + if i ∈ layout.reusedMembers then layout.memberState state i else 0 + +def freshContribution (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) + (i : layout.Member) : Rat := + if i ∈ layout.freshMembers then + layout.freshSelectorState state selectors i + else 0 + +theorem plannedSelector_eq_contributions (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) + (i : layout.Member) : + plannedSelector layout.reusedMembers (layout.memberState state) + (layout.freshSelectorState state selectors) i = + layout.reusedContribution state i + + layout.freshContribution state selectors i := by + by_cases hr : i ∈ layout.reusedMembers + · have hf : i ∉ layout.freshMembers := by + simpa [reusedMembers] using hr + simp [plannedSelector, reusedContribution, freshContribution, hr, hf] + · have hf : i ∈ layout.freshMembers := by + simp [reusedMembers] at hr + exact hr + simp [plannedSelector, reusedContribution, freshContribution, hr, hf] + +theorem reusedSelectorSum_eq (layout : SelectorLayout n) + (state : State n) : + (∑ i ∈ layout.reusedIndices, state i) = + ∑ i : layout.Member, layout.reusedContribution state i := by + classical + calc + (∑ i ∈ layout.reusedIndices, state i) = + ∑ i ∈ layout.reusedMembers, layout.memberState state i := by + simp [reusedIndices, memberState] + _ = ∑ i : layout.Member, layout.reusedContribution state i := by + simpa [reusedContribution] using + (Finset.sum_ite_mem_eq layout.reusedMembers + (layout.memberState state)).symm + +theorem freshSelectorSum_eq (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) : + (∑ j, selectors j) = + ∑ i : layout.Member, layout.freshContribution state selectors i := by + calc + (∑ j, selectors j) = + ∑ i : {i // i ∈ layout.freshMembers}, + layout.freshSelectorState state selectors i.val := by + apply Fintype.sum_equiv + (layout.freshMembers.orderIsoOfFin rfl).toEquiv + intro j + unfold freshSelectorState + have hi : + ((layout.freshMembers.orderIsoOfFin rfl).toEquiv j).val ∈ + layout.freshMembers := + ((layout.freshMembers.orderIsoOfFin rfl).toEquiv j).property + rw [dif_pos hi] + change selectors j = + selectors ((layout.freshMembers.orderIsoOfFin rfl).symm + ((layout.freshMembers.orderIsoOfFin rfl) j)) + exact congrArg selectors + ((layout.freshMembers.orderIsoOfFin rfl).symm_apply_apply j).symm + _ = ∑ i ∈ layout.freshMembers, + layout.freshSelectorState state selectors i := by + exact Finset.sum_coe_sort layout.freshMembers + (layout.freshSelectorState state selectors) + _ = ∑ i : layout.Member, + layout.freshContribution state selectors i := by + symm + simpa [freshContribution] using + (Finset.sum_ite_mem_eq layout.freshMembers + (layout.freshSelectorState state selectors)) + +theorem selectorSum_eq_plannedSelector (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) : + layout.selectorSum state selectors = + ∑ i, plannedSelector layout.reusedMembers (layout.memberState state) + (layout.freshSelectorState state selectors) i := by + rw [selectorSum, layout.reusedSelectorSum_eq state, + layout.freshSelectorSum_eq state selectors] + rw [← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro i _ + exact (layout.plannedSelector_eq_contributions state selectors i).symm + +@[simp] +theorem cardinalityConstraint_holds (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) : + layout.cardinalityConstraint.Holds (State.append state selectors) ↔ + layout.selectorSum state selectors ≤ 1 := by + simp [cardinalityConstraint, cardinalityExpr, selectorSum, + LinearConstraint.Holds, Affine.eval, State.append, Fin.sum_univ_add] + +/-! ## Complete canonical row block -/ + +/-- Upper/lower links for every fresh selector, followed by cardinality. -/ +def canonicalRows (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) : + List (LinearConstraint (n + layout.freshCount)) := + layout.linkConstraints bounds ++ [layout.cardinalityConstraint] + +theorem plannedSelector_binary (layout : SelectorLayout n) + (state : State n) (selectors : State layout.freshCount) + (hreusedBinary : + GenericBinaryOn layout.reusedMembers (layout.memberState state)) + (hfreshBinary : ∀ j, selectors j ∈ Domain.binary) : + GenericBinaryOn Finset.univ + (plannedSelector layout.reusedMembers (layout.memberState state) + (layout.freshSelectorState state selectors)) := by + intro i _ + by_cases hr : i ∈ layout.reusedMembers + · simpa [plannedSelector, hr] using hreusedBinary i hr + · have hfresh : i ∈ layout.freshMembers := by + simp [reusedMembers] at hr + exact hr + simpa [plannedSelector, hr, freshSelectorState, hfresh] using + hfreshBinary (layout.freshIndex i hfresh) + +theorem linksForFresh_iff_linksForMembers (layout : SelectorLayout n) + (bounds : SelectorBounds layout.Member) + (state : State n) (selectors : State layout.freshCount) : + (∀ j, + OptionalUpperLink (bounds.upper (layout.freshMember j)) + (state (layout.freshMember j).val) (selectors j) ∧ + OptionalLowerLink (bounds.lower (layout.freshMember j)) + (state (layout.freshMember j).val) (selectors j)) ↔ + ∀ i, i ∉ layout.reusedMembers → + OptionalUpperLink (bounds.upper i) + (layout.memberState state i) + (layout.freshSelectorState state selectors i) ∧ + OptionalLowerLink (bounds.lower i) + (layout.memberState state i) + (layout.freshSelectorState state selectors i) := by + constructor + · intro h i hr + have hfresh : i ∈ layout.freshMembers := by + simp [reusedMembers] at hr + exact hr + have hi := h (layout.freshIndex i hfresh) + simpa [memberState, freshSelectorState, hfresh] using hi + · intro h j + have hfresh : layout.freshMember j ∈ layout.freshMembers := + (layout.freshMembers.orderIsoOfFin rfl j).property + have hr : layout.freshMember j ∉ layout.reusedMembers := by + simpa [reusedMembers] using hfresh + have hj := h (layout.freshMember j) hr + simpa [memberState, freshSelectorState, hfresh] using hj + +/-- The canonical linear rows denote exactly the abstract reused/fresh +selector formulation once reused and fresh selectors are known to be binary. -/ +theorem canonicalRows_hold_iff_plannedSelectorFormulation + (layout : SelectorLayout n) (bounds : SelectorBounds layout.Member) + (state : State n) (selectors : State layout.freshCount) + (hreusedBinary : + GenericBinaryOn layout.reusedMembers (layout.memberState state)) + (hfreshBinary : ∀ j, selectors j ∈ Domain.binary) : + (∀ constraint ∈ layout.canonicalRows bounds, + constraint.Holds (State.append state selectors)) ↔ + PlannedSelectorFormulationHolds layout.reusedMembers bounds + (layout.memberState state) + (layout.freshSelectorState state selectors) := by + rw [canonicalRows, List.forall_mem_append, + List.forall_mem_singleton, layout.linkConstraints_hold_iff, + layout.cardinalityConstraint_holds, + layout.linksForFresh_iff_linksForMembers] + constructor + · rintro ⟨hlinks, hcardinality⟩ + refine + ⟨layout.plannedSelector_binary state selectors hreusedBinary hfreshBinary, + hlinks, ?_⟩ + rw [← layout.selectorSum_eq_plannedSelector state selectors] + exact hcardinality + · intro hformulation + refine ⟨hformulation.nonReusedHaveLinkedSelectors, ?_⟩ + rw [layout.selectorSum_eq_plannedSelector state selectors] + exact hformulation.selectorsSumLe1 + +/-- The abstract formulation forces every fresh selector to be binary. -/ +theorem freshSelectors_binary_of_plannedSelectorFormulation + (layout : SelectorLayout n) (bounds : SelectorBounds layout.Member) + (state : State n) (selectors : State layout.freshCount) + (hformulation : + PlannedSelectorFormulationHolds layout.reusedMembers bounds + (layout.memberState state) + (layout.freshSelectorState state selectors)) : + ∀ j, selectors j ∈ Domain.binary := by + intro j + have hfresh : layout.freshMember j ∈ layout.freshMembers := + (layout.freshMembers.orderIsoOfFin rfl j).property + have hr : layout.freshMember j ∉ layout.reusedMembers := by + simpa [reusedMembers] using hfresh + have hbinary := + hformulation.allSelectorsAreBinary (layout.freshMember j) (by simp) + simpa [plannedSelector, hr, freshSelectorState, hfresh] using hbinary + +end SelectorLayout + +end SOS1BigM + +end Instance + +end OMMXProof diff --git a/lean/OMMXProof/Instance/Transform/SOS1BigM/Target.lean b/lean/OMMXProof/Instance/Transform/SOS1BigM/Target.lean deleted file mode 100644 index de141a726..000000000 --- a/lean/OMMXProof/Instance/Transform/SOS1BigM/Target.lean +++ /dev/null @@ -1,484 +0,0 @@ -import OMMXProof.Instance.Extend -import OMMXProof.Instance.Transform.SOS1BigM.Plan -import Mathlib.Tactic - -/-! -# Target construction for SOS1 Big-M lowering - -This module builds the generated linear constraints and target `Instance`, then -relates target feasibility to the reused/fresh selector formulation. --/ - -namespace OMMXProof - -namespace Instance - -namespace SOS1BigM - -namespace Plan - -/-- A virtual selector tuple indexed by every SOS1 member. At a reused member -its value is ignored by `plannedSelector`; choosing the canonical value makes -the encode lemma exact. -/ -def freshSelectorState {source : Instance n} (plan : Plan source) - (members : State n) (fresh : State plan.freshCount) : - plan.Member → Rat := - fun i => - if hi : i ∈ plan.freshMembers then - fresh (plan.freshIndex i hi) - else - canonicalSelector (plan.memberState members) i - -namespace Validated - -def upperLink {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (j : Fin plan.freshCount) : - LinearConstraint (n + plan.freshCount) where - expr := Affine.sub - (Affine.coordinate - (Fin.castAdd plan.freshCount (plan.freshMember j).val)) - (Affine.scale (validated.bounds.upper (plan.freshMember j)) - (Affine.coordinate (Fin.natAdd n j))) - sense := .lessEqual - -def lowerLink {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (j : Fin plan.freshCount) : - LinearConstraint (n + plan.freshCount) where - expr := Affine.sub - (Affine.scale (validated.bounds.lower (plan.freshMember j)) - (Affine.coordinate (Fin.natAdd n j))) - (Affine.coordinate - (Fin.castAdd plan.freshCount (plan.freshMember j).val)) - sense := .lessEqual - -@[simp] -theorem upperLink_holds {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (j : Fin plan.freshCount) (state : State n) - (selectors : State plan.freshCount) : - (validated.upperLink j).Holds (State.append state selectors) ↔ - state (plan.freshMember j).val ≤ - validated.bounds.upper (plan.freshMember j) * selectors j := by - simp [upperLink, LinearConstraint.Holds, State.append] - -@[simp] -theorem lowerLink_holds {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (j : Fin plan.freshCount) (state : State n) - (selectors : State plan.freshCount) : - (validated.lowerLink j).Holds (State.append state selectors) ↔ - validated.bounds.lower (plan.freshMember j) * selectors j ≤ - state (plan.freshMember j).val := by - simp [lowerLink, LinearConstraint.Holds, State.append] - -def linksFor {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (j : Fin plan.freshCount) : - List (LinearConstraint (n + plan.freshCount)) := - (if 0 < validated.bounds.upper (plan.freshMember j) then - [validated.upperLink j] - else []) ++ - if validated.bounds.lower (plan.freshMember j) < 0 then - [validated.lowerLink j] - else [] - -def linkConstraints {source : Instance n} {plan : Plan source} (validated : plan.Validated) : - List (LinearConstraint (n + plan.freshCount)) := - (List.ofFn fun j => validated.linksFor j).flatten - -theorem linkConstraints_hold_iff {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (state : State n) (selectors : State plan.freshCount) : - (∀ constraint ∈ validated.linkConstraints, - constraint.Holds (State.append state selectors)) ↔ - ∀ j, - OptionalUpperLink (validated.bounds.upper (plan.freshMember j)) - (state (plan.freshMember j).val) (selectors j) ∧ - OptionalLowerLink (validated.bounds.lower (plan.freshMember j)) - (state (plan.freshMember j).val) (selectors j) := by - simp only [linkConstraints, List.forall_mem_flatten, - List.forall_mem_ofFn_iff] - constructor - · intro h j - have hj := h j - by_cases hu : 0 < validated.bounds.upper (plan.freshMember j) - <;> by_cases hl : validated.bounds.lower (plan.freshMember j) < 0 - <;> simp [linksFor, hu, hl, OptionalUpperLink, OptionalLowerLink] at hj ⊢ - <;> exact hj - · intro h j - have hj := h j - by_cases hu : 0 < validated.bounds.upper (plan.freshMember j) - <;> by_cases hl : validated.bounds.lower (plan.freshMember j) < 0 - <;> simp [linksFor, hu, hl, OptionalUpperLink, OptionalLowerLink] at hj ⊢ - <;> exact hj - -end Validated - -/-- Coefficients of the mixed cardinality row: reused binary members stay in -the source block and every fresh selector contributes in the right block. -/ -def cardinalityExpr {source : Instance n} (plan : Plan source) : - Affine (n + plan.freshCount) where - coeff := Fin.append - (fun i => - if i ∈ plan.constraint.members ∧ source.domains i = .binary then 1 else 0) - (fun _ => 1) - constant := -1 - -def cardinalityConstraint {source : Instance n} (plan : Plan source) : - LinearConstraint (n + plan.freshCount) where - expr := plan.cardinalityExpr - sense := .lessEqual - -def selectorSum {source : Instance n} (plan : Plan source) - (state : State n) (selectors : State plan.freshCount) : Rat := - (∑ i ∈ plan.constraint.members, - if source.domains i = .binary then state i else 0) + - ∑ j, selectors j - -def reusedContribution {source : Instance n} (plan : Plan source) - (state : State n) (i : plan.Member) : Rat := - if i ∈ plan.reusedMembers then plan.memberState state i else 0 - -def freshContribution {source : Instance n} (plan : Plan source) - (state : State n) (selectors : State plan.freshCount) - (i : plan.Member) : Rat := - if i ∈ plan.freshMembers then plan.freshSelectorState state selectors i else 0 - -theorem plannedSelector_eq_contributions {source : Instance n} - (plan : Plan source) (state : State n) - (selectors : State plan.freshCount) (i : plan.Member) : - plannedSelector plan.reusedMembers (plan.memberState state) - (plan.freshSelectorState state selectors) i = - plan.reusedContribution state i + - plan.freshContribution state selectors i := by - by_cases hr : i ∈ plan.reusedMembers - · have hf : i ∉ plan.freshMembers := by - simp [freshMembers, hr] - simp [plannedSelector, reusedContribution, freshContribution, hr, hf] - · have hf : i ∈ plan.freshMembers := by - simp [freshMembers, hr] - simp [plannedSelector, reusedContribution, freshContribution, hr, hf] - -theorem sourceReusedSum_eq {source : Instance n} (plan : Plan source) - (state : State n) : - (∑ i ∈ plan.constraint.members, - if source.domains i = .binary then state i else 0) = - ∑ i : plan.Member, plan.reusedContribution state i := by - symm - calc - (∑ i : plan.Member, plan.reusedContribution state i) = - ∑ i : plan.Member, - if source.domains i = .binary then state i else 0 := by - apply Finset.sum_congr rfl - intro i _ - simp [reusedContribution, reusedMembers, memberState] - _ = ∑ i ∈ plan.constraint.members, - if source.domains i = .binary then state i else 0 := by - exact Finset.sum_coe_sort plan.constraint.members - (fun i => if source.domains i = .binary then state i else 0) - -theorem freshSelectorSum_eq {source : Instance n} (plan : Plan source) - (state : State n) (selectors : State plan.freshCount) : - (∑ j, selectors j) = - ∑ i : plan.Member, plan.freshContribution state selectors i := by - calc - (∑ j, selectors j) = - ∑ i : {i // i ∈ plan.freshMembers}, - plan.freshSelectorState state selectors i.val := by - apply Fintype.sum_equiv - (plan.freshMembers.orderIsoOfFin rfl).toEquiv - intro j - unfold freshSelectorState - have hi : - ((plan.freshMembers.orderIsoOfFin rfl).toEquiv j).val ∈ - plan.freshMembers := - ((plan.freshMembers.orderIsoOfFin rfl).toEquiv j).property - rw [dif_pos hi] - change selectors j = - selectors ((plan.freshMembers.orderIsoOfFin rfl).symm - ((plan.freshMembers.orderIsoOfFin rfl) j)) - exact congrArg selectors - ((plan.freshMembers.orderIsoOfFin rfl).symm_apply_apply j).symm - _ = ∑ i ∈ plan.freshMembers, - plan.freshSelectorState state selectors i := by - exact Finset.sum_coe_sort plan.freshMembers - (plan.freshSelectorState state selectors) - _ = ∑ i : plan.Member, plan.freshContribution state selectors i := by - symm - simpa [freshContribution] using - (Finset.sum_ite_mem_eq plan.freshMembers - (plan.freshSelectorState state selectors)) - -theorem selectorSum_eq_plannedSelector {source : Instance n} - (plan : Plan source) (state : State n) - (selectors : State plan.freshCount) : - plan.selectorSum state selectors = - ∑ i, plannedSelector plan.reusedMembers (plan.memberState state) - (plan.freshSelectorState state selectors) i := by - rw [selectorSum, plan.sourceReusedSum_eq state, - plan.freshSelectorSum_eq state selectors] - rw [← Finset.sum_add_distrib] - apply Finset.sum_congr rfl - intro i _ - exact (plan.plannedSelector_eq_contributions state selectors i).symm - -@[simp] -theorem cardinalityConstraint_holds {source : Instance n} (plan : Plan source) - (state : State n) (selectors : State plan.freshCount) : - plan.cardinalityConstraint.Holds (State.append state selectors) ↔ - plan.selectorSum state selectors ≤ 1 := by - have hsum : - (∑ i : Fin n, - if i ∈ plan.constraint.members ∧ source.domains i = .binary then - state i - else 0) = - ∑ i ∈ plan.constraint.members, - if source.domains i = .binary then state i else 0 := by - convert Finset.sum_ite_mem_eq plan.constraint.members - (fun i => if source.domains i = .binary then state i else 0) using 1 - simp [ite_and] - simp [cardinalityConstraint, cardinalityExpr, selectorSum, - LinearConstraint.Holds, Affine.eval, State.append, Fin.sum_univ_add] - rw [hsum] - -namespace Validated - -def generatedConstraints {source : Instance n} {plan : Plan source} (validated : plan.Validated) : - List (LinearConstraint (n + plan.freshCount)) := - validated.linkConstraints ++ [plan.cardinalityConstraint] - -end Validated - -theorem plannedSelector_binary_of_domains {source : Instance n} - (plan : Plan source) (state : State n) - (selectors : State plan.freshCount) - (hsourceDomains : ∀ i, state i ∈ source.domains i) - (hselectorDomains : ∀ j, selectors j ∈ Domain.binary) : - GenericBinaryOn Finset.univ - (plannedSelector plan.reusedMembers (plan.memberState state) - (plan.freshSelectorState state selectors)) := by - intro i _ - by_cases hr : i ∈ plan.reusedMembers - · have hdomain : source.domains i = .binary := - (Finset.mem_filter.mp hr).2 - simpa [plannedSelector, hr, memberState, hdomain] using - hsourceDomains i - · have hfresh : i ∈ plan.freshMembers := by - simp [freshMembers, hr] - simpa [plannedSelector, hr, freshSelectorState, hfresh] using - hselectorDomains (plan.freshIndex i hfresh) - -namespace Validated - -theorem linksForFresh_iff_linksForMembers {source : Instance n} - {plan : Plan source} (validated : plan.Validated) (state : State n) - (selectors : State plan.freshCount) : - (∀ j, - OptionalUpperLink (validated.bounds.upper (plan.freshMember j)) - (state (plan.freshMember j).val) (selectors j) ∧ - OptionalLowerLink (validated.bounds.lower (plan.freshMember j)) - (state (plan.freshMember j).val) (selectors j)) ↔ - ∀ i, i ∉ plan.reusedMembers → - OptionalUpperLink (validated.bounds.upper i) - (plan.memberState state i) - (plan.freshSelectorState state selectors i) ∧ - OptionalLowerLink (validated.bounds.lower i) - (plan.memberState state i) - (plan.freshSelectorState state selectors i) := by - constructor - · intro h i hr - have hfresh : i ∈ plan.freshMembers := by - simp [freshMembers, hr] - have hi := h (plan.freshIndex i hfresh) - simpa [memberState, freshSelectorState, hfresh] using hi - · intro h j - have hfresh : plan.freshMember j ∈ plan.freshMembers := - (plan.freshMembers.orderIsoOfFin rfl j).property - have hr : plan.freshMember j ∉ plan.reusedMembers := by - simpa [freshMembers] using hfresh - have hj := h (plan.freshMember j) hr - simpa [memberState, freshSelectorState, hfresh] using hj - -/-- The generated linear rows denote exactly the SDK reused/fresh selector -formulation, provided the old and fresh blocks satisfy their declared domains. -/ -theorem generatedConstraints_hold_iff_plannedSelectorFormulation - {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (state : State n) (selectors : State plan.freshCount) - (hsourceDomains : ∀ i, state i ∈ source.domains i) - (hselectorDomains : ∀ j, selectors j ∈ Domain.binary) : - (∀ constraint ∈ validated.generatedConstraints, - constraint.Holds (State.append state selectors)) ↔ - PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds - (plan.memberState state) - (plan.freshSelectorState state selectors) := by - rw [generatedConstraints, List.forall_mem_append, - List.forall_mem_singleton, validated.linkConstraints_hold_iff, - plan.cardinalityConstraint_holds, - validated.linksForFresh_iff_linksForMembers] - constructor - · rintro ⟨hlinks, hcardinality⟩ - refine { - allSelectorsAreBinary := plan.plannedSelector_binary_of_domains state selectors - hsourceDomains hselectorDomains - nonReusedHaveLinkedSelectors := hlinks - selectorsSumLe1 := ?_ - } - rw [← plan.selectorSum_eq_plannedSelector state selectors] - exact hcardinality - · intro hformulation - refine ⟨hformulation.nonReusedHaveLinkedSelectors, ?_⟩ - rw [plan.selectorSum_eq_plannedSelector state selectors] - exact hformulation.selectorsSumLe1 - -theorem freshSelectors_binary_of_plannedSelectorFormulation - {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (state : State n) (selectors : State plan.freshCount) - (hformulation : PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds - (plan.memberState state) - (plan.freshSelectorState state selectors)) : - ∀ j, selectors j ∈ Domain.binary := by - intro j - have hfresh : plan.freshMember j ∈ plan.freshMembers := - (plan.freshMembers.orderIsoOfFin rfl j).property - have hr : plan.freshMember j ∉ plan.reusedMembers := by - simpa [freshMembers] using hfresh - have hbinary := hformulation.allSelectorsAreBinary (plan.freshMember j) (by simp) - simpa [plannedSelector, hr, freshSelectorState, hfresh] using hbinary - -theorem selectedHolds_of_plannedSelectorFormulation - {source : Instance n} {plan : Plan source} (validated : plan.Validated) - {state : State n} - {selectors : State plan.freshCount} - (hdomains : ∀ i, state i ∈ source.domains i) - (hformulation : PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds - (plan.memberState state) - (plan.freshSelectorState state selectors)) : - plan.constraint.Holds state := by - apply (plan.genericSOS1_memberState_iff_holds state).mp - exact plannedSelectorFormulation_project_sos1 - plan.reusedMembers validated.bounds - (plan.memberState state) - (plan.freshSelectorState state selectors) - (validated.withinBounds_of_domains hdomains) hformulation - -end Validated - -def BaseFeasible {source : Instance n} (plan : Plan source) - (state : State n) : Prop := - (∀ i, state i ∈ source.domains i) ∧ - (∀ constraint ∈ source.constraints, constraint.Holds state) ∧ - (∀ constraint ∈ source.oneHotConstraints, constraint.Holds state) ∧ - (∀ constraint ∈ source.sos1Constraints.eraseIdx plan.constraintIndex.val, - constraint.Holds state) ∧ - ∀ constraint ∈ source.indicatorConstraints, constraint.Holds state - -theorem allSOS1_iff_erased_and_selected {source : Instance n} - (plan : Plan source) (state : State n) : - (∀ constraint ∈ source.sos1Constraints, constraint.Holds state) ↔ - (∀ constraint ∈ - source.sos1Constraints.eraseIdx plan.constraintIndex.val, - constraint.Holds state) ∧ - plan.constraint.Holds state := by - constructor - · intro hall - constructor - · intro constraint hconstraint - exact hall constraint (List.mem_of_mem_eraseIdx hconstraint) - · exact hall plan.constraint (List.get_mem _ plan.constraintIndex) - · rintro ⟨herased, hselected⟩ constraint hconstraint - have hperm := List.getElem_cons_eraseIdx_perm - (l := source.sos1Constraints) plan.constraintIndex.isLt - have hleft : - constraint ∈ - plan.constraint :: - source.sos1Constraints.eraseIdx plan.constraintIndex.val := by - exact hperm.symm.subset hconstraint - rcases List.mem_cons.mp hleft with hsame | herasedMem - · simpa [hsame] using hselected - · exact herased constraint herasedMem - -theorem source_feasible_iff_base_and_selected {source : Instance n} - (plan : Plan source) (state : State n) : - source.Feasible state ↔ - plan.BaseFeasible state ∧ plan.constraint.Holds state := by - unfold Instance.Feasible BaseFeasible - rw [plan.allSOS1_iff_erased_and_selected state] - aesop - -namespace Validated - -def target {source : Instance n} {plan : Plan source} (validated : plan.Validated) : - Instance (n + plan.freshCount) where - domains := Domain.append source.domains (fun _ => .binary) - constraints := - (source.constraints.map fun constraint => - constraint.extend plan.freshCount) ++ validated.generatedConstraints - oneHotConstraints := - source.oneHotConstraints.map fun constraint => - constraint.castAdd plan.freshCount - sos1Constraints := - (source.sos1Constraints.eraseIdx plan.constraintIndex.val).map - fun constraint => constraint.castAdd plan.freshCount - indicatorConstraints := - source.indicatorConstraints.map fun constraint => - constraint.extend plan.freshCount - objective := source.objective.extend plan.freshCount - sense := source.sense - -theorem target_feasible_append_iff_base_and_formulation - {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (state : State n) (selectors : State plan.freshCount) : - validated.target.Feasible (State.append state selectors) ↔ - plan.BaseFeasible state ∧ - PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds - (plan.memberState state) - (plan.freshSelectorState state selectors) := by - have hsourceAt (i : Fin n) : - State.append state selectors (Fin.castAdd plan.freshCount i) = state i := by - simp [State.append] - have hfreshAt (j : Fin plan.freshCount) : - State.append state selectors (Fin.natAdd n j) = selectors j := by - simp [State.append] - simp only [Instance.Feasible, target, Domain.append, - Fin.forall_fin_add, hsourceAt, hfreshAt, Fin.append_left, - Fin.append_right, List.forall_mem_append, List.forall_mem_map, - LinearConstraint.holds_extend_append, - OneHotConstraint.holds_castAdd_append, SOS1Constraint.holds_castAdd_append, - IndicatorConstraint.holds_extend_append, BaseFeasible] - constructor - · rintro ⟨⟨hdomains, hselectors⟩, - ⟨holdConstraints, hgenerated⟩, honeHot, hsos1, hindicator⟩ - have hformulation := - (validated.generatedConstraints_hold_iff_plannedSelectorFormulation - state selectors hdomains hselectors).mp hgenerated - exact ⟨⟨hdomains, holdConstraints, honeHot, hsos1, hindicator⟩, - hformulation⟩ - · rintro ⟨⟨hdomains, holdConstraints, honeHot, hsos1, hindicator⟩, - hformulation⟩ - have hselectors := - validated.freshSelectors_binary_of_plannedSelectorFormulation - state selectors hformulation - have hgenerated := - (validated.generatedConstraints_hold_iff_plannedSelectorFormulation - state selectors hdomains hselectors).mpr hformulation - exact ⟨⟨hdomains, hselectors⟩, - ⟨holdConstraints, hgenerated⟩, honeHot, hsos1, hindicator⟩ - -theorem target_feasible_iff_base_and_formulation - {source : Instance n} {plan : Plan source} (validated : plan.Validated) - (state : State (n + plan.freshCount)) : - validated.target.Feasible state ↔ - plan.BaseFeasible (State.source state) ∧ - PlannedSelectorFormulationHolds plan.reusedMembers validated.bounds - (plan.memberState (State.source state)) - (plan.freshSelectorState (State.source state) - (State.extendedPart state)) := by - simpa only [State.append_source_extendedPart] using - validated.target_feasible_append_iff_base_and_formulation - (State.source state) (State.extendedPart state) - -end Validated - -end Plan - -end SOS1BigM - -end Instance - -end OMMXProof diff --git a/lean/OMMXProofTest.lean b/lean/OMMXProofTest.lean index 33b17a304..ba5005853 100644 --- a/lean/OMMXProofTest.lean +++ b/lean/OMMXProofTest.lean @@ -2,5 +2,7 @@ import OMMXProofTest.Affine import OMMXProofTest.Domain import OMMXProofTest.IndicatorBigM import OMMXProofTest.SOS1BigM +import OMMXProofTest.SOS1BigM.Lowering +import OMMXProofTest.SOS1BigM.Promotion import OMMXProofTest.Transform import OMMXProofTest.Trust diff --git a/lean/OMMXProofTest/SOS1BigM.lean b/lean/OMMXProofTest/SOS1BigM.lean index 6ee745d37..2f449247c 100644 --- a/lean/OMMXProofTest/SOS1BigM.lean +++ b/lean/OMMXProofTest/SOS1BigM.lean @@ -1,261 +1,9 @@ -import OMMXProof.Instance.Transform.SOS1BigM +import OMMXProofTest.SOS1BigM.Lowering +import OMMXProofTest.SOS1BigM.Promotion /-! # SOS1 Big-M transformation fixtures -The fixture mixes one reused binary member with one continuous member that -needs a fresh selector. Its lower bound is zero, so lowering from the plan -emits only the upper link for that member. +This module collects executable fixtures for both SOS1 Big-M lowering and +promotion. -/ - -namespace OMMXProof.Test.SOS1BigM - -open Instance.SOS1BigM - -/-! Mixed selector formulation: member 0 is reused as its own binary selector, -while member 1 gets a fresh selector. Its lower bound is zero, so the lower -link is omitted by the lowering. -/ - -def plannedReusedExample : Finset (Fin 2) := {0} - -def plannedBoundsExample : SelectorBounds (Fin 2) where - lower := fun _ => 0 - upper := fun i => if i.val = 0 then 1 else 3 - -def plannedMembersExample : Fin 2 → Rat := fun i => if i.val = 0 then 0 else 2 - -def plannedFreshSelectorsExample : Fin 2 → Rat := fun _ => 1 - -example : PlannedSelectorFormulationHolds plannedReusedExample plannedBoundsExample - plannedMembersExample plannedFreshSelectorsExample := by - native_decide - -def invalidPlannedMembersExample : Fin 2 → Rat := - fun i => if i.val = 0 then 1 else 2 - -example : ¬PlannedSelectorFormulationHolds plannedReusedExample plannedBoundsExample - invalidPlannedMembersExample plannedFreshSelectorsExample := by - native_decide - -def members : Finset (Fin 2) := Finset.univ - -def domains : Fin 2 → Domain := - fun i => - if i = 0 then .binary - else .continuous (.finite 0 2 (by norm_num)) - -def objective : Affine 2 where - coeff := fun i => if i = 0 then 1 else 2 - constant := 0 - -def selected : SOS1Constraint 2 where - members := members - -def source : Instance 2 where - domains := domains - constraints := [] - sos1Constraints := [selected] - objective := objective - sense := .minimize - -def plan : Plan source where - constraintIndex := ⟨0, by native_decide⟩ - -theorem plan_valid : plan.Valid := by native_decide - -theorem plan_validate_isSome : plan.validate.isSome = true := by - native_decide - -def validated : plan.Validated := - plan.validate.get plan_validate_isSome - -theorem lowering_plan_isSome : (lowering plan).isSome = true := by - native_decide - -def transform : Instance.Transform source := - (lowering plan).get lowering_plan_isSome - -theorem lowering_plan : lowering plan = some transform := - (Option.some_get lowering_plan_isSome).symm - -example : plan.reusedMembers.card = 1 := by native_decide - -example : plan.freshMembers.card = 1 := by native_decide - -example : plan.freshCount = 1 := by native_decide - -def freshZero : Fin plan.freshCount := - ⟨0, by native_decide⟩ - -example : validated.bounds.lower (plan.freshMember freshZero) = 0 := by - native_decide - -example : validated.bounds.upper (plan.freshMember freshZero) = 2 := by - native_decide - -/-- One nontrivial upper link; the zero lower-bound side is omitted. -/ -example : validated.linkConstraints.length = 1 := by native_decide - -example : validated.generatedConstraints.length = 2 := by native_decide - -example : transform.targetDimension = 3 := by native_decide - -example : transform.IsReduction := - lowering_isReduction plan lowering_plan - -example : transform.IsRelaxation := - lowering_isRelaxation plan lowering_plan - -example : transform.SensePreserving := - lowering_sensePreserving plan lowering_plan - -example : transform.SourceObjectiveValuePreserving := - lowering_sourceObjectiveValuePreserving plan lowering_plan - -example : transform.TargetObjectiveValuePreserving := - lowering_targetObjectiveValuePreserving plan lowering_plan - -example : transform.SourceObjectivePreserving := - lowering_sourceObjectivePreserving plan lowering_plan - -example : transform.TargetObjectivePreserving := - lowering_targetObjectivePreserving plan lowering_plan - -example : transform.SourceRoundTrip := - lowering_sourceRoundTrip plan lowering_plan - -/-! Only selected member bounds must be finite. Empty SOS1 constraints and -finite member bounds that exclude zero need no additional preconditions. -/ - -def emptySource : Instance 1 where - domains := fun _ => .continuous - constraints := [] - sos1Constraints := [{ members := ∅ }] - objective := Affine.zero - sense := .minimize - -def emptyPlan : Plan emptySource where - constraintIndex := ⟨0, by native_decide⟩ - -example : emptyPlan.Valid := by native_decide - -example : (lowering emptyPlan).isSome = true := by native_decide - -def positiveBoundedSource : Instance 1 where - domains := fun _ => .continuous (.finite 1 3 (by norm_num)) - constraints := [] - sos1Constraints := [{ members := Finset.univ }] - objective := Affine.zero - sense := .minimize - -def positiveBoundedPlan : Plan positiveBoundedSource where - constraintIndex := ⟨0, by native_decide⟩ - -example : positiveBoundedPlan.Valid := by native_decide - -example : (lowering positiveBoundedPlan).isSome = true := by native_decide - -def unboundedSource : Instance 1 where - domains := fun _ => .continuous - constraints := [] - sos1Constraints := [{ members := Finset.univ }] - objective := Affine.zero - sense := .minimize - -def unboundedPlan : Plan unboundedSource where - constraintIndex := ⟨0, by native_decide⟩ - -/-- A valid plan for a fresh selector requires finite source bounds. -/ -example : ¬unboundedPlan.Valid := by native_decide - -example : lowering unboundedPlan = none := by native_decide - -def lowerBoundedSource : Instance 1 := - { unboundedSource with - domains := fun _ => .continuous (.lowerBounded 0) } - -def lowerBoundedPlan : Plan lowerBoundedSource where - constraintIndex := ⟨0, by native_decide⟩ - -example : ¬lowerBoundedPlan.Valid := by native_decide - -example : lowering lowerBoundedPlan = none := by native_decide - -def upperBoundedSource : Instance 1 := - { unboundedSource with - domains := fun _ => .continuous (.upperBounded 0) } - -def upperBoundedPlan : Plan upperBoundedSource where - constraintIndex := ⟨0, by native_decide⟩ - -example : ¬upperBoundedPlan.Valid := by native_decide - -example : lowering upperBoundedPlan = none := by native_decide - -def zeroSource : State 2 := fun _ => 0 - -theorem zeroSource_feasible : source.Feasible zeroSource := by - unfold Instance.Feasible - refine ⟨?_, ?_, ?_, ?_, ?_⟩ - · intro i - fin_cases i <;> native_decide - · simp [source] - · simp [source] - · simp [source, selected, SOS1Constraint.Holds, zeroSource] - · simp [source] - -example : - Option.map transform.target.ObjectiveValue - (transform.encode zeroSource) = - some (source.ObjectiveValue zeroSource) := - lowering_sourceObjectiveValuePreserving plan lowering_plan - zeroSource_feasible - -def oneSelector : State plan.freshCount := fun _ => 1 - -def noncanonicalTarget : State (2 + plan.freshCount) := - State.append zeroSource oneSelector - -/-- A zero member permits either selector value, so canonical re-encoding does -not recover every feasible target state. -/ -theorem not_targetRoundTrip_of_lowering - {lowered : Instance.Transform source} - (hlowering : lowering plan = some lowered) : - ¬lowered.TargetRoundTrip := by - unfold lowering at hlowering - rcases Option.map_eq_some_iff.mp hlowering with - ⟨validated, hvalidated, rfl⟩ - clear hlowering - have htarget : - validated.target.Feasible noncanonicalTarget := by - rw [noncanonicalTarget, - validated.target_feasible_append_iff_base_and_formulation] - refine - ⟨(plan.source_feasible_iff_base_and_selected zeroSource).mp - zeroSource_feasible |>.1, - ?_⟩ - native_decide +revert - intro hroundTrip - have hstate := hroundTrip htarget - change - some (State.append (State.source noncanonicalTarget) fun j => - canonicalSelector - (plan.memberState (State.source noncanonicalTarget)) - (plan.freshMember j)) = - some noncanonicalTarget at hstate - have heq : - State.append (State.source noncanonicalTarget) (fun j => - canonicalSelector - (plan.memberState (State.source noncanonicalTarget)) - (plan.freshMember j)) = - noncanonicalTarget := - Option.some.inj hstate - have hcomponent := congrArg - (fun state => state (Fin.natAdd 2 freshZero)) heq - simp [Plan.memberState, noncanonicalTarget, oneSelector, zeroSource, - canonicalSelector, State.source, State.append] at hcomponent - -example : ¬transform.TargetRoundTrip := - not_targetRoundTrip_of_lowering lowering_plan - -end OMMXProof.Test.SOS1BigM diff --git a/lean/OMMXProofTest/SOS1BigM/Lowering.lean b/lean/OMMXProofTest/SOS1BigM/Lowering.lean new file mode 100644 index 000000000..408d7c46e --- /dev/null +++ b/lean/OMMXProofTest/SOS1BigM/Lowering.lean @@ -0,0 +1,264 @@ +import OMMXProof.Instance.Transform.SOS1BigM.Lowering + +/-! +# SOS1 Big-M transformation fixtures + +The fixture mixes one reused binary member with one continuous member that +needs a fresh selector. Its lower bound is zero, so lowering from the plan +emits only the upper link for that member. +-/ + +namespace OMMXProof.Test.SOS1BigM.Lowering + +open Instance.SOS1BigM + +/-! Mixed selector formulation: member 0 is reused as its own binary selector, +while member 1 gets a fresh selector. Its lower bound is zero, so the lower +link is omitted by the lowering. -/ + +def plannedReusedExample : Finset (Fin 2) := {0} + +def plannedBoundsExample : SelectorBounds (Fin 2) where + lower := fun _ => 0 + upper := fun i => if i.val = 0 then 1 else 3 + +def plannedMembersExample : Fin 2 → Rat := fun i => if i.val = 0 then 0 else 2 + +def plannedFreshSelectorsExample : Fin 2 → Rat := fun _ => 1 + +example : PlannedSelectorFormulationHolds plannedReusedExample plannedBoundsExample + plannedMembersExample plannedFreshSelectorsExample := by + native_decide + +def invalidPlannedMembersExample : Fin 2 → Rat := + fun i => if i.val = 0 then 1 else 2 + +example : ¬PlannedSelectorFormulationHolds plannedReusedExample plannedBoundsExample + invalidPlannedMembersExample plannedFreshSelectorsExample := by + native_decide + +def members : Finset (Fin 2) := Finset.univ + +def domains : Fin 2 → Domain := + fun i => + if i = 0 then .binary + else .continuous (.finite 0 2 (by norm_num)) + +def objective : Affine 2 where + coeff := fun i => if i = 0 then 1 else 2 + constant := 0 + +def selected : SOS1Constraint 2 where + members := members + +def source : Instance 2 where + domains := domains + constraints := [] + sos1Constraints := [selected] + objective := objective + sense := .minimize + +def plan : Plan source where + constraintIndex := ⟨0, by native_decide⟩ + +theorem plan_valid : plan.Valid := by native_decide + +theorem plan_validate_isSome : plan.validate.isSome = true := by + native_decide + +def validated : plan.Validated := + plan.validate.get plan_validate_isSome + +theorem lowering_plan_isSome : (lowering plan).isSome = true := by + native_decide + +def transform : Instance.Transform source := + (lowering plan).get lowering_plan_isSome + +theorem lowering_plan : lowering plan = some transform := + (Option.some_get lowering_plan_isSome).symm + +example : plan.reusedMembers.card = 1 := by native_decide + +example : plan.freshMembers.card = 1 := by native_decide + +example : plan.freshCount = 1 := by native_decide + +def freshZero : Fin plan.freshCount := + ⟨0, by native_decide⟩ + +example : validated.bounds.lower (plan.freshMember freshZero) = 0 := by + native_decide + +example : validated.bounds.upper (plan.freshMember freshZero) = 2 := by + native_decide + +/-- One nontrivial upper link; the zero lower-bound side is omitted. -/ +example : + (plan.selectorLayout.linkConstraints validated.bounds).length = 1 := by + native_decide + +example : validated.generatedConstraints.length = 2 := by native_decide + +example : transform.targetDimension = 3 := by native_decide + +example : transform.IsReduction := + lowering_isReduction plan lowering_plan + +example : transform.IsRelaxation := + lowering_isRelaxation plan lowering_plan + +example : transform.SensePreserving := + lowering_sensePreserving plan lowering_plan + +example : transform.SourceObjectiveValuePreserving := + lowering_sourceObjectiveValuePreserving plan lowering_plan + +example : transform.TargetObjectiveValuePreserving := + lowering_targetObjectiveValuePreserving plan lowering_plan + +example : transform.SourceObjectivePreserving := + lowering_sourceObjectivePreserving plan lowering_plan + +example : transform.TargetObjectivePreserving := + lowering_targetObjectivePreserving plan lowering_plan + +example : transform.SourceRoundTrip := + lowering_sourceRoundTrip plan lowering_plan + +/-! Only selected member bounds must be finite. Empty SOS1 constraints and +finite member bounds that exclude zero need no additional preconditions. -/ + +def emptySource : Instance 1 where + domains := fun _ => .continuous + constraints := [] + sos1Constraints := [{ members := ∅ }] + objective := Affine.zero + sense := .minimize + +def emptyPlan : Plan emptySource where + constraintIndex := ⟨0, by native_decide⟩ + +example : emptyPlan.Valid := by native_decide + +example : (lowering emptyPlan).isSome = true := by native_decide + +def positiveBoundedSource : Instance 1 where + domains := fun _ => .continuous (.finite 1 3 (by norm_num)) + constraints := [] + sos1Constraints := [{ members := Finset.univ }] + objective := Affine.zero + sense := .minimize + +def positiveBoundedPlan : Plan positiveBoundedSource where + constraintIndex := ⟨0, by native_decide⟩ + +example : positiveBoundedPlan.Valid := by native_decide + +example : (lowering positiveBoundedPlan).isSome = true := by native_decide + +def unboundedSource : Instance 1 where + domains := fun _ => .continuous + constraints := [] + sos1Constraints := [{ members := Finset.univ }] + objective := Affine.zero + sense := .minimize + +def unboundedPlan : Plan unboundedSource where + constraintIndex := ⟨0, by native_decide⟩ + +/-- A valid plan for a fresh selector requires finite source bounds. -/ +example : ¬unboundedPlan.Valid := by native_decide + +example : lowering unboundedPlan = none := by native_decide + +def lowerBoundedSource : Instance 1 := + { unboundedSource with + domains := fun _ => .continuous (.lowerBounded 0) } + +def lowerBoundedPlan : Plan lowerBoundedSource where + constraintIndex := ⟨0, by native_decide⟩ + +example : ¬lowerBoundedPlan.Valid := by native_decide + +example : lowering lowerBoundedPlan = none := by native_decide + +def upperBoundedSource : Instance 1 := + { unboundedSource with + domains := fun _ => .continuous (.upperBounded 0) } + +def upperBoundedPlan : Plan upperBoundedSource where + constraintIndex := ⟨0, by native_decide⟩ + +example : ¬upperBoundedPlan.Valid := by native_decide + +example : lowering upperBoundedPlan = none := by native_decide + +def zeroSource : State 2 := fun _ => 0 + +theorem zeroSource_feasible : source.Feasible zeroSource := by + unfold Instance.Feasible + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + · intro i + fin_cases i <;> native_decide + · simp [source] + · simp [source] + · simp [source, selected, SOS1Constraint.Holds, zeroSource] + · simp [source] + +example : + Option.map transform.target.ObjectiveValue + (transform.encode zeroSource) = + some (source.ObjectiveValue zeroSource) := + lowering_sourceObjectiveValuePreserving plan lowering_plan + zeroSource_feasible + +def oneSelector : State plan.freshCount := fun _ => 1 + +def noncanonicalTarget : State (2 + plan.freshCount) := + State.append zeroSource oneSelector + +/-- A zero member permits either selector value, so canonical re-encoding does +not recover every feasible target state. -/ +theorem not_targetRoundTrip_of_lowering + {lowered : Instance.Transform source} + (hlowering : lowering plan = some lowered) : + ¬lowered.TargetRoundTrip := by + unfold lowering at hlowering + rcases Option.map_eq_some_iff.mp hlowering with + ⟨validated, hvalidated, rfl⟩ + clear hlowering + have htarget : + validated.target.Feasible noncanonicalTarget := by + rw [noncanonicalTarget, + validated.target_feasible_append_iff_base_and_formulation] + refine + ⟨(plan.source_feasible_iff_base_and_selected zeroSource).mp + zeroSource_feasible |>.1, + ?_⟩ + native_decide +revert + intro hroundTrip + have hstate := hroundTrip htarget + change + some (State.append (State.source noncanonicalTarget) fun j => + canonicalSelector + (plan.memberState (State.source noncanonicalTarget)) + (plan.freshMember j)) = + some noncanonicalTarget at hstate + have heq : + State.append (State.source noncanonicalTarget) (fun j => + canonicalSelector + (plan.memberState (State.source noncanonicalTarget)) + (plan.freshMember j)) = + noncanonicalTarget := + Option.some.inj hstate + have hcomponent := congrArg + (fun state => state (Fin.natAdd 2 freshZero)) heq + simp [Plan.memberState, SelectorLayout.memberState, noncanonicalTarget, + oneSelector, zeroSource, canonicalSelector, State.source, + State.append] at hcomponent + +example : ¬transform.TargetRoundTrip := + not_targetRoundTrip_of_lowering lowering_plan + +end OMMXProof.Test.SOS1BigM.Lowering diff --git a/lean/OMMXProofTest/SOS1BigM/Promotion.lean b/lean/OMMXProofTest/SOS1BigM/Promotion.lean new file mode 100644 index 000000000..367b5fc1e --- /dev/null +++ b/lean/OMMXProofTest/SOS1BigM/Promotion.lean @@ -0,0 +1,431 @@ +import OMMXProof.Instance.Transform.SOS1BigM.Promotion + +/-! +# SOS1 Big-M promotion fixtures + +The accepted fixture is an independently written flat selector formulation. +It does not call SOS1 lowering, so promotion validation depends only on the +flat `Instance` and the user-supplied witness. + +The retained variables are a reused binary member `x` and a bounded continuous +member `y ∈ [-2, 3]`. A fresh binary selector `z` is appended at the end. +The retained regular row is followed by the exact upper link, lower link, and +cardinality suffix: + +* `x + y ≤ 2`, +* `y - 3z ≤ 0`, +* `-y - 2z ≤ 0`, +* `x + z ≤ 1`. + +The rejection fixtures exercise the initial checker as a conservative +sufficient-condition recognizer. Rejection is intentionally not interpreted +as evidence that no correct promotion exists. +-/ + +namespace OMMXProof.Test.SOS1BigM.Promotion + +open Instance.SOS1BigM + +def members : Finset (Fin 2) := Finset.univ + +def freshMembers : Finset {i // i ∈ members} := + {⟨1, by native_decide⟩} + +def witness : Witness 2 where + members := members + freshMembers := freshMembers + retainedConstraintCount := 1 + +example : witness.freshCount = 1 := by + native_decide + +def freshZero : Fin witness.freshCount := + ⟨0, by native_decide⟩ + +theorem freshMember_zero_val : + (witness.freshMember freshZero).val = 1 := by + native_decide + +/-! ## Independently written flat source -/ + +def flatDomains : Fin (2 + witness.freshCount) → Domain := + fun i => + if i.val = 0 then .binary + else if i.val = 1 then .continuous (.finite (-2) 3 (by norm_num)) + else .binary + +def affine (x y z constant : Rat) : + Affine (2 + witness.freshCount) where + coeff := fun i => + if i.val = 0 then x + else if i.val = 1 then y + else z + constant := constant + +def row (x y z constant : Rat) : + LinearConstraint (2 + witness.freshCount) where + expr := affine x y z constant + sense := .lessEqual + +def retainedRow : LinearConstraint (2 + witness.freshCount) := + row 1 1 0 (-2) + +def upperLink : LinearConstraint (2 + witness.freshCount) := + row 0 1 (-3) 0 + +def lowerLink : LinearConstraint (2 + witness.freshCount) := + row 0 (-1) (-2) 0 + +def cardinality : LinearConstraint (2 + witness.freshCount) := + row 1 0 1 (-1) + +def objective : Affine (2 + witness.freshCount) := + affine 1 2 0 0 + +def source : Instance (2 + witness.freshCount) where + domains := flatDomains + constraints := [retainedRow, upperLink, lowerLink, cardinality] + oneHotConstraints := [] + sos1Constraints := [] + indicatorConstraints := [] + objective := objective + sense := .minimize + +theorem source_validate_isSome : + (witness.validate source).isSome = true := by + native_decide + +def validated : witness.Validated source := + (witness.validate source).get source_validate_isSome + +def transform : Instance.Transform source := + promotion witness source + +example : transform.targetDimension = 2 := by + rfl + +example : transform.target.constraints.length = 1 := by + native_decide + +example : transform.target.sos1Constraints.length = 1 := by + native_decide + +example : + (transform.target.sos1Constraints.get ⟨0, by native_decide⟩).members = + members := by + native_decide + +example : transform.IsReduction := + promotion_isReduction validated + +example : transform.IsRelaxation := + promotion_isRelaxation validated + +example : transform.SensePreserving := + promotion_sensePreserving witness source + +example : transform.SourceObjectiveValuePreserving := + promotion_sourceObjectiveValuePreserving validated + +example : transform.TargetObjectiveValuePreserving := + promotion_targetObjectiveValuePreserving validated + +example : transform.SourceObjectivePreserving := + promotion_sourceObjectivePreserving validated + +example : transform.TargetObjectivePreserving := + promotion_targetObjectivePreserving validated + +example : transform.TargetRoundTrip := + promotion_targetRoundTrip witness source + +/-! ## Conservative rejection fixtures -/ + +def selectorNonbinarySource : Instance (2 + witness.freshCount) := + { source with + domains := fun i => + if i.val = 2 then .continuous (.finite 0 1 (by norm_num)) + else flatDomains i } + +def unboundedMemberSource : Instance (2 + witness.freshCount) := + { source with + domains := fun i => + if i.val = 0 then .binary + else if i.val = 1 then .continuous + else .binary } + +def badUpperSource : Instance (2 + witness.freshCount) := + { source with + constraints := + [retainedRow, row 0 1 (-4) 0, lowerLink, cardinality] } + +def badCardinalitySource : Instance (2 + witness.freshCount) := + { source with + constraints := + [retainedRow, upperLink, lowerLink, row 1 0 1 (-2)] } + +def objectiveDependencySource : Instance (2 + witness.freshCount) := + { source with objective := affine 1 2 1 0 } + +def retainedDependencySource : Instance (2 + witness.freshCount) := + { source with + constraints := + [row 1 1 1 (-2), upperLink, lowerLink, cardinality] } + +/-- Member `x` is still declared reused by the witness but is no longer +binary. The adjusted cardinality row matches the domains, isolating the +reused-member classification check. -/ +def reusedNonbinarySource : Instance (2 + witness.freshCount) := + { source with + domains := fun i => + if i.val = 0 then .continuous (.finite 0 1 (by norm_num)) + else flatDomains i + constraints := + [retainedRow, upperLink, lowerLink, row 0 0 1 (-1)] } + +def existingOneHotSource : Instance (2 + witness.freshCount) := + { source with + oneHotConstraints := [{ members := {0} }] } + +def existingSOS1Source : Instance (2 + witness.freshCount) := + { source with + sos1Constraints := [{ members := {0} }] } + +def existingIndicatorSource : Instance (2 + witness.freshCount) := + { source with + indicatorConstraints := + [{ trigger := 0 + polarity := .activeOnOne + body := retainedRow }] } + +theorem existingOneHotSource_validate_isSome : + (witness.validate existingOneHotSource).isSome = true := by + native_decide + +def existingOneHotTransform : Instance.Transform existingOneHotSource := + promotion witness existingOneHotSource + +example : existingOneHotTransform.target.oneHotConstraints.length = 1 := by + native_decide + +example : + (existingOneHotTransform.target.oneHotConstraints.get + ⟨0, by native_decide⟩).members = ({0} : Finset (Fin 2)) := by + native_decide + +theorem existingSOS1Source_validate_isSome : + (witness.validate existingSOS1Source).isSome = true := by + native_decide + +def existingSOS1Transform : Instance.Transform existingSOS1Source := + promotion witness existingSOS1Source + +/-- A previously promoted SOS1 is retained before the newly promoted one. -/ +example : existingSOS1Transform.target.sos1Constraints.length = 2 := by + native_decide + +example : + (existingSOS1Transform.target.sos1Constraints.get + ⟨0, by native_decide⟩).members = ({0} : Finset (Fin 2)) := by + native_decide + +example : + (existingSOS1Transform.target.sos1Constraints.get + ⟨1, by native_decide⟩).members = members := by + native_decide + +theorem existingIndicatorSource_validate_isSome : + (witness.validate existingIndicatorSource).isSome = true := by + native_decide + +def existingIndicatorTransform : Instance.Transform existingIndicatorSource := + promotion witness existingIndicatorSource + +example : existingIndicatorTransform.target.indicatorConstraints.length = 1 := by + native_decide + +example : + (existingIndicatorTransform.target.indicatorConstraints.get + ⟨0, by native_decide⟩).trigger.val = 0 := by + native_decide + +example : + let body := + (existingIndicatorTransform.target.indicatorConstraints.get + ⟨0, by native_decide⟩).body + body.expr.coeff (0 : Fin 2) = 1 ∧ + body.expr.coeff (1 : Fin 2) = 1 ∧ + body.expr.constant = -2 ∧ + body.sense = .lessEqual := by + native_decide + +def freshOneHotMemberSource : Instance (2 + witness.freshCount) := + { source with + oneHotConstraints := [{ members := {0, 2} }] } + +def freshSOS1MemberSource : Instance (2 + witness.freshCount) := + { source with + sos1Constraints := [{ members := {0, 2} }] } + +def freshIndicatorTriggerSource : Instance (2 + witness.freshCount) := + { source with + indicatorConstraints := + [{ trigger := 2 + polarity := .activeOnOne + body := retainedRow }] } + +def freshIndicatorBodySource : Instance (2 + witness.freshCount) := + { source with + indicatorConstraints := + [{ trigger := 0 + polarity := .activeOnOne + body := row 0 0 1 0 }] } + +example : witness.validate selectorNonbinarySource = none := by + native_decide + +example : witness.validate unboundedMemberSource = none := by + native_decide + +example : witness.validate badUpperSource = none := by + native_decide + +example : witness.validate badCardinalitySource = none := by + native_decide + +example : witness.validate objectiveDependencySource = none := by + native_decide + +example : witness.validate retainedDependencySource = none := by + native_decide + +example : witness.validate reusedNonbinarySource = none := by + native_decide + +example : witness.validate freshOneHotMemberSource = none := by + native_decide + +example : witness.validate freshSOS1MemberSource = none := by + native_decide + +example : witness.validate freshIndicatorTriggerSource = none := by + native_decide + +example : witness.validate freshIndicatorBodySource = none := by + native_decide + +/-! ## Multiple sequential SOS1 promotions -/ + +namespace MultipleSOS1 + +def members : Finset (Fin 3) := {0, 1} + +def freshMembers : Finset {i // i ∈ members} := + {⟨1, by native_decide⟩} + +def witness : Witness 3 where + members := members + freshMembers := freshMembers + retainedConstraintCount := 0 + +def domains : Fin (3 + witness.freshCount) → Domain := + fun i => + if i.val = 0 then .binary + else if i.val = 1 then .continuous (.finite (-2) 3 (by norm_num)) + else if i.val = 2 then .continuous (.finite (-1) 1 (by norm_num)) + else .binary + +/-- The formulation rows are generated here to keep this fixture focused on +preservation of a distinct SOS1 recovered by an earlier promotion. -/ +def skeleton : Instance (3 + witness.freshCount) where + domains := domains + constraints := [] + oneHotConstraints := [] + sos1Constraints := [] + indicatorConstraints := [] + objective := Affine.zero + sense := .minimize + +def source : Instance (3 + witness.freshCount) := + { skeleton with + constraints := + witness.selectorLayout.canonicalRows (witness.selectorBounds skeleton) + sos1Constraints := [{ members := {1, 2} }] } + +theorem source_validate_isSome : + (witness.validate source).isSome = true := by + native_decide + +def validated : witness.Validated source := + (witness.validate source).get source_validate_isSome + +def transform : Instance.Transform source := + promotion witness source + +example : transform.target.sos1Constraints.length = 2 := by + native_decide + +example : + (transform.target.sos1Constraints.get + ⟨0, by native_decide⟩).members = ({1, 2} : Finset (Fin 3)) := by + native_decide + +example : + (transform.target.sos1Constraints.get + ⟨1, by native_decide⟩).members = members := by + native_decide + +example : transform.IsReduction := + promotion_isReduction validated + +example : transform.IsRelaxation := + promotion_isRelaxation validated + +end MultipleSOS1 + +/-! ## Noncanonical feasible flat state -/ + +def noncanonicalSourceState : State (2 + witness.freshCount) := + fun i => if i.val = 2 then 1 else 0 + +theorem noncanonicalSourceState_feasible : + source.Feasible noncanonicalSourceState := by + unfold Instance.Feasible + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + · intro i + fin_cases i <;> native_decide + · intro constraint hconstraint + simp only [source, List.mem_cons, List.not_mem_nil, or_false] at hconstraint + rcases hconstraint with rfl | rfl | rfl | rfl + all_goals native_decide + · simp [source] + · simp [source] + · simp [source] + +/-- The flat source admits a noncanonical selector value when both members are +zero. Promotion projects it away and canonical decoding restores `z = 0`, so +the source-side round trip is intentionally not guaranteed. -/ +example : ¬transform.SourceRoundTrip := by + intro hroundTrip + have hstate := hroundTrip noncanonicalSourceState_feasible + change + some + (State.append (State.source noncanonicalSourceState) fun j => + canonicalSelector + (witness.memberState (State.source noncanonicalSourceState)) + (witness.freshMember j)) = + some noncanonicalSourceState at hstate + have heq : + State.append (State.source noncanonicalSourceState) (fun j => + canonicalSelector + (witness.memberState (State.source noncanonicalSourceState)) + (witness.freshMember j)) = + noncanonicalSourceState := + Option.some.inj hstate + have hcomponent := congrArg + (fun state => state (Fin.natAdd 2 freshZero)) heq + simp [noncanonicalSourceState, Witness.memberState, + SelectorLayout.memberState, State.source, State.append, + canonicalSelector, freshMember_zero_val] at hcomponent + +end OMMXProof.Test.SOS1BigM.Promotion diff --git a/lean/README.md b/lean/README.md index 2b7fc5740..7838d5344 100644 --- a/lean/README.md +++ b/lean/README.md @@ -36,7 +36,9 @@ The current model focuses on exact-rational affine optimization. It provides: - an `Instance.Transform` contract with explicit target, encode/decode, directional preservation, round-trip, and composition laws; and - partial Indicator and SOS1 Big-M lowering that validates a `Plan` before - constructing an `Instance.Transform`. + constructing an `Instance.Transform`; and +- conservative SOS1 Big-M promotion that validates an untrusted `Witness` + before establishing transformation correctness. Detailed modules and implemented features are listed below. SDK serialization and lifecycle, floating-point behavior, Rust mutation correctness, and @@ -61,11 +63,18 @@ completeness of recognition or presolve algorithms remain outside this model. | `OMMXProof.Instance.Transform.IndicatorBigM.Target` | Generated linear rows, target Instance construction, and feasibility equivalence | | `OMMXProof.Instance.Transform.IndicatorBigM.Basic` | Partial lowering with identity state maps and transformation correctness | | `OMMXProof.Instance.Transform.IndicatorBigM` | Entrypoint for the complete Indicator Big-M lowering | -| `OMMXProof.Instance.Transform.SOS1BigM.Formulation` | Mixed reused/fresh selector formulation and its exact relation to SOS1 semantics | -| `OMMXProof.Instance.Transform.SOS1BigM.Plan` | SOS1 selection, reused/fresh member partitioning, and finite-bound validation | -| `OMMXProof.Instance.Transform.SOS1BigM.Target` | Big-M links, selector cardinality, target Instance construction, and feasibility equivalence | -| `OMMXProof.Instance.Transform.SOS1BigM.Basic` | Partial lowering, canonical encoding, source projection, and transformation correctness | -| `OMMXProof.Instance.Transform.SOS1BigM` | Entrypoint for the complete SOS1 Big-M lowering | +| `OMMXProof.Instance.Transform.SOS1BigM.SelectorFormulation` | Shared selector semantics and layout, canonical Big-M rows, and their exact relation to SOS1 | +| `OMMXProof.Instance.Transform.SOS1BigM.Lowering.Plan` | SOS1 selection, reused/fresh member partitioning, and finite-bound validation | +| `OMMXProof.Instance.Transform.SOS1BigM.Lowering.Target` | Canonical-row instantiation, target Instance construction, and feasibility equivalence | +| `OMMXProof.Instance.Transform.SOS1BigM.Lowering.Basic` | Partial lowering, canonical encoding, source projection, and transformation correctness | +| `OMMXProof.Instance.Transform.SOS1BigM.Lowering` | Entrypoint for complete SOS1 Big-M lowering | +| `OMMXProof.Instance.Transform.SOS1BigM.Promotion.Witness` | Untrusted retained/fresh suffix layout supplied to the promotion checker | +| `OMMXProof.Instance.Transform.SOS1BigM.Promotion.Target` | Retained-prefix projection, promoted target construction, and target feasibility characterization | +| `OMMXProof.Instance.Transform.SOS1BigM.Promotion.Validation` | Direct canonical-row validation and structural source equalities derived from a validated witness | +| `OMMXProof.Instance.Transform.SOS1BigM.Promotion.Semantics` | Feasibility, canonical-selector, and objective characterizations for validated promotion | +| `OMMXProof.Instance.Transform.SOS1BigM.Promotion.Basic` | Total witnessed promotion plus correctness theorems under validated sufficient conditions | +| `OMMXProof.Instance.Transform.SOS1BigM.Promotion` | Entrypoint for complete SOS1 Big-M promotion | +| `OMMXProof.Instance.Transform.SOS1BigM` | Umbrella for both directions of the SOS1 Big-M formulation | | `OMMXProof.Instance.Transform` | Entrypoint for common transformation semantics and all concrete Instance transformations | ## Checks @@ -100,18 +109,19 @@ includes Lean's standard `propext`, `Classical.choice`, and `Quot.sound` axioms. - [x] Reduction/relaxation composition and encode/decode round-trip laws - [x] Partial Indicator Big-M lowering with validated affine body bounds and identity state maps - [x] Partial SOS1 Big-M lowering with mixed reused/fresh selector layouts +- [x] Conservative SOS1 Big-M promotion from a standard selector/link suffix - [x] Executable accept/reject fixtures and counterexamples ## Planned directions -The packaged `Instance.Transform` examples currently focus on lowering -Indicator and SOS1 constraints into regular linear constraints. The common -transformation contract is not restricted to lowering or to presolve -reductions. The intended next directions are: +The packaged `Instance.Transform` examples include lowering Indicator and SOS1 +constraints into regular linear constraints and promoting one standard SOS1 +Big-M layout back to a first-class SOS1 constraint. The common transformation +contract is not restricted to lowering or to presolve reductions. The intended +next directions are: -- promotion from regular linear formulations to higher-level constraint - families, including validation of whether earlier lowering data still - supports inverse lowering after presolve; +- promotion from alternative regular or nonlinear formulations to higher-level + constraint families beyond the currently recognized SOS1 Big-M layout; - presolve transformations for MILP problems represented by `Instance`; - more general presolve transformations beyond the current affine MILP fragment; @@ -121,6 +131,6 @@ reductions. The intended next directions are: - a canonical SDK-to-Lean bridge in which SDK-produced `Witness` values are checked against this formal contract. -The future SDK-produced `Witness` is distinct from the current in-Lean `Plan`, -which selects and validates one lowering operation. The versioned `Witness` -contract, bridge, and SDK-side producer are intentionally unimplemented here. +The current in-Lean promotion `Witness` is untrusted layout data checked against +the source Instance. A future versioned SDK contract, bridge, and SDK-side +producer for such witnesses are intentionally unimplemented here.