Optimal solutions exist for discrete problems

Stream: new members

[Asei Inoue]

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr

/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Bool :=
  items.weight <= P.capacity

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  sorry

[Asei Inoue]

I am always grateful to those who answer my questions on Zulip. :pray:

I have defined the Knapsack problem as described above. However, I am having trouble proving an optimal solution exists. How can I fill in the above sorry?

[Asei Inoue]

The existence of an optimal solution is obviously not a fact specific to the Knapsack problem. Would it be easier to define a more general 'discrete problem' and show for it...?

[Adomas Baliuka]

Isn't the theorem false? You didn't specify what Items are available so I can always have an item of weight 0 with arbitrary price. Put that in an ItemList and you get arbitrarily high-price knapsacks.

[Adomas Baliuka]

In fact,

open ItemList in
theorem not_exist_optimal (P : Problem) : ¬∃ items : ItemList, items.optimal P := by
  simp
  intro itl
  simp [optimal, feasible]
  intro _incap
  use [{weight:=0, price:=itl.price + 1 : Item}]
  simp [weight, price]

[Asei Inoue]

@Adomas Baliuka Thanks. I was careless ...

[Asei Inoue]

It seems that I have to edit the definition of feasible.

But if I add items ⊆ P.items to the definition of ItemList.feasible, fun items : ItemList ↦ items.feasible P would not work.
It is not immediately clear how to fix it.

[Adomas Baliuka]

I don't understand what "would not work". What do you want this hypothetical fun items to do?

[Asei Inoue]

@Adomas Baliuka
Oh sorry... My whole code is here:

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr

/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Prop :=
  items ⊆ P.items ∧ items.weight <= P.capacity

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  sorry

/-!
  ## Examples for Test
  --------------------
-/

def problem1 : Problem := {
    items := [Item.mk 1 2, Item.mk 2 1, Item.mk 3 4]
    capacity := 5
  }

#eval problem1.items

def sol1 : ItemList := [Item.mk 1 2]

#eval sol1.price

/-!
  ## Algorithm to Solve Knapsack Problem
  --------------------------------------
-/

variable (α β : Type) [LinearOrder β]

def brute (P : Problem) : ItemList :=
  let sublists := P.items.sublists
  let feasible_solutions := sublists.filter (fun items : ItemList ↦ items.feasible P)   -- error
  let max_list := argmax ItemList.price feasible_solutions
  match max_list with
  | none => []
  | some opt => opt

#eval brute problem1

[Asei Inoue]

What do you want this hypothetical fun items to do?

I want to use feasible to filter items, but the function must return a Bool type instead of a Prop type.

[Asei Inoue]

However, if items ⊆ P.items is included in the definition, it will be of type Prop.

[Adomas Baliuka]

You cannot compute with Prop anyway. Use Bool instead. I would separate the conditions "within capacity" (Bool so you can use it inside brute) and "optimal" still has to be Prop because you use a quantifier.

[Yaël Dillies]

Certainly you can compute with Prop. You just need to provide a Decidable instance.

[Adomas Baliuka]

