simp at * with hypotheses occurring in the goal

Stream: lean4

[Sven Manthe]

In the following MWE, simp at * does not simplify a hypothesis, seemingly because it occurs in the goal:

def z : Nat := 0
@[simp] theorem zeq : z = 0 := rfl
def P := True
theorem bug (f : z = 0 → Prop) (h : z = 0) : f h ∨ P ∨ P := by
  simp [zeq] at * -- this simplifies the goal, but not the hypothesis h
  simp [zeq] at h -- this simplifies the hypothesis h
  exact Or.inr trivial

I was wondering whether this is a bug. Otherwise, is there a variant of simp at * also simplifying hypotheses used in the goal?

[Kyle Miller]

Notice that simp [zeq] at h doesn't simplify h per se, but it creates a new hypothesis called h, shadowing the old one, and simplifies that. It needs to do this because f depends on its argument being a proof of z = 0.

That said, I haven't looked into why simp at * works the way it does. This seems likely to be intentional.

[Kyle Miller]

In the code of docs#Lean.Elab.Tactic.simpLocation I see that in the wildcard case it collects specifically non-dependent proposition hypotheses.

[Sven Manthe]

Okay, thank you. My concrete use case was that I tried to write a tactic, not expecting this behavior (and know no metaprogamming). Do you have a suggestion how to achieve something like "for all hypotheses h, do simp at h", that is, explicitly create all these new shadowing hypotheses?