Using `simp`

Stream: lean4

[yokatta]

I'm trying to do the following proof:

import Mathlib.Data.List.Basic

theorem thm
  {α : Type} [DecidableEq α] {xs : List α} (mem : { x // x ∈ xs }) (f : { x // x ∈ xs } → Nat) :
  f mem < (xs.attach.map f).sum :=
  match xs with
  | [] => nomatch mem
  | x :: xs => by
      simp only [List.mem_cons] at mem f
      sorry

Why is it when I try to simplify { x_1 // x_1 ∈ x :: xs } to { x_1 // x_1 = x ∨ x_1 ∈ xs }, the old terms are kept in the tactic state and only new ones are made? How can I do the simplification so that it updates the terms correclt.?

[Kyle Miller]

A way to think about how simp at works is that it adds the simplified term as a new hypothesis and deletes the old one if possible (unless simp is using only rfl lemmas, in which case it changes the type of the hypothesis directly). This means that if the goal depends on the original hypothesis, there is a chance it won't be able to delete it.

[Kyle Miller]

These are some tricky dependent types to work with, but the statement needs a bit more work since it's currently false as stated:

import Mathlib.Data.List.Basic

axiom thm
  {α : Type} [DecidableEq α] {xs : List α} (mem : { x // x ∈ xs }) (f : { x // x ∈ xs } → Nat) :
  f mem < (xs.attach.map f).sum

theorem ohno : False := by
  let xs := [1]
  let mem : {x // x ∈ xs} := ⟨1, by simp⟩
  let f : {x // x ∈ xs} → Nat := fun m => m.1
  have := thm mem f
  simp at this

[yokatta]

Thank you, it should be ≤, not <.

[yokatta]

Do you have a suggestion for how to deal with this kind of problem where I need to simplify a hypothesis that appears in the goal?

[Mario Carneiro]

in this particular case you are lucky because the statement is still true without the attach

[Mario Carneiro]

import Mathlib.Data.List.BigOperators.Basic

theorem thm' {α : Type} [DecidableEq α] {xs : List α}
    (x : α) (h : x ∈ xs) (f : α → Nat) : f x ≤ (xs.map f).sum :=
  List.single_le_sum (by simp) _ (List.mem_map_of_mem _ h)

theorem thm {α : Type} [DecidableEq α] {xs : List α}
    (mem : { x // x ∈ xs }) (f : { x // x ∈ xs } → Nat) : f mem ≤ (xs.attach.map f).sum :=
  thm' _ (List.mem_attach _ _) _

[Kyle Miller]

You beat me to it. Yeah, ideally you prove something that's as non-dependent as possible and use that to prove the dependent one

[yokatta]

Thanks! I wasn't expecting a full proof, though seems like yours would have been much simpler than mine anyways. Out of curiosity, how did you find the right theorem to finish the proof? Just tried using library_search for the first time, is the expectation to go through each of the suggested refinements and find one that seems like it's easier to prove?

[Mario Carneiro]

I use old school methods to find theorems. I searched for List.sum, found the file that proves stuff like sum_le_sum and looked around because I knew that there would be something relevant in there