I wrote a Decidable instance, seems to work:

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr, DecidableEq -- added this to make instance work !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr, DecidableEq -- added this too (probably won't ever get used) !!!!!!!!!!!!!!!!



/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Prop :=
  items ⊆ P.items ∧ items.weight <= P.capacity

open ItemList in
instance instDecidableFeasible (items : ItemList) (P : Problem)
  : Decidable (ItemList.feasible items P) := by
    simp [feasible, weight]
    infer_instance

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price


open ItemList in
theorem exist_optimal (P : Problem) (nonem : P.items ≠ []) : ∃ items : ItemList, items.optimal P := by
  sorry
-- something like this might help, although I also haven't proved it yet...
#check Finset.exists_maximal

/-!
  ## Examples for Test
  --------------------
-/

def problem1 : Problem := {
    items := [⟨1, 2⟩, ⟨2, 1⟩, ⟨3, 4⟩]
    capacity := 5
  }

#eval problem1.items

def sol1 : ItemList := [⟨1, 2⟩]

#eval sol1.price

/-!
  ## Algorithm to Solve Knapsack Problem
  --------------------------------------
-/

variable (α β : Type) [LinearOrder β]

def brute (P : Problem) : ItemList :=
  let sublists := P.items.sublists
  let feasible_solutions := sublists.filter (fun items : ItemList ↦ decide (items.feasible P))
  let max_list := argmax ItemList.price feasible_solutions
  match max_list with
  | none => []
  | some opt => opt

#eval brute problem1

[Z. Wu]

Not sure if it's appropriate here, but do you mind posting the final proof when you are done?
I'm interested to see the final version of this problem

[Asei Inoue]

@Adomas Baliuka @Yaël Dillies Thank you very much. I'm glad to know how to use `Decidable.

[Asei Inoue]

@Z. Wu Thanks for your interest. I'll share the code here when it's completed.

[Asei Inoue]

There is an optimal solution even if the item set is empty

@Adomas Baliuka Why did you add hypothesis (nonem : P.items ≠ []) ? If P.items = [], then [] is an optimal solution.

[Asei Inoue]

I can prove optimal_of_empty as followings.

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr, DecidableEq

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr, DecidableEq

/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Prop :=
  items ⊆ P.items ∧ items.weight <= P.capacity

open ItemList

instance instDecidableFeasible (items : ItemList) (P : Problem) :
    Decidable (ItemList.feasible items P) := by
  simp [feasible, weight]
  infer_instance

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price

@[simp]
lemma optimal_of_empty (P : Problem) (emp : P.items = []) : optimal [] P := by
  simp [optimal, feasible, weight, emp]
  intro opp hopp
  replace hopp : opp = [] := by
    exact? says
      exact subset_nil.mp hopp
  simp? [hopp] says
    simp only [
      hopp,
      map_nil,
      sum_nil,
      zero_le,
      le_refl,
      forall_true_left
    ]

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  let sublists := P.items.sublists
  let feasible_solutions := sublists.filter (fun items : ItemList ↦ decide (items.feasible P))

  sorry

/- Finset.exists_maximal.{u_4} {α : Type u_4} [inst✝ : Preorder α] (s : Finset α) (h : Finset.Nonempty s) :
  ∃ m ∈ s, ∀ x ∈ s, ¬m < x -/
#check Finset.exists_maximal

/-!
  ## Examples for Test
  --------------------
-/

def problem1 : Problem := {
    items := [⟨1, 2⟩, ⟨2, 1⟩, ⟨3, 4⟩]
    capacity := 5
  }

#eval problem1.items

def sol1 : ItemList := [⟨1, 2⟩]

#eval sol1.price

/-!
  ## Algorithm to Solve Knapsack Problem
  --------------------------------------
-/

variable (α β : Type) [LinearOrder β]

def brute (P : Problem) : ItemList :=
  let sublists := P.items.sublists
  let feasible_solutions := sublists.filter (fun items : ItemList ↦ decide (items.feasible P))
  let max_list := argmax ItemList.price feasible_solutions
  match max_list with
  | none => []
  | some opt => opt

#eval brute problem1

[Asei Inoue]

finite set has an element that gives the maximum value of the function

-- something like this might help, although I also haven't proved it yet...
#check Finset.exists_maximal

Thank you very much! I am sure your comments will be useful. But I want a proposition that shows that there exists an element in a finite set that maximises the value of a given function.

[Asei Inoue]

Unfortunately I don't find such a theorem.

import Mathlib.Tactic

#find Finset ?a → (?a → ?b) → ?a

I would like to ask if there is a similar theorem in mathlib.

[Yakov Pechersky]

(Finset.image f s).max' (hs.image _), where s is your finset and hs is your proof that it's not empty. This is the direct construction of the max. Then, Finset.max'_mem is the proof that that max is a member of the image. Use Finset.mem_image to rewrite that proof into the existential of the element in the original finset such that it maps to the max.

[Yakov Pechersky]

(deleted)

[Asei Inoue]

@Yakov Pechersky Thanks! I will try it.

[Asei Inoue]

How can I create a Finset term from a list of lists?

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr, DecidableEq

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr, DecidableEq

/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Prop :=
  items ⊆ P.items ∧ items.weight <= P.capacity

open ItemList

instance instDecidableFeasible (items : ItemList) (P : Problem) :
    Decidable (ItemList.feasible items P) := by
  simp [feasible, weight]
  infer_instance

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price

@[simp]
lemma optimal_of_empty (P : Problem) (emp : P.items = []) : optimal [] P := by
  simp [optimal, feasible, weight, emp]
  intro opp hopp
  replace hopp : opp = [] := by
    exact subset_nil.mp hopp
  simp [hopp]

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  let sublists := P.items.sublists
  let feasible_solutions := sublists.filter (fun items : ItemList ↦ decide (items.feasible P))
  let solutions : Finset (P.items : Type) := by sorry -- error!!!!!
  sorry

[Asei Inoue]

oh I have found a List.toFinset (https://loogle.lean-lang.org/?q=List+%3Fa+-%3E+Finset+%3Fa)

[Asei Inoue]

@Yakov Pechersky Thanks for the advice. But I think it could be shown using the argmax of the List directly, without going through Finset.

[Asei Inoue]

my attempt:

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr, DecidableEq

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr, DecidableEq

/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Prop :=
  items ⊆ P.items ∧ items.weight <= P.capacity

open ItemList

instance instDecidableFeasible (items : ItemList) (P : Problem) :
    Decidable (ItemList.feasible items P) := by
  simp [feasible, weight]
  infer_instance

/-!
  ### Optimality of a feasible solution
-/

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price

@[simp]
lemma optimal_of_empty (P : Problem) (emp : P.items = []) : optimal [] P := by
  simp [optimal, feasible, weight, emp]
  intro opp hopp
  replace hopp : opp = [] := by
    exact subset_nil.mp hopp
  simp [hopp]

#check argmax

#eval argmax (fun x ↦ - x) [1, 2, -5, 3]

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  let sublists := P.items.sublists
  let feasible_solution_list := sublists.filter (fun items : ItemList ↦ decide (items.feasible P))

  have nonemp : feasible_solution_list ≠ [] := by
    simp [feasible_solution_list]
    intro h
    guard_hyp h : filter (fun items => decide (feasible items P)) (List.sublists P.items) = []
    -- how to get `[] : ItemList is not feasible solution of P` from `h`...?
    sorry

  let optimal_solution := argmax ItemList.price feasible_solution_list
  match optimal_solution with
  | none => sorry
  | some opt =>
    exists opt
    unfold optimal
    refine ⟨?feas, ?opt⟩

    case feas =>
      sorry

    case opt =>
      sorry

[Yakov Pechersky]

You asked about a Finset function, so I gave you a finset function.

[Asei Inoue]

@Yakov Pechersky Oh you're right. I didn't check enough ... Sorry ...

[Yakov Pechersky]

The same strategy of max', max'_mem, and mem_image should work for the equivalent statements for lists.

[Yakov Pechersky]

Suggestion: prove that Itemlist.feasible [] P for any P. Then you know for sure that feasible_solution_list \ne [] since [] is in any sublists.

[Yakov Pechersky]

And use refine with argmax, thus leaving you with solely the \forall opp ... goal. That goal should be dealt with using docs#List.le_of_mem_argmin. Since you have that opp \subset P.items, so opp \mem P.items.sublists so opp.price \le (argmax ...).price.

[Yaël Dillies]

Asei Inoue said:

But I want a proposition that shows that there exists an element in a finite set that maximises the value of a given function.

docs#Finset.exists_max_image

[Asei Inoue]

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  let sublists := P.items.sublists
  let feasible_solution_list := sublists.filter (fun items : ItemList ↦ decide (items.feasible P))

  have nonemp : feasible_solution_list ≠ [] := by
    simp [feasible_solution_list]
    intro h
    set f := fun items => decide (feasible items P) with fh
    have femp : f [] := by simp [f]
    have emp_sub : [] ∈ P.items.sublists := by
      simp [sublists]
    have emp_mem : [] ∈ filter f (List.sublists P.items) := by exact mem_filter_of_mem emp_sub femp
    rw [h] at emp_mem
    contradiction

  let feasible_solution_finset := feasible_solution_list.toFinset
  let optimal_solution := argmax ItemList.price feasible_solution_list
  match optimal_solution with
  | none => sorry
  | some opt =>
    exists opt
    unfold optimal
    refine ⟨?feas, ?opt⟩

    case feas =>
      sorry

    case opt =>
      sorry

[Asei Inoue]

I am finally able to show nonemp . Thanks.

[Adomas Baliuka]

I tried doing this proof yesterday and got stuck on the fact that sublists does not give you "every feasible subset" due to order. So using Finset.exists_max_image requires you to prove that "for any feasible subset of available items, there is a sublist inside feasible_solution_list that has the same price (i.e., a reordering that is inside feasible_solution_list)". Of course, this can be proved but it might take some work that I had not anticipated.

Alternatively, one might use some function instead of sublists which gives you a list of "all permutations of sublists". I didn't find such a function in the library. If you want to prove eventually that brute gives an optimal solution, this approach might not be the way to go.

[Adomas Baliuka]

Here's what I did, just in case it helps you... I think I won't have time to play with this for a while

lemma ItemList.emptyFeasible (P : Problem) : ItemList.feasible [] P := by simp [ItemList.feasible, weight]

lemma mem_toFinset_pred [DecidableEq α] (l : List α) (P : α → Prop)
    : (∃ x ∈ l, P x) ↔ (∃ x ∈ l.toFinset, P x) := by
    simp_all only [mem_toFinset]

#check Finset.exists_max_image
lemma List.exists_max_image [DecidableEq α] [DecidableEq β] [LinearOrder α]
    {l : List β} (f : β → α) (h : l ≠ [])
  : ∃ x ∈ l, ∀ x' ∈ l, f x' ≤ f x := by
    apply (mem_toFinset_pred l (fun m ↦ ∀ x ∈ l, f x ≤ f m)).mpr
    simp_rw [←mem_toFinset]
    apply Finset.exists_max_image
    exact (toFinset_nonempty_iff l).mpr h

-- solution ∈ filter (fun items => decide (feasible items P)) (sublists P.items)
lemma prop_of_filter_prop [DecidableEq α] {l : List α} {P : α → Prop} [DecidablePred P] {a : α}
    (h : a ∈ filter (fun a' => decide (P a')) l)
    : P a := by
    have := List.filter_subset (p:=(fun a' => decide (P a'))) l
    have := (List.mem_filter.mp h).2
    simp_all only [decide_eq_true_eq]

