simp working only after dsimp

Stream: lean4

[Thomas Murrills]

In a file I'm porting from mathlib (mathlib#1088), a mathlib proof of the formext; simp worked in lean 3, but needed to be changed to ext; dsimp; simp to work now.

A notable thing here is that the goal after ext; dsimp looks exactly the same as it does with just ext; simp; you have to set_option pp.all true to see the difference (not just pp.explicit).

Is this weird enough to warrant making an mwe for?

[Kevin Buzzard]

In my opinion every simp call which stops working after being ported should at least be flagged with a porting note, and ideally should be investigated. dsimp, simp is strictly speaking not good style because of the nonterminal dsimp. Does dsimp only; simp work?

[Yaël Dillies]

Kevin, once again this is all fine.

[Yaël Dillies]

Fancy tactics can be followed by fancy tactics, and arguably dsimp isn't even fancy at all.

[Kevin Buzzard]

You've said this before and then others have said "no it's not fine", right? I'm still unclear about this.

[Mario Carneiro]

I recall being part of that earlier conversation, and my line is that dsimp is a fancy tactic, but fancy tactics followed by other fancy tactics is okay. (Although dsimp, simp doing something different from simp is probably a bug in any case.)

[Kevin Buzzard]

I was talking to Oliver about this recently. Isn't the only reason we do dsimp, simp that dsimp unfolds structure projections but simp doesn't? Oliver suggested making the structure projection unfolding a simp lemma (Amelia was having problems with dsimps taking a long time)

[Thomas Murrills]

Just want to record that I encountered this again, this time in the form of needing to dsimp only [] at hypotheses for simp [*] to use them!

example (P : α → Prop) (h : P (y,y).1) : P y := by -- unsolved goals ...
  simp only [*]

example (P : α → Prop) (h : P (y,y).1) : P y := by -- works
  dsimp only [] at h
  simp only [*]

(Note that simp only [*, h] also is insufficient to close the goal.)

[Thomas Murrills]

Is there a better workaround than writing dsimp only ..., specifically in the context of using simp inside another tactic? Possibly a config option? If not, I'm considering having the tactic run dsimp only [] at * if the user provides a simp star, though this is imperfect, since it might change hypotheses that the user wouldn't expect to be touched. (If that were a big issue, maybe I could restore all hypotheses that weren't reported as used by simp, if the goal isn't closed? Not necessary for the immediate application, though.)

[Kyle Miller]

For what it's worth, I'd probably reach for simpa using h here

[Kyle Miller]

It'd be interesting if simp [*] would run simp on each local hypothesis while creating its simp set (no need to literally simp at *, unless you're just wanting to avoid reaching into internals -- it's possible to run the simplifier on any given Expr).

[Thomas Murrills]

simpa seems to work in the example! But in general (and in the real example that prompted this) we need to use simp only [*, simp_lemma1, simp_lemma2] and interleave the hypothesis applications with lemma simps, and there it struggles.

[Thomas Murrills]

It would! (I wonder what happens currently if a hypothesis is not in simp normal form or something, and causes a loop?) Though, I'd even settle for running the internal version of dsimp only [] on each hypothesis while creating the simp set. :)

[Kyle Miller]

Sometimes the best configuration option is simply a composition of tactics. Is there anything that a configuration option would let you do that preceding simp with dsimp only at * wouldn't do?

[Thomas Murrills]

If I run dsimp only at * inside the tactic I'm writing, then the user's hypotheses would change unexpectedly, unless I manage goals and the like. Not the biggest problem in the world, but still. Though, I am using simpGoals explicitly, and generating the simp context from syntax, so maybe there's an easy way to do this "the right way" somehow?

[Kyle Miller]

(and regarding trying to put things into simp normal form, just for comparison one place that does something about it is the @[elementwise] attribute, which uses a function to simp the LHS and RHS of the generated equality lemma separately)

[Kyle Miller]

Another "lean metaprogramming koan" for you is that making your tactic less smart makes it a smarter tactic. What feature are you trying to implement that you feel needs dsimp only at *?

[Kyle Miller]

It just occurred to me that even better than simpa using h for your examples is assumption. Many tactics use assumption to discharge some obvious goals.

[Kyle Miller]

Thomas Murrills said:

If I run dsimp only at * inside the tactic I'm writing, then the user's hypotheses would change unexpectedly

I was meaning that you'd leave the dsimp only at * to the user, if possible. Though maybe your tactic makes some hypotheses that you know will need simplification before they're useful.

[Thomas Murrills]

Kyle Miller said:

Another "lean metaprogramming koan" for you is that making your tactic less smart makes it a smarter tactic. What feature are you trying to implement that you feel needs dsimp only at *?

Ah, very wise. :) So, specifically, mono* using <simpArgs> (where mono* applies mono repetitively) runs (in MetaM, not by macro) simp only [<simpArgs>] before each application of mono. One of the extant usages of mono* is of the above form: there are hypotheses in the context which, if dsimp'd, could be used simp inside this tactic invocation. Moreover, the hypotheses need to be interleaved with other provided simp lemmas—we're running mono* using *, lem1, lem2—so following it by assumption doesn't work.

So basically, I was thinking I might try to patch what I see as a bug in simp "by hand". :)

In this particular case, mono (being fancy) also relies on solve_by_elim. Maybe it would make sense to pass these simp lemmas to solve_by_elim too, though that seems like overkill. (But if that takes more than a little while I might just say it's fine for now, get mono out there, and enhance it later. :) )

[Kyle Miller]

I've wished for a feature where simp could be told to simplify local hypotheses before. As a first step, maybe (if it doesn't already exist) there could be a simp% term elaborator that simplifies a term so you could write simp [simp% h, simp% s].

[Kyle Miller]

I wonder if * in a simp lemma list is ever "correct", or merely convenient. Simp expects simp lemmas, but random hypotheses in the local context surely aren't simp lemmas since what are the chances they're in normal form?

[Kyle Miller]

That suggests that either it shouldn't be used in non-draft code, or simp should be responsible for trying to transform the lemmas drawn in using * into a simp set.

[Kyle Miller]

(That said, I use it all the time for one-liner induction arguments: by induction x <;> simp [*] when it works is nice and short. The main purpose of * here is that I wanted to avoid naming the induction hypotheses, and furthermore, each case will have different local contexts.)

[Thomas Murrills]

It does seem pretty unsafe! I just wanted to check, and indeed you can make it loop indefinitely in the obvious way:

example (P : α → Prop) (h : a = b) (h' : b = a) : P b := by simp [*] -- simp failed, maximum number of steps exceeded

Though, I'm not sure that protecting against this sort of thing is worth the overhead. I suppose it depends on how expensive making a simp set is.

[Thomas Murrills]

I do love the feature, though, especially when used in tandem with other lemmas e.g. whose arguments might need to be provided by hypotheses. That sort of interleaving effect can be very useful.

[Kyle Miller]

@Thomas Murrills Maybe a feature worth looking into is simp's discharger configuration. Doing simp (discharger := assumption) only is similar to simp only [*] if you're only wanting to use local hypotheses to close goals, but with the difference that assumption is more willing to do things up to defeq.