The result of simp? gives a different result to simp

Stream: lean4

[Bhavik Mehta]

Here's my mathlib-free mwe:

def nothing (T : Nat → Prop) : Prop := sorry
def bar (T : Nat → Prop) : Nat := sorry

def foo (x : Nat) : Prop :=
  ∃ (S : Nat → Prop) (_ : nothing S) (_ : ∀ T, (∀ x, T x → S x) → nothing T), x = bar S

theorem foo_zero (n : Nat) : foo n := by
  rw [foo]
  simp?

The goal after simp or simp? is of the form ∃ S, _ ∧ nothing S ∧ _, but the goal after applying the code action is of the form ∃ S, nothing S ∧ _ ∧ _.

[Kim Morrison]

What does simp? say?

[Kim Morrison]

Creating an issue from this would be useful!

[Bhavik Mehta]

Expanding the simp? says simp only [exists_prop', nonempty_prop, exists_and_left]

[Bhavik Mehta]

exists_and_left isn't necessary but it's believable that it's used somewhere

[Bhavik Mehta]

Kim Morrison said:

Creating an issue from this would be useful!

lean4#5308

[Kim Morrison]

Oof:

@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b :=
  ⟨i.elim, fun hb _ => hb⟩

looks like a bad idea!

[Kim Morrison]

(It applies everywhere, and generates a Nonempty \a goal, and then if \a is a Prop that simplifies to just \a.)

[Bhavik Mehta]

Hmm, I agree that looks like a bad idea but how do we know that that's responsible here?

[Bhavik Mehta]

I thought exists_prop' is the thing generating the Nonempty bits

[Kim Morrison]

set_option trace.Meta.Tactic.simp true

[Kim Morrison]

exists_prop' is generating Nonempty is a good way that we like: the rhs of the simp lemma

[Kim Morrison]

forall_const is generating it as a side goal

[Bhavik Mehta]

I agree forall_const is getting applied and a bunch of side goals like this are getting generated and this is a bad simp lemma, but turning it off doesn't fix the actual issue here; so I don't see how it's actually the culprit

[Kim Morrison]

Agreed, but I'm now distracted by fixing forall_const, which I suspect is an even bigger problem. :-)