open ItemList in
theorem exist_optimal (P : Problem)
    : ∃ items : ItemList, items.optimal P := by
  let feasibles := (P.items).sublists.filter (fun items : ItemList ↦ decide (items.feasible P))
  have sublnonempty : feasibles ≠ [] := by
    simp [feasibles]
    have nil_mem_sublists : [] ∈ P.items.sublists := by simp only [mem_sublists, nil_sublist]
    by_contra h
    have := List.filter_eq_nil.mp h [] (by simp)
    have emptyFeas := emptyFeasible P
    simp at this
    contradiction
  obtain ⟨solution, ⟨isfeasible, ismax⟩⟩ := List.exists_max_image price sublnonempty
  use solution
  simp [optimal]
  constructor
  · simp [feasibles] at isfeasible
    apply prop_of_filter_prop isfeasible
  · rintro opp ⟨opp_within, opp_capac⟩
    sorry -- remains to prove that any feasible *subset* of P.items
    -- is a reordering of some *sublist* inside `feasibles`, and that
    -- `ItemList.price` is permutation-invariant.

[Adomas Baliuka]

(Also, of course, I was dumb and didn't use List.argmax, so I had to prove a version of List.le_of_mem_argmax, which you probably shouldn't copy...)

[Yakov Pechersky]

