Agent Skills¶
FLARE utilizes two Agent Skills for auto-formalization of the MILPFormulation (see definition) and automated formal proof synthesis (AFPS) of MILPReformulation (see definition). Both skills include a SKILL.md and a Lean template template.lean with detailed scaffolding instructions.
lean-milp-formulation¶
Standard structure and conventions for a Lean file defining a MILP formulation MILPFormulation.
assets/skills/lean-milp-formulation/SKILL.md
---
name: lean-milp-formulation
description: >
Standard for the structure and conventions of Lean 4 MILP formulation files.
Use when authoring a new formulation file, reviewing an existing one, or
modifying one.
---
# Lean MILP Formulation Standard
A MILP formulation file encodes a single mixed-integer linear program as a
`MILPFormulation` value built from four pieces: a `Params` structure for
problem data, a `Vars` structure for decision variables, a `Feasible`
predicate for constraints, and an `obj` function for the objective.
## File structure
Every formulation file contains, in order:
1. Imports (always includes the common MILP definitions module that provides
`MILPFormulation`, and any targeted Mathlib imports needed by the file).
2. `open BigOperators Finset` if the file uses `∑` or `Finset`.
3. A `namespace` scoped to the formulation (e.g. `P1.a`).
4. `structure Params` — problem data and assumptions on the data.
5. `structure Vars (p : Params)` — decision variables.
6. `structure Feasible (p : Params) (v : Vars p) : Prop` — constraints.
7. `def obj (p : Params) (v : Vars p) : ℝ` — objective (always ℝ-valued).
8. `def formulation : MILPFormulation` — bundles the above.
9. `end <namespace>`.
See `template.lean` for the canonical layout.
## Type encoding
Use `ℝ` universally for continuous quantities and `ℤ` universally for integer
quantities. This applies uniformly to parameters and variables. The only `ℕ`
in a formulation is for problem _dimensions_ (sizes used to build `Fin`).
| Concept | Lean encoding |
| ----------------------------- | --------------------------------------------------------- |
| Problem dimension | `ℕ` field of `Params` |
| Index set tied to a dimension | `Fin <dim>` where `<dim>` is a prior `Params` field |
| Continuous (scalar) | `ℝ` |
| Continuous vector `b[i]` | `b : Fin <dim> → ℝ` |
| Continuous matrix `A[i][j]` | `A : Fin <dim1> → Fin <dim2> → ℝ` |
| Integer (scalar) | `ℤ` |
| Integer vector | `Fin <dim> → ℤ` |
| Binary | `ℤ` with `h<name>_bin : ∀ …, <name> … = 0 ∨ <name> … = 1` |
| Non-negative | `h<name>_nn : ∀ …, 0 ≤ <name> …` |
| Summation `∑` | `∑ i : Fin p.<dim>, …` with `open BigOperators` |
## Formulation Modeling Rules
### No type-level parameters on `Params`
`Params` itself is a plain (parameter-less) structure. Problem dimensions
are fields of `Params`, not type-level arguments to `Params`. This allows
proving a formulation with different dimension variables is a reformulation.
`Vars`, `Feasible`, and `obj` _are_ parameterized — by `p : Params` (and,
for `Feasible` and `obj`, also by `v : Vars p`). Vector decision
variables are typed `Fin p.<dim> → ℤ` / `Fin p.<dim> → ℝ` directly.
### `NeZero` on dimensions
When a dimension must be nonzero for the formulation to make sense, add an
assumption field `hNumFoo : NeZero NumFoo` in the `Params` implicit
assumptions section. Do NOT attach `[NeZero n]` to any structure
(`Params`, `Vars`, `Feasible`) — there are no type-level dimensions.
### Graph topology
For network problems with `nA : ℕ` arcs and `nN : ℕ` nodes (both `Params`
fields), represent graph structure as functions rather than `Finset` edge
lists when possible:
```lean
tail : Fin nA → Fin nN -- arc tail node
head : Fin nA → Fin nN -- arc head node
```
Use `Finset.univ.filter` to express flow conservation at specific nodes:
```lean
(univ.filter (fun e => p.tail e = i)).sum (fun e => v.x e k) = …
```
### Big-M is forbidden
**Never introduce a big-M constant in a Lean formulation, even if the
source description does.** Big-M is a solver linearization technique; it is not
required in Lean. Instead, rewrite big-M constraints as disjunctions or
conditional equalities on the underlying variables.
**How to rewrite.** The following patterns are examples of big-M patterns in
source MILP formulations and how they should be rewritten in Lean. Another
indicator of big-M is the presence of a parameter named `M` or `bigM` in the
source, or a description of a "sufficiently large constant" in the assumptions.
| Source MILP | Lean `Feasible` field |
| -------------------------------------------------- | --------------------------- |
| `x ≤ M · y` (binary `y`, `x ≥ 0`) | `hlink : v.x = 0 ∨ v.y = 1` |
| `A ≤ B + M·(1 − y)` and `C ≤ D + M·y` (binary `y`) | `hdisj : A ≤ B ∨ C ≤ D` |
**After rewriting:**
- The big-M parameter (`M`) and its `_pos`/`_nn` assumption MUST NOT appear
in `Params`.
- Binary indicator variables that exist _solely_ to linearize the
disjunction (the `y` in `x ≤ M·y` when `y` has no other role) MUST NOT
appear in `Vars`. Indicators with independent semantics (e.g. `y_j`
meaning "warehouse `j` is open" with its own opening cost in `obj`)
stay, but the `M·y` constraint is still rewritten as a disjunction.
## Naming Conventions
- `Params` fields: use the parameter name exactly as it appears in the source.
- `Vars` fields: use the variable name exactly as it appears in the source.
- `Feasible` fields: `h` + short camel-case constraint name — `hassign`,
`hcap`, `hbal`, `hprec`, `hoverlap`, `hmtz`, `hflow`, `hdemand`.
- Bound-style suffixes on assumptions and constraints: `_nn` (non-negative),
`_pos` (positive), `_bin` (binary), `_lo`, `_hi`.
## Formatting Rules
- Single space between a field name and `:`. Do NOT pad field names to
force column alignment.
- Do NOT wrap inline comments in parentheses (write `-- arc cost`, not
`-- (arc cost)`).
- If a type is too long to fit on one line with a comment, place the comment
after the field name on the same line and the type on the next line,
indented 2 spaces.
- A comment line precedes each constraint or group of like constraints
with a short description. Sign constraints (non-negativity, positivity)
do not require a comment.
## Type casting
Decision variables in `Vars` are `ℤ` while `Params` fields and the `obj`
return type are `ℝ`. Lean inserts `ℤ → ℝ` coercions automatically, but
always write them explicitly.
- **In `obj`**: cast the first `ℤ` operand with ascription syntax
`(v.field : ℝ)`; Lean unifies the rest.
```lean
def obj (_ : Params) (v : Vars _) : ℝ := (v.s : ℝ) + v.r
```
- **In `Feasible` constraints**: cast each `ℤ` variable that appears
alongside `ℝ` parameters in an arithmetic expression.
```lean
hpeople : p.A * (v.s : ℝ) + p.K * v.r ≤ p.U
```
- **Be consistent within a file.** Do not mix explicit and implicit casts
across constraints in the same `Feasible` block. If one constraint casts
`v.s` explicitly, all constraints must.
## Common pitfalls
- **Implicit ℤ→ℝ casts in `obj` and `Feasible`.** Lean coerces silently,
but the cast must always be written explicitly using `(v.field : ℝ)`.
Inconsistent casts (explicit in one constraint, implicit in another) make
reformulation proofs harder to follow and can cause `exact h.hconstraint`
to fail when the elaborated type does not match the goal.
- **Type-level dimensions on `Params`.** Do NOT write
`structure Params (n : ℕ)` or `def formulation (n : ℕ) [NeZero n] : …`.
`Params` is parameter-less; dimensions are `ℕ` fields of `Params`.
- **`ℕ →` in `Vars` for vector variables.** Vector decision variables
should be typed `Fin p.<dim> → ℤ` / `Fin p.<dim> → ℝ`, not `ℕ → ℤ` /
`ℕ → ℝ`. Since `Vars` takes `p : Params`, it has access to dimensions.
- **`[NeZero]` attached to a structure.** Nonzero-ness of a dimension is
an _assumption field_ inside `Params`: `hNumFoo : NeZero NumFoo`. Do
NOT write `[NeZero n]` anywhere.
- **Binary via `Bool` or `Fin 2`.** Use `ℤ` with an explicit
`h<name>_bin : … = 0 ∨ … = 1` constraint (in `Feasible` for variables, in
the `Params` assumptions for parameters).
- **Objective not in ℝ.** Even when all data and vars are integer, cast to
ℝ in `obj`. `MILPFormulation.obj` is ℝ-valued. For maximization,
negate: `- (∑ …)`.
- **Padding field names.** Single space before `:`, always.
- **Parenthesized inline comments.** Use `-- arc cost`, not `-- (arc cost)`.
- **Missing implicit assumptions.** If a formulation needs a property to prove
it is a valid reformulation (e.g. non-self-loops, triangle inequality), mark it
explicitly in the `-- Implicit Assumptions` section rather than
assuming it silently.
assets/skills/lean-milp-formulation/template.lean
/-
NOTE: Add necessary imports at the top of the file.
Always include the project's common MILP definitions module:
import Common
Use targeted imports, NOT `import Mathlib`.
For files with only ℝ/ℤ (no BigOperators):
import Mathlib.Data.Real.Basic
For files with BigOperators + ∑ over Fin p.<dim> (like this template):
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Int.Basic
If constraints use Fin p.<dim1> × Fin p.<dim2> (pair-indexed variables),
also add:
import Mathlib.Data.Fintype.Prod
-/
import Common
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Int.Basic
-- NOTE: Always include `open BigOperators Finset` when using ∑ and Finsets.
open BigOperators Finset
/-
NOTE: Open a namespace that uniquely identifies this formulation.
Use `<Problem>.<formulation>`, e.g. `P1.a` for problem p1 formulation a.
-/
namespace P1.a
/-
NOTE: Include any definitions used in constructing `Params`, `Vars`, `Feasible`,
or `obj` here. These must be included *within* the namespace to avoid polluting
the global namespace with duplicate definitions across formulations.
-/
/-
NOTE: Params structure — problem dimensions, data, and assumptions.
- `Params` is a plain (parameter-less) structure. Do NOT write
`structure Params (n : ℕ)` or attach any `[NeZero …]` to it.
- Dimensions come first as `ℕ` fields. Later data fields reference them.
- Data fields follow: vectors `Fin <dim> → <ℝ|ℤ>`, matrices
`Fin <dim1> → Fin <dim2> → <ℝ|ℤ>`, scalars `<ℝ|ℤ>`.
- In `Params`, indexed data MUST use `Fin <dim>` for every index, never `ℕ`.
- If an index range itself depends on a prior parameter (e.g. each item
`a` in set `A` has different set size `n_B a`) — use a *dependent*
function type, not flat `ℕ → ℕ`:
n_B : Fin n_A → ℕ
x : (a : Fin n_A) → Fin (n_B a) → ℤ
Do NOT collapse these to `ℕ → ℕ` or `ℕ → ℕ → ℝ`.
- Each parameter has an inline comment with a short description.
- Single space before `:`; do NOT pad field names for column alignment.
- Do NOT wrap inline comments in parentheses (write `-- arc cost`, not
`-- (arc cost)`).
- Assumptions go at the end under an `-- Assumptions` comment.
- Separate explicitly stated assumptions from implicit ones (e.g. non-negativity)
by placing implicit assumptions under an `-- ImplicitAssumptions` comment.
- The `-- Assumptions` and `-- ImplicitAssumptions` sections are both optional;
if there are no assumptions of that type, omit the section entirely.
- For `NeZero` assumptions on dimensions, use `h<DimName> : NeZero <DimField>`.
- Use `_nn`, `_pos`, `_bin` suffixes where applicable. Sign assumptions
do not require an inline comment.
-/
structure Params where
NumExperiments : ℕ -- number of experiments
NumResources : ℕ -- number of resource types
ElectricityProduced : Fin NumExperiments → ℝ -- electricity produced by experiment i
ResourceRequired : Fin NumResources → Fin NumExperiments → ℝ -- resource j required by experiment i
ResourceAvailable : Fin NumResources → ℝ -- amount of resource j available
-- Assumptions
hNumExperiments : NeZero NumExperiments
hNumResources : NeZero NumResources
-- Implicit Assumptions
hElectricityProduced_nn : ∀ i, 0 ≤ ElectricityProduced i
hResourceRequired_nn : ∀ j i, 0 ≤ ResourceRequired j i
hResourceAvailable_nn : ∀ j, 0 ≤ ResourceAvailable j
/-
NOTE: Vars structure — decision variables.
- `Vars` is parameterized by `p : Params`. Write `structure Vars (p : Params)`.
- Scalar variables: `ℤ` or `ℝ`.
- Vector variables: `Fin p.<dim> → ℤ` or `Fin p.<dim> → ℝ`. `Vars` has
access to `p`, so use the real index range — do NOT use `ℕ → ℤ`.
- Binary-ness is enforced in `Feasible`, not in the type.
- Each variable has an inline comment with a short description.
- Single space before `:`; do NOT pad field names for column alignment.
- `Vars` contains no assumptions; assumptions involving variables go in `Feasible`.
-/
structure Vars (p : Params) where
ConductExperiment : Fin p.NumExperiments → ℤ -- number of times each experiment is conducted
/-
NOTE: Feasible structure — constraints.
- Signature is exactly `(p : Params) (v : Vars p) : Prop`. No other args.
- If `Vars` contains fields with names `p` or `v`, that is fine; they will be
accessed unambiguously as `v.<field>` or `p.<field>`.
- One `--` comment line precedes each constraint or group of like
constraints. Sign constraints do not need a comment.
- Use `_nn`, `_pos`, `_bin`, `_lo`, `_hi` suffixes where applicable.
- Group implicit constraints at the end under `-- [Implicit Constraints]`.
-/
structure Feasible (p : Params) (v : Vars p) : Prop where
-- For each resource, total requirement across all experiments is within supply
hres : ∀ j : Fin p.NumResources,
∑ i : Fin p.NumExperiments, p.ResourceRequired j i * (v.ConductExperiment i : ℝ)
≤ p.ResourceAvailable j
hConductExperiment_nn : ∀ i : Fin p.NumExperiments, 0 ≤ v.ConductExperiment i
/-
NOTE: Objective — always ℝ-valued, named `obj`.
- Signature is exactly `(p : Params) (v : Vars p) : ℝ`.
- Define the equation on the second line for readability.
- Precede with a one-line `--` comment stating direction and what is
optimized. For maximization, negate the sum (MILPFormulation expects
minimization-style objectives as ℝ values).
-/
-- Maximize total electricity produced
def obj (p : Params) (v : Vars p) : ℝ :=
-(∑ i : Fin p.NumExperiments, p.ElectricityProduced i * (v.ConductExperiment i : ℝ))
/-
NOTE: Include EXACTLY as formatted below, with the padded alignment and spacing.
-/
def formulation : MILPFormulation where
Params := Params
Vars := Vars
feasible := Feasible
obj := obj
-- NOTE: End the namespace at the end of the file
end P1.a
lean-milp-reformulation¶
Standard structure and conventions for a Lean file containing a constructive reformulation proof MILPReformulation.
assets/skills/lean-milp-reformulation/SKILL.md
---
name: lean-milp-reformulation
description: >
Standard for the structure and conventions of Lean 4 MILP reformulation files.
Use when authoring a new reformulation file, reviewing an existing one, or
modifying one.
---
# Lean MILP Reformulation Standard
A reformulation proof file shows that two MILP formulations `A` and `B` are
related under the project's `MILPReformulation` structure: it produces a
parameter map `A.Params → B.Params`, mutually inverse feasibility-preserving
variable maps, and a strictly monotone objective map that makes forward and
backward objective diagrams commute.
## `MILPReformulation` at a glance
The project's common MILP module defines `MILPReformulation F G` with fields:
- `paramMap : F.Params → G.Params`
- `fwd : (p : F.Params) → F.Vars p → G.Vars (paramMap p)`
- `bwd : (p : F.Params) → G.Vars (paramMap p) → F.Vars p`
- `fwd_feas : ∀ p x, F.feasible p x → G.feasible (paramMap p) (fwd p x)`
- `bwd_feas : ∀ p x', G.feasible (paramMap p) x' → F.feasible p (bwd p x')`
- `objMap : ℝ → ℝ`
- `objMap_mono : StrictMono objMap`
- `fwd_obj : ∀ p x, F.feasible p x → G.obj (paramMap p) (fwd p x) = objMap (F.obj p x)`
- `bwd_obj : ∀ p x', G.feasible (paramMap p) x' → G.obj (paramMap p) x' = objMap (F.obj p (bwd p x'))`
The semantic requirement is **pointwise**: feasibility and objective
preservation for _all_ feasible solutions — not merely equal optima.
## File structure
Every reformulation file contains, in order:
1. Imports: the common MILP module (providing `MILPReformulation`), both
formulations `A` and `B`, and targeted Mathlib imports.
2. `open BigOperators Finset` if the proofs use `∑` or `Finset`.
3. A `namespace` matching the shared problem scope (e.g. `P1`, `General.TSP`).
4. Optional helper-lemma section (lemmas local to this reformulation).
5. Optional `paramMap` definition (inline in the structure if trivial).
6. Optional forward-helpers section + `fwd` and `fwd_feas`.
7. Optional backward-helpers section + `bwd` and `bwd_feas`.
8. Optional objective-mapping section + `objMap`, `objMap_mono`, and
`fwd_obj` / `bwd_obj`.
9. The final `MILPReformulation` `def`.
10. `end <namespace>`.
See `template.lean` for the canonical layout.
## Naming conventions
- Reformulation `def` name: camelCase, `<formA><FormB>Reformulation`
(e.g. `aBReformulation`, `scfMcfReformulation`). The first letter is
lowercase and the second formulation letter is uppercase. Match the file name.
- Helper defs/lemmas: `private`. All helpers live in the reformulation file
itself — there is no shared-lemmas module.
- Canonical names: `paramMap`, `fwd`, `bwd`, `fwd_feas`, `bwd_feas`,
`objMap`, `objMap_mono`, `fwd_obj`, `bwd_obj`.
## When to inline vs. extract
Each of `paramMap`, `fwd`/`fwd_feas`, `bwd`/`bwd_feas`, and the objective
mapping has a dedicated optional section. Use these rules:
- **Inline in the `MILPReformulation` structure** when the body is a single line or
a trivial expression. Examples: `paramMap := id` (but see the pitfall
below), `paramMap p := { c := p.c }`, `fwd _ v := { a := v.x }`,
`fwd_obj _ _ _ := rfl`, `objMap := id`,
`objMap_mono := strictMono_id`.
- **Extract to a `private def`/`lemma` above the structure** when the body
is multi-line or the proof is non-trivial.
- Do NOT leave empty section headers. If a section is not needed, remove
the header along with its contents.
## Helper sections (`ForwardHelpers` / `BackwardHelpers`)
Only include a `section ForwardHelpers` (resp. `BackwardHelpers`) block
when there are `private` helper lemmas or definitions that depend on a
feasible solution. Inside:
- Introduce `Params` and `Vars` as **implicit** parameters (e.g.
`{p : <A>.Params} {v : <A>.Vars p}`). `Vars` is parameterized by `p`,
so the `v` binder must reference it. Do NOT introduce any separate
dimension parameters — dimensions live as fields of `p`.
- Introduce the feasibility hypothesis as an **explicit** parameter `h`,
then `include h` so Lean uses it.
## Reformulation files are self-contained
Every reformulation file contains all of its own helper lemmas and
definitions. Reformulation files do not import each other, and there is no
shared-lemmas module. If two reformulation files need the same lemma,
duplicate it (each as `private`) rather than introducing a shared module.
## Stray-content rules
- No additional `/-! … -/` doc-comment blocks after the module header.
Proof reasoning goes in tactic-line `-- …` comments inside the proof
body.
- No leftover `sorry` in a finalized file.
- No leftover `/- NOTE … -/` template comments.
- No empty section headers — delete the header along with the contents.
## Common pitfalls
These patterns cause the most wasted iterations; check each one before
finalizing a file.
### `paramMap := id` when namespaces differ
`A.Params` and `B.Params` from different namespaces are **distinct types**
even when structurally identical. `id` will not typecheck. Always write an
explicit field-by-field `paramMap`, even when it looks trivial:
```lean
paramMap p := { c := p.c, d := p.d }
```
### Claim strength mismatch
`MILPReformulation` is pointwise. If the source claims only "same optimal value",
the hard direction may be intractable under `MILPReformulation`. Identify this up
front and decide whether to leave `sorry`, restrict the claim, or change
formulations.
### `|>.field` in type positions
`|>.` pipe-chained accessor notation is **invalid in Lean 4 type
annotations** (lemma return types, `show` targets). Use explicit
parenthesization:
```lean
-- WRONG (parse error):
… : <A>.formulation |>.obj (paramMap p) (fwd p v) = … := by
-- CORRECT:
… : (<A>.formulation).obj (paramMap p) (fwd p v) = … := by
```
### Cast across sums
`↑(∑ i, f i)` is **not definitionally equal** to `∑ i, ↑(f i)`; `show` and
`rfl` both fail. Use `push_cast`, `simp_rw [Int.cast_sum]`, or
`Finset.cast_sum`:
```lean
-- FAILS:
show ↑(∑ j, v.y i j) = ↑(v.y i)
-- WORKS:
simp_rw [Int.cast_sum] -- or push_cast; ring
```
### Dimension nonzero-ness comes from `Params`
Dimensions are `Params` fields (`NumFoo : ℕ`) and their non-emptiness is
an assumption field (`hNumFoo : NeZero NumFoo`). To use `Fintype`
instances on `Fin p.NumFoo` inside a helper, bring the `NeZero` into
scope from the feasibility / params hypothesis — e.g. `haveI := p.hNumFoo`.
Do NOT reintroduce dimensions as standalone `{n : ℕ} [NeZero n]` binders
in helper lemmas.
### `linarith` across cast boundaries
When `linarith` must reason across `ℤ → ℝ` or `ℕ → ℤ`, it often fails.
Break the chain with explicit `have` steps using `norm_cast` / `push_cast`
before handing to `linarith`.
### Cast notation in proofs: prefer `↑`
In tactic proofs, use the coercion arrow `↑v.field` rather than the
ascription form `(v.field : ℝ)`. Both desugar to `Int.cast v.field`, but
`↑` is conventional in proof scripts and matches what `push_cast` /
`norm_cast` produce in the goal state, making it easier to read the goal
and the proof side by side.
```lean
-- In a tactic proof:
show ↑v.s + ↑v.r = ↑(v.s + v.r)
push_cast; ring
```
Use `(v.field : ℝ)` only in term-mode expressions such as `fwd` / `bwd`
definitions or `show` targets where the target type must be stated explicitly.
### `rewrite` interaction with `if`
`rw [eq]` that substitutes inside the condition of an `if h_cond then …`
changes `h_cond`, so a later `rw` looking for the original pattern fails.
Scope such rewrites to specific subgoals.
### `noncomputable` for structure extraction
Mark `fwd` / `bwd` / the whole section `noncomputable` when a direction
uses `Classical.choice` or extracts structure (tour order, permutation)
from a feasible solution. Prefer deterministic selections (e.g. minimum
index via `LinearOrder` on `Fin n`) when possible — cleaner and avoids
`noncomputable`.
assets/skills/lean-milp-reformulation/template.lean
/-
NOTE: Imports go at the very top.
Always include the project's common MILP definitions module:
import Common
Import both formulation modules being compared. The exact import paths
depend on where the formulation files live in the project.
Use targeted Mathlib imports, NOT `import Mathlib`. Common options:
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Int.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic
-/
import Common
import <FormulationModuleA>
import <FormulationModuleB>
/-
NOTE: Add `open BigOperators Finset` only if the feasibility proofs use ∑ or Finsets.
-/
open BigOperators Finset
/-
NOTE: Open a namespace corresponding to the shared problem scope.
e.g., `P1` for problem p1.
-/
namespace <Problem>
-- ============================================================================
-- § Helper Lemmas
-- ============================================================================
/-
NOTE: This section is *optional*. Include only general lemmas that have no
dependency on any specific feasible solution.
- Use the `lemma` keyword.
- Mark as `private`. Every helper lemma lives in this reformulation file;
reformulation files do not import each other and there is no shared-lemmas
module. If another reformulation file needs the same lemma, duplicate it.
- Lemmas specific to a particular formulation that are needed by fwd_feas or
bwd_feas belong in ForwardHelpers / BackwardHelpers sections below.
- Remove this section entirely if no such lemmas are needed.
-/
-- ============================================================================
-- § Parameter Mapping
-- ============================================================================
/-
NOTE: This section is *optional*. Include only if the paramMap body is longer
than a single line. If the mapping is trivial (e.g., `id`, `{ c := p.c }`),
put it inline in the reformulation structure instead.
- Use `private def paramMap`.
-/
private def paramMap (p : <A>.Params) : <B>.Params :=
{ ... }
-- ============================================================================
-- § Forward Mapping and Feasibility
-- ============================================================================
/-
NOTE: This section is *optional*. Include only if `fwd` or `fwd_feas` are longer
than a single line. Otherwise, put them inline in the reformulation structure.
- Use `private def fwd` and `private lemma fwd_feas`.
- Mark `noncomputable` when the construction uses Classical.choice. If the
majority of the construction requires `noncomputable`, mark the entire section
as `noncomputable` instead.
-/
/-
NOTE: The ForwardHelpers section is *optional*. Include it when there are private
helper lemmas or definitions needed by `fwd_feas` that depend on a feasible
solution from formulation <A>. Remove the section entirely if not needed.
-/
section ForwardHelpers
/-
NOTE: Use `variable` to automatically add parameters for convenience.
- Introduce `Params` and `Vars` as *implicit* parameters.
- Introduce the feasibility hypothesis as an *explicit* parameter (h)
- Explicitly `include h` to avoid issues with Lean inferring the variable
-/
variable {p : <A>.Params} {v : <A>.Vars p} (h : <A>.Feasible p v)
include h
-- Private helper lemmas and definitions depending on h go here.
end ForwardHelpers
/--
**<A> → <B>**: {Brief informal description of the forward map construction}
-/
private def fwd (p : <A>.Params) (v : <A>.Vars p) : <B>.Vars (paramMap p) :=
{ ... }
private lemma fwd_feas (p : <A>.Params) (v : <A>.Vars p)
(h : <A>.Feasible p v) :
<B>.Feasible (paramMap p) (fwd p v) := by
sorry
-- ============================================================================
-- § Backward Mapping and Feasibility
-- ============================================================================
/-
NOTE: This section is *optional*. Include only if `bwd` or `bwd_feas` are longer
than a single line. Otherwise, put them inline in the reformulation structure.
- Use `private def bwd` and `private lemma bwd_feas`.
- Mark `noncomputable` when the construction uses Classical.choice or extracts
structure from the solution (e.g., tour order, permutation).
-/
/-
NOTE: The BackwardHelpers section is *optional*. Include it when there are private
helper lemmas or definitions needed by `bwd_feas` that depend on a feasible
solution from formulation <B>. Remove the section entirely if not needed.
-/
section BackwardHelpers
/-
NOTE: Use `variable` to automatically add parameters for convenience.
- Introduce `Params` and `Vars` as *implicit* parameters.
- Introduce the feasibility hypothesis as an *explicit* parameter (h)
- Explicitly `include h` to avoid issues with Lean inferring the variable
-/
variable {p : <A>.Params} {v : <B>.Vars (paramMap p)}
(h : <B>.Feasible (paramMap p) v)
include h
-- Private helper lemmas and definitions depending on h go here.
end BackwardHelpers
/--
**<B> → <A>**: {Brief informal description of the backward map construction}
-/
private def bwd (p : <A>.Params) (v : <B>.Vars (paramMap p)) : <A>.Vars p :=
{ ... }
private lemma bwd_feas (p : <A>.Params) (v : <B>.Vars (paramMap p))
(h : <B>.Feasible (paramMap p) v) :
<A>.Feasible p (bwd p v) := by
sorry
-- ============================================================================
-- § Objective Mapping
-- ============================================================================
/-
NOTE: This section is *optional*. Include only if the objective map is not a
single inline expression. If `objMap = id` or a simple lambda (e.g., `fun v => 2 * v`),
put it inline in the reformulation structure instead.
When the section is needed, define:
- `private def objMap : ℝ → ℝ := ...`
- `private lemma objMap_mono : StrictMono objMap := ...`
- `private lemma fwd_obj ...` and `private lemma bwd_obj ...` if the objective
commutativity proofs are non-trivial (not just `rfl`).
-/
private def objMap : ℝ → ℝ := fun v => ...
private lemma objMap_mono : StrictMono objMap := by
sorry
private lemma fwd_obj (p : <A>.Params) (v : <A>.Vars p)
(h : <A>.Feasible p v) :
<B>.obj (paramMap p) (fwd p v) = objMap (<A>.obj p v) := by
sorry
private lemma bwd_obj (p : <A>.Params) (v : <B>.Vars (paramMap p))
(h : <B>.Feasible (paramMap p) v) :
<B>.obj (paramMap p) v = objMap (<A>.obj p (bwd p v)) := by
sorry
-- ============================================================================
-- § Reformulation Structure
-- ============================================================================
/-
NOTE: The final def should be a `MILPReformulation` structure:
- See the project's common MILP module for the definition of `MILPReformulation`
and its fields.
- Named camelCase: <formA><FormB>Reformulation (e.g., `aBReformulation`, `scfMcfReformulation`)
- Marked `noncomputable` if any helper def is noncomputable
- `paramMap`: reference the private def above, or inline for trivial cases
e.g., `paramMap p := { c := p.c }` or `paramMap := id`
- `fwd` / `bwd`: reference the private defs above, or inline for trivial cases
e.g., `fwd _ v := { a := v.numTop, g := v.numFront }`
- `fwd_feas` / `bwd_feas`: reference the private lemmas above
- `objMap`: use `id` when both objectives are identical; reference the private
def above when the Objective Mapping section is present
- `objMap_mono`: use `strictMono_id` when `objMap = id`; reference the
private lemma above when the Objective Mapping section is present
- `fwd_obj` / `bwd_obj`: use `_ _ _ := rfl` when `objMap = id` and objectives
are definitionally equal; reference private lemmas when the section is present
-/
def <formA><FormB>Reformulation : MILPReformulation <A>.formulation <B>.formulation where
paramMap := paramMap
fwd := fwd
bwd := bwd
fwd_feas := fwd_feas
bwd_feas := bwd_feas
objMap := id
objMap_mono := strictMono_id
fwd_obj _ _ _ := rfl
bwd_obj _ _ _ := rfl
end <Problem>