simp? missing lemmas

Stream: mathlib4

[Michael Stoll]

import Mathlib.Tactic.Says

variable {α} [DecidableEq α] (a b : α)

example (x : α) (hx : x = a ∨ x = b) : x ∈ [a, b] := by
  -- simp [hx] -- no goals
  simp? [hx] says simp only [List.mem_cons, List.mem_singleton, hx]
  -- ⊢ x = a ∨ x = b ∨ x ∈ []
  simp? says simp only [List.not_mem_nil, or_false]
  -- ⊢ x = a ∨ x = b
  simp? [hx] says simp only [hx]

It appers that simp? leaves out some lemmas that the simp call actually uses.

[Kim Morrison]

The problem is not so much simp? leaving anything out that it used, but rather the simp only call using the lemmas in a different way:

import Std.Data.List.Lemmas

variable {α} (a b : α)

set_option trace.Meta.Tactic.simp.rewrite true

example (x : α) (hx : x = a ∨ x = b) : x ∈ [a, b] := by
  simp [hx]
  -- [Meta.Tactic.simp.rewrite] @List.mem_cons:1000, x ∈ [a, b] ==> x = a ∨ x ∈ [b]
  -- [Meta.Tactic.simp.rewrite] @List.mem_singleton:1100, x ∈ [b] ==> x = b
  -- [Meta.Tactic.simp.rewrite] hx:1000, x = a ∨ x = b ==> True

example (x : α) (hx : x = a ∨ x = b) : x ∈ [a, b] := by
  simp only [List.mem_cons, List.mem_singleton, hx]
  -- [Meta.Tactic.simp.rewrite] @List.mem_cons:1000, x ∈ [a, b] ==> x = a ∨ x ∈ [b]
  -- [Meta.Tactic.simp.rewrite] @List.mem_cons:1000, x ∈ [b] ==> x = b ∨ x ∈ []

[Kim Morrison]

The problem is that mem_singleton has priority 1100, but when we provide it as a term in a simp only call this priority is forgotten, and so it doesn't get promoted ahead of mem_cons.

[Kim Morrison]

I'm not sure how to fix this!

• Could we look up the priorities for explicitly provided simp lemmas? (this seems best if it is implementable)
• Could we provide a way of specifying priorities in simp only? And generate these priorities in simp??

[Mario Carneiro]

why not both?

[Mario Carneiro]

I'm not sure if it is more or less surprising to get the priority of an explicitly passed simp lemma from the @[simp N] attribute

[Mario Carneiro]

but a (prio := N) argument to simp lemmas in an explicit simp [...] call sounds like it would be useful for simp-set macros

[Yury G. Kudryashov]

I think that priorities of explicitly provided simp lemmas should be higher than default.

[Yury G. Kudryashov]

If I provide a lemma, then probably I really want to use it.

[Yury G. Kudryashov]

E.g., if I say simp [not_and_or], then I don't want to use docs#not_and

[Michael Stoll]

Maybe we need a special case for the output of simp? that keeps the priorities the same as they were in the simp? call? Maybe simp only! [...]? But that would not provide a way to make explicitly provided lemmas higher priority, as it could not differentiate whether a lemma in the simp set was provided explicitly to the original call or not. Annotating the lemmas with their priority (if different from 1000) seems the most flexible (if potentially a bit verbose) approach to me.

[Michael Stoll]

This has just hit me again:

mport Mathlib.Analysis.Complex.Basic

set_option trace.Meta.Tactic.simp.rewrite true

lemma test1 {F : ℕ → ℂ} : Set.indicator {0}ᶜ F 0 = 0 := by
  simp? says simp only [Set.mem_compl_iff, not_true_eq_false, not_false_eq_true,
      Set.indicator_of_not_mem] -- simp made no progress
  -- goal: `Set.indicator {0}ᶜ F 0 = 0`

lemma test2 {F : ℕ → ℂ} : Set.indicator {0}ᶜ F 0 = 0 := by
  simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, not_false_eq_true,
    Set.indicator_of_not_mem]
  -- no goals

The trace in the second call is