My argmax idea was wrong. Because what feasible is doesn't limit the number of times an Item can be duplicated. For example, I can have a problem of { items := [(1, 1)], capacity: 100 }. Then the optimal items are that item x 100. That's never going to be in sublists.

[Yakov Pechersky]

This is my way of building out the API:

import Mathlib.Tactic

namespace Knapsack

open List

/-!
  ## The definition of Knapsack problem
-/

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr, DecidableEq

structure Problem where
  /-- the list of items -/
  items : List Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving Repr, DecidableEq

/-!
  ## The Basic Functions
-/

abbrev ItemList := List Item

def ItemList.price (items : ItemList) : ℕ :=
  (items.map Item.price).sum

def ItemList.weight (items : ItemList) : ℕ :=
  (items.map Item.weight).sum

def ItemList.feasible (items : ItemList) (P : Problem) : Prop :=
  items ⊆ P.items ∧ items.weight <= P.capacity

theorem ItemList.feasible_iff {items: ItemList} {P : Problem} :
    items.feasible P ↔ items ⊆ P.items ∧ items.weight <= P.capacity := Iff.rfl

@[simp]
theorem ItemList.feasible_nil (P : Problem) : ItemList.feasible [] P :=
  ⟨nil_subset _, Nat.zero_le _⟩

abbrev Problem.empty (P : Problem) : Prop := P.items = []

theorem ItemList.feasible_empty_iff {items: ItemList} {P : Problem} (h : P.empty) :
    items.feasible P ↔ items = [] := by
  simp (config := { contextual := true }) [feasible_iff, h, List.subset_nil, weight]

theorem ItemList.perm_price_eq {items items' : ItemList} (h : items ~ items') :
    items.price = items'.price := by
  simp [price, (h.symm.map _).sum_eq]

theorem ItemList.perm_weight_eq {items items' : ItemList} (h : items ~ items') :
    items.weight = items'.weight := by
  simp [weight, (h.symm.map _).sum_eq]

theorem ItemList.feasible.perm {items items' : ItemList} {P : Problem} (h : items.feasible P)
    (hp : items ~ items') : items'.feasible P :=
  ⟨hp.symm.subset.trans h.left, h.right.trans' (perm_weight_eq hp).ge⟩

open ItemList

instance instDecidableFeasible (items : ItemList) (P : Problem) :
    Decidable (ItemList.feasible items P) :=
  decidable_of_iff' _ (ItemList.feasible_iff)

/-!
  ### Optimality of a feasible solution
-/

def ItemList.optimal (items : ItemList) (P : Problem) : Prop :=
  items.feasible P ∧
  ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price

theorem ItemList.optimal_iff {items : ItemList} {P : Problem} :
    items.optimal P ↔
      items.feasible P ∧ ∀ opp : ItemList, opp.feasible P → opp.price ≤ items.price := Iff.rfl

lemma optimal_of_empty (P : Problem) (emp : P.empty) : optimal [] P := by
  simp [optimal_iff, feasible_empty_iff emp]

theorem ItemList.optimal.perm {items items' : ItemList} {P : Problem} (h : items.optimal P)
    (hp : items ~ items') : items'.optimal P := by
  rw [optimal_iff, items.perm_price_eq hp] at *
  exact h.imp (ItemList.feasible.perm · hp) (by simp)

@[simp]
theorem _root_.List.sublists_ne_nil {α : Type*} (l : List α) : l.sublists ≠ [] := by
  induction l
  case nil => simp
  case cons =>
  rw [sublists_cons]
  simp only [bind_eq_bind, ne_eq, bind_eq_nil, mem_sublists, not_forall, exists_prop, and_true]
  exact ⟨[], by simp⟩

theorem _root_.List.argmax_isSome_of_ne_nil {α β : Type*} [Preorder β]
    [DecidableRel (fun x y : β ↦ x < y)] (l : List α) (f : α → β) (hl : l ≠ []) :
    (l.argmax f).isSome := by
  simp [←Option.ne_none_iff_isSome, hl]

theorem _root_.List.argmin_isSome_of_ne_nil {α β : Type*} [Preorder β]
    [DecidableRel (fun x y : β ↦ x < y)] (l : List α) (f : α → β) (hl : l ≠ []) :
    (l.argmin f).isSome := by
  simp [←Option.ne_none_iff_isSome, hl]

lemma ItemList.feasible.exists_perm_mem_sublists {items : ItemList} {P : Problem}
    (h : items.feasible P) : ∃ l, items ~ l ∧ l ∈ P.items.sublists := by
  rw [feasible_iff] at h
  contrapose! h
  intro H
  sorry -- fails here

theorem exist_optimal (P : Problem) : ∃ items : ItemList, items.optimal P := by
  have ha := (P.items.sublists.filter (ItemList.feasible · P)).argmax_isSome_of_ne_nil
    ItemList.price $ List.ne_nil_of_mem
    (List.mem_filter_of_mem (by simp) (decide_eq_true (ItemList.feasible_nil _)))
  refine ⟨Option.get _ ha, ?_⟩
  obtain ⟨l', hl⟩ := Option.isSome_iff_exists.mp ha
  obtain ⟨ha'', hl'⟩ := Option.eq_some_iff_get_eq.mp hl
  rw [List.argmax_eq_some_iff] at hl
  simp_rw [hl']
  rw [optimal_iff]
  refine ⟨?_, ?_⟩
  · simpa using List.of_mem_filter hl.left
  intros opp hf
  obtain ⟨opp', hp, hmem⟩ := hf.exists_perm_mem_sublists
  rw [opp.perm_price_eq hp]
  apply hl.right.left
  exact List.mem_filter_of_mem hmem (by simpa using hf.perm hp)

[Adomas Baliuka]

Yakov Pechersky said:

My argmax idea was wrong. Because what feasible is doesn't limit the number of times an Item can be duplicated. For example, I can have a problem of { items := [(1, 1)], capacity: 100 }. Then the optimal items are that item x 100. That's never going to be in sublists.

I think that means the definition of feasible should be changed? Doesn't sound like the normal Knapsack problem. (Edit: never mind, it's called "unbounded knapsack problem)

[Yakov Pechersky]

For the unbounded one, one brute force witness would be the argmax of sublists of Problem.items repeated capacity times (because we are over N). Of course, that's too loose, one could do capacity / min weight over P.items but the proof will probably be easier if you do with a plain repeated capacity times.

[Yakov Pechersky]

But even that doesn't work here, because there is nothing constraining an Item to have greater than 0 weight.

[Yakov Pechersky]

If I had such an item, then feasible items are unbounded.

[Adomas Baliuka]

Maybe we should check first if this is really the problem @Asei Inoue wants to work on. Did you mean to define an "unbounded knapsack"? The brute algorithm you wrote would suggest otherwise.

[Asei Inoue]

@Adomas Baliuka

Did you mean to define an "unbounded knapsack"?

No. I thought I had defined the knapsack problem of non-reusable items.

[Asei Inoue]

My brute algorithm was designed with this assumption in mind, as you said

[Yakov Pechersky]

Then List.subset isn't the correct way to express the constraint. I think it would be fine if you used Multiset everywhere in place of List.

[Asei Inoue]

It certainly doesn't seem like a good idea to have items as a list...

import Mathlib.Tactic

#guard [1, 1, 2] ⊆ [1, 2]

[Asei Inoue]

Is this better...?

import Mathlib.Tactic

namespace Knapsack

open List

structure Item where
  /-- the weight of item -/
  weight : ℕ
  /-- the price of item -/
  price : ℕ
  deriving Repr, DecidableEq

structure Problem where
  /-- the group of items -/
  items : Multiset Item
  /-- the capacity of the knapsack -/
  capacity : ℕ
  deriving DecidableEq

[Yakov Pechersky]

You also likely want to make items weigh a positive amount

[Adomas Baliuka]

I guess the ways for doing that would be to either change the type of weightof include another field for the hypothesis. Which would you choose here @Yakov Pechersky? I think in some cases such choices can turn out to make quite a difference for how easy it is to deal with later...

[Yakov Pechersky]

You can do make weight a pnat, you can add a property to Item, you can make a restriction in feasible to restrict items to ones with positive weight.

[Asei Inoue]

Thanks to all who have helped me so far.
I won't have time for this problem for a while ...
If anyone is interested in this problem, please feel free to work on it.