simp behaviour

Stream: lean4

[Jakob von Raumer]

When the goal depends on a hypothesis which we simplify, the old unsimplified version stays in the context and the goal still depends on the old version. Is that the desired behaviour?

inductive W : Nat → Prop where
| mk1 : W 5

example (w : W (5, 3).1) (β : {n : Nat} → W n → Type) : β w := by
  simp at w

[Mario Carneiro]

lean 3 does the same thing. This is unavoidable, given the way that simp works. dsimp should avoid this behavior

[Jakob von Raumer]

We don't have dsimp yet, do we?

[Mario Carneiro]

ah, well then

[Mario Carneiro]

a simple version of dsimp would be to call simp, then throw away the proof and change the hypothesis using revert/intro

[Jakob von Raumer]

We don't have change yet, either ^^

[Mario Carneiro]

it's called show now

[Jakob von Raumer]

Yes, and the Meta backend of it is trivial anyway

[Mario Carneiro]

Hi lean devs, can you make mkSimpContext, elabSimpLemmas, addSimpLemma, addDeclToUnfoldOrLemma in Lean.Elab.Tactic.Simp not private?