[Meta.Tactic.simp.rewrite] @Set.mem_compl_iff:1000, 0 ∈ {0}ᶜ ==> 0 ∉ {0}
[Meta.Tactic.simp.rewrite] @Set.mem_singleton_iff:1000, 0 ∈ {0} ==> 0 = 0
[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True
[Meta.Tactic.simp.rewrite] not_true_eq_false:1000, ¬True ==> False
[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, ¬False ==> True
[Meta.Tactic.simp.rewrite] @Set.indicator_of_not_mem:1000, Set.indicator {0}ᶜ F 0 ==> 0
[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True

(with just simp, it is

[Meta.Tactic.simp.rewrite] @Set.mem_compl_iff:1000, 0 ∈ {0}ᶜ ==> 0 ∉ {0}
[Meta.Tactic.simp.rewrite] @Set.mem_singleton_iff:1000, 0 ∈ {0} ==> 0 = 0
[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True
[Meta.Tactic.simp.rewrite] not_true_eq_false:1000, ¬True ==> False
[Meta.Tactic.simp.rewrite] @Set.mem_compl_iff:1000, 0 ∈ {0}ᶜ ==> 0 ∉ {0}
[Meta.Tactic.simp.rewrite] not_true_eq_false:1000, ¬True ==> False
[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, ¬False ==> True
[Meta.Tactic.simp.rewrite] @Set.indicator_of_not_mem:1000, Set.indicator {0}ᶜ F 0 ==> 0
[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True

which is pretty similar).

Howeverm it looks like all priorities are the same and Set.mem_singleton_iff is actually used by the simpcall, so there seems to be a more fundamental problem with the output of simp?. (I also noticed that it still frequently adds gt_iff_lt and/or ge_iff_le even though they are not really needed.)

[Michael Stoll]

Minimized a bit more:

import Mathlib.Algebra.Function.Indicator

def foo (s : Set ℕ) [DecidablePred (· ∈ s)] (a : ℕ) : ℕ := if a ∈ s then 1 else 0

@[simp]
lemma bar {s : Set ℕ} [DecidablePred (· ∈ s)] {a : ℕ} (h : a ∉ s) : foo s a = 0 := by
  simp only [foo, h, ↓reduceIte]

lemma test1 : foo {0}ᶜ 0 = 0 := by
  simp? says simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false,
      not_false_eq_true, bar]

lemma test2 {F : ℕ → ℕ} : Set.indicator {0}ᶜ F 0 = 0 := by
  -- simp -- works
  simp? says simp only [Set.mem_compl_iff, not_true_eq_false, not_false_eq_true,
    Set.indicator_of_not_mem]
  -- simp made no progress, `Set.mem_singleton_iff` is missing

I'm trying to emulate Set.indicator_of_not_mem via bar, but in this case, simp? does put Set.mem_singleton_iff in the list.

I have no idea how to debug this.

[Michael Stoll]

@Scott Morrison ?

[Kim Morrison]

Keep minimising. :-)

The basic no-insight-required method is to iteratively:

• replace import X with its imports and section X; <contents of X>; end X
• delete everything from that section that isn't needed to reproduce the problem
• remove any imports that aren't needed

Until no imports remain.

[Michael Stoll]

This seems to be very brittle.

import Mathlib.Data.Set.Function

-- copied definitions
noncomputable def Set.indicator' {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : α → M)
    (x : α) : M :=
  haveI := Classical.decPred (· ∈ s)
  if x ∈ s then f x else 0

@[simp]
theorem Set.indicator_of_not_mem' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {a : α}
    (h : a ∉ s) (f : α → M) :
    Set.indicator' s f a = 0 :=
  if_neg h

lemma test1 {F : ℕ → ℕ} : Set.indicator' {0}ᶜ F 0 = 0 := by
  simp? -- includes `Set.mem_singleton_iff`

import Mathlib.Algebra.Function.Indicator

-- attribute[-simp] Set.indicator_of_mem -- with attribute removed: OK

lemma test2 {F : ℕ → ℕ} : Set.indicator {0}ᶜ F 0 = 0 := by
  simp?

But:

import Mathlib.Data.Set.Function

-- copied definitions
noncomputable def Set.indicator' {α : Type u_1} {M : Type u_4} [Zero M] (s : Set α) (f : α → M)
    (x : α) : M :=
  haveI := Classical.decPred (· ∈ s)
  if x ∈ s then f x else 0

@[simp]
theorem Set.indicator_of_not_mem' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {a : α}
    (h : a ∉ s) (f : α → M) :
    Set.indicator' s f a = 0 :=
  if_neg h

@[simp]
theorem Set.indicator_of_mem' {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {a : α}
    (h : a ∈ s) (f : α → M) :
    Set.indicator' s f a = f a :=
  if_pos h

lemma test1 {F : ℕ → ℕ} : Set.indicator' {0}ᶜ F 0 = 0 := by
  simp? -- OK

[Michael Stoll]

This is how far I got:

def Set := Nat → Prop

namespace Set

def singleton (a : Nat) : Set := fun b ↦ b = a

def compl (s : Set) : Set := fun x ↦ ¬ s x

@[simp]
theorem compl_iff (s : Set) (x : Nat) : s.compl x ↔ ¬ s x := Iff.rfl

@[simp]
theorem singleton_iff {a b : Nat} : singleton b a ↔ a = b := Iff.rfl

open Classical

noncomputable def indicator (s : Set) (x : Nat) : Nat := if s x then 1 else 0

@[simp] -- remove `simp` attribute --> works (and the trace changes)
theorem indicator_of {s : Set} {a : Nat} (h : s a) : indicator s a = 1 := if_pos h

@[simp]
theorem indicator_of_not {s : Set} {a : Nat} (h : ¬ s a) : indicator s a = 0 := if_neg h

set_option trace.Meta.Tactic.simp.rewrite true

theorem test : indicator (compl <| singleton 0) 0 = 0 := by
  simp? -- leaves out `singleton_iff` even though it is necessary

I have no idea why and how the fact whether indicator_of_mem is a simp lemma or not influences a simp? call that does not use it.

[Michael Stoll]

Trying to minimize a bit fruther...

[Michael Stoll]

Done in the code block above. This seems to be close to the bare minimum. @Scott Morrison ?

[Kim Morrison]

Can you open an issue on the Lean repo?

[Michael Stoll]

I have never done that, but I will try.

[Michael Stoll]

lean4#3710

[Michael Stoll]

With set_option trace.Meta.Tactic.simp.discharge true, the trace in the "bad" case is

[Meta.Tactic.simp.discharge] @Set.indicator_of discharge ❌
      Set.compl (Set.singleton 0) 0 ▼
  [rewrite] Set.compl_iff:1000, Set.compl (Set.singleton 0) 0 ==> ¬Set.singleton 0 0
  [rewrite] @Set.singleton_iff:1000, Set.singleton 0 0 ==> 0 = 0
  [rewrite] @eq_self:1000, 0 = 0 ==> True
  [rewrite] not_true_eq_false:1000, ¬True ==> False

[Meta.Tactic.simp.discharge] @Set.indicator_of_not discharge ✅
      ¬Set.compl (Set.singleton 0) 0 ▼
  [rewrite] Set.compl_iff:1000, Set.compl (Set.singleton 0) 0 ==> ¬Set.singleton 0 0
  [rewrite] not_true_eq_false:1000, ¬True ==> False
  [rewrite] not_false_eq_true:1000, ¬False ==> True

[Meta.Tactic.simp.rewrite] @Set.indicator_of_not:1000, Set.indicator (Set.compl (Set.singleton 0)) 0 ==> 0

[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True

whereas in the "good" case, it is

[Meta.Tactic.simp.discharge] @Set.indicator_of_not discharge ✅
      ¬Set.compl (Set.singleton 0) 0 ▼
  [rewrite] Set.compl_iff:1000, Set.compl (Set.singleton 0) 0 ==> ¬Set.singleton 0 0
  [rewrite] @Set.singleton_iff:1000, Set.singleton 0 0 ==> 0 = 0
  [rewrite] @eq_self:1000, 0 = 0 ==> True
  [rewrite] not_true_eq_false:1000, ¬True ==> False
  [rewrite] not_false_eq_true:1000, ¬False ==> True

[Meta.Tactic.simp.rewrite] @Set.indicator_of_not:1000, Set.indicator (Set.compl (Set.singleton 0)) 0 ==> 0

[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True

Note: in the "bad" case, singleton_iff is used in the first attempt via indicator_of that ultimately fails, and is not listed again in the second (succeeding) attempt. However, it is necessary to use it there (as the "good" trace shows).

Speculation: simp caches the result obtained from singleton_iff in the first attempt and reuses that in the second one, but does not take note of it for inclusion in the lemma list.

Does this sound reasonable?

[Michael Stoll]

@Scott Morrison @Mario Carneiro :up:
Do you think this makes sense?

[Mario Carneiro]

I recall there was some issue here with the UsedSimps state getting reset or not being handled correctly when simp backtracks