ナップサック問題に対する全探索アルゴリズムを実装し、それが最適解を常に返すことを証明する

namespace Knapsack

/-- 0-1ナップサック問題の問題状況 -/
structure Problem where
  /-- 商品の個数 -/
  n : Nat
  /-- 重量制限 -/
  capacity : Nat
  /-- `i` 番目の商品の価値を集めたベクトル -/
  prices : Vector Nat n
  /-- `i` 番目の商品の重さを集めたベクトル -/
  weights : Vector Nat n

/-- ナップサック問題を決定的に解く関数の型。
`Vector Bool p.n` というのは、`i` 番目の商品を選ぶか選ばないかを記録したベクトルである -/
abbrev Solver := (p : Problem) → Vector Bool p.n

/-- 選んだ商品の部分集合の重み合計 -/
def weight (p : Problem) (items : Vector Bool p.n) : Nat :=
  items.map (fun b => if b then 1 else 0)
    |>.zip p.weights
    |>.map (fun (b, w) => b * w)
    |>.foldl (· + ·) 0

/-- 選んだ商品の部分集合の価値合計 -/
def price (p : Problem) (items : Vector Bool p.n) : Nat :=
  items.map (fun b => if b then 1 else 0)
    |>.zip p.prices
    |>.map (fun (b, p) => b * p)
    |>.foldl (· + ·) 0

/-- 選んだ商品の部分集合がナップサックの容量制限を満たすかどうか -/
def feasible (p : Problem) (items : Vector Bool p.n) : Bool :=
  weight p items ≤ p.capacity

end Knapsack

/-
## 全列挙について
-/

/-- リストとして全要素を重複なく列挙する -/
class AsList (α : Type) where
  asList : List α
  /-- 重複がない -/
  noDup : asList.Nodup
  /-- 正しく全列挙になっていることを保証する -/
  complete : ∀ a : α, a ∈ asList

/-- `AsList.asList` を便利に呼び出せるようにするためのラッパー -/
def asList (α : Type) [AsList α] : List α :=
  AsList.asList

instance : AsList Bool where
  asList := [false, true]
  noDup := by decide
  complete := by decide

/-- 長さ `n` のベクトルを、末尾への追加によって再帰的に列挙する。 -/
def vectorAsList [AsList α] : (n : Nat) → List (Vector α n)
  | 0 => [#v[]]
  | n + 1 => (vectorAsList n).flatMap fun xs =>
      (asList α).map xs.push

/-- `vectorAsList` には重複がない。 -/
theorem vectorAsList_noDup [AsList α] (n : Nat) :
    (vectorAsList (α := α) n).Nodup := by
  induction n with
  | zero => simp [vectorAsList]
  | succ n ih =>
    rw [vectorAsList]
    change List.Pairwise (fun x y => x ≠ y) _
    rw [List.pairwise_flatMap]
    constructor
    · intro xs _
      exact AsList.noDup.map xs.push fun a b hab h =>
        hab (Vector.push_eq_push.mp h).1
    · exact ih.imp fun hxy x hx y hy h => by
        obtain ⟨a, _, rfl⟩ := List.mem_map.mp hx
        obtain ⟨b, _, rfl⟩ := List.mem_map.mp hy
        exact hxy (Vector.push_eq_push.mp h).2

/-- `vectorAsList` はすべての長さ `n` のベクトルを含む。 -/
theorem vectorAsList_complete [AsList α] :
    ∀ {n : Nat} (xs : Vector α n), xs ∈ vectorAsList n
  | 0, xs => by
      rw [Vector.eq_empty (xs := xs)]
      simp [vectorAsList]
  | n + 1, xs => by
      obtain ⟨ys, a, rfl⟩ := Vector.exists_push (xs := xs)
      apply List.mem_flatMap.mpr
      refine ⟨ys, vectorAsList_complete ys, ?_⟩
      exact List.mem_map.mpr ⟨a, AsList.complete a, rfl⟩

instance [AsList α] : AsList (Vector α n) where
  asList := vectorAsList n
  noDup := vectorAsList_noDup n
  complete := vectorAsList_complete

/-
## 全探索
-/

/-- 0 だけを並べたベクトルの和は 0。 -/
@[simp] theorem Vector.foldl_add_replicate_zero (n : Nat) :
    (Vector.replicate n 0).foldl (· + ·) 0 = 0 := by
  rw [← Vector.foldl_toList, Vector.toList_replicate]
  induction n with
  | zero => rfl
  | succ n ih => simp [List.replicate_succ, ih]

namespace Knapsack

/-- どの商品も選ばない選択。 -/
def emptyItems (p : Problem) : Vector Bool p.n :=
  Vector.replicate p.n false

/-- どの商品も選ばない選択の総重量は 0。 -/
@[simp] theorem weight_emptyItems (p : Problem) :
    weight p (emptyItems p) = 0 := by
  simp only [weight, emptyItems, Vector.map_replicate]
  simp
  have allZero :
      ((Vector.replicate p.n 0).zip p.weights).map (fun (b, w) => b * w) =
        Vector.replicate p.n 0 := by
    apply Vector.ext
    intro i hi
    simp
  rw [allZero, Vector.foldl_add_replicate_zero]

/-- どの商品も選ばなければ容量制限を必ず満たす。 -/
@[simp] theorem feasible_emptyItems (p : Problem) :
    feasible p (emptyItems p) = true := by
  simp [feasible]

/-- 全列挙された選択肢のうち、容量制限を満たすもの。 -/
def feasibleItems (p : Problem) : List (Vector Bool p.n) :=
  (asList (Vector Bool p.n)).filter (feasible p)

/-- `feasibleItems` への所属は、容量制限を満たすことと同値。 -/
theorem mem_feasibleItems_iff {p : Problem} {items : Vector Bool p.n} :
    items ∈ feasibleItems p ↔ feasible p items = true := by
  constructor
  · exact fun h => (List.mem_filter.mp h).2
  · exact fun h => List.mem_filter.mpr ⟨AsList.complete _, h⟩

/-- `feasibleItems` は、少なくとも `emptyItems` を含む。 -/
theorem feasibleItems_ne_nil (p : Problem) : feasibleItems p ≠ [] := by
  apply List.ne_nil_of_mem (a := emptyItems p)
  exact List.mem_filter.mpr ⟨AsList.complete _, feasible_emptyItems p⟩

/-- アイテム数を`n`として`2^n`個の要素をすべて列挙して
最適解を求める全探索アルゴリズム -/
def bruteForce (p : Problem) : Vector Bool p.n :=
  (feasibleItems p).maxOn (price p) (feasibleItems_ne_nil p)

/-- 解が feasible であり、他のどの feasible な解よりも価値が低くないこと。 -/
def IsOptimal (p : Problem) (solution : Vector Bool p.n) : Prop :=
  feasible p solution = true ∧
    ∀ other : Vector Bool p.n,
      feasible p other = true → price p other ≤ price p solution

/-- `bruteForce` が返す解は、列挙された feasible な解の一つ。 -/
theorem bruteForce_mem_feasibleItems (p : Problem) :
    bruteForce p ∈ feasibleItems p := by
  simp [bruteForce]

/-- `bruteForce` が返す解は容量制限を満たす。 -/
theorem bruteForce_feasible (p : Problem) :
    feasible p (bruteForce p) = true :=
  mem_feasibleItems_iff.mp (bruteForce_mem_feasibleItems p)

/-- 任意の feasible な解の価値は、`bruteForce` が返す解の価値以下。 -/
theorem price_le_bruteForce (p : Problem) (other : Vector Bool p.n)
    (h : feasible p other = true) :
    price p other ≤ price p (bruteForce p) := by
  have hmem : other ∈ feasibleItems p := mem_feasibleItems_iff.mpr h
  simpa [bruteForce] using
    (List.le_apply_maxOn_of_mem (f := price p) hmem)

/-- 全探索アルゴリズム `bruteForce` は最適解を返す。 -/
theorem bruteForce_optimal (p : Problem) : IsOptimal p (bruteForce p) :=
  ⟨bruteForce_feasible p, price_le_bruteForce p⟩

end Knapsack

/- ## 具体的な問題を解いてみる -/

#eval
  /- [https://www.msi.co.jp/solution/nuopt/docs/examples/html/02-05-00.html] において紹介されている例題 -/
  let problem : Knapsack.Problem := {
    n := 6
    capacity := 65
    prices := #v[120, 130, 80, 100, 250, 185]
    weights := #v[10, 12, 7, 9, 21, 16]
  }
  let solution := Knapsack.bruteForce problem
  IO.println s!"最適解: {solution.toArray}"

/- ## ここからが本番

* よくあるDPによる解法を実装する
* DP による解法が常に最適解を返すことを証明する！
* 分子限定法もできればやる
-/

Start with the Lean code block in issue #2597 and run the existing #eval example to understand the current brute-force result. The requested work is to add a dynamic-programming solver and prove that it always returns an optimal solution; branch-and-bound is explicitly optional. Done means the implementation and its correctness proof compile.