simpa using

Stream: general

[David Loeffler]

I just came across some weird behaviour with simpa using. I was under the impression that simpa using foo is supposed to be more robust than plain simp -- less likely to be broken by changes to the simp-lemma set. But I just encountered a case where adding a new simp lemma elsewhere in the library broke a proof of the form by simpa using foo, causing it to fail with the error match failed: no goals.

Given the nature of this bug it's rather hard to produce an MWE. You can reproduce it as follows:

• grab a copy of the current mathlib3
• in the file src/analysis/upper_half_plane/basic.lean, add the following lemma at line 314 (just after modular_S_smul):

@[simp] lemma modular_T_smul (z : ℍ) : modular_group.T • z = (1 : ℝ) +ᵥ z :=
begin
  suffices : ((modular_group.T • z : ℍ) : ℂ) = ↑((1 : ℝ) +ᵥ z), by rwa subtype.coe_inj at this,
  rw [coe_vadd, add_comm, special_linear_group_apply, coe_mk, modular_group.coe_T],
  simp only [of_apply, cons_val_zero, algebra_map.coe_one, complex.of_real_one, one_mul,
    cons_val_one, head_cons, algebra_map.coe_zero, zero_mul, zero_add, div_one],
end

• open src/number_theory/modular.lean and wait for it to recompile as far as line 327, which has the lemma

lemma im_T_smul : (T • z).im = z.im := by simpa using im_T_zpow_smul z 1

This will now fail, where it previously worked before. The new simp lemma in basic.lean means that im_T_smul can now be proved just with by simp, and apparently that causes by simpa using ... to fail.

The documentation says that simpa using h calls the simplifier on both h and the goal, and succeeds if they simplify to the same thing. My guess is that here the simplifier has simplified the goal away to nothing, then complains because it hasn't got anything to match h against. But surely an unexpectedly easy success shouldn't count as a failure!

Is this the intended behaviour, or am I correct that it's a bug in the simpa tactic?

[Martin Dvořák]

We were discussing simpa on Discord yesterday. If I understood correctly what I was told, it behaves as follows:
If simp succeeds on its own, then simpa will fail.

Calling simpa using foo is supposed to do something like simp [foo] at ⊢ foo, assumption and, therefore, if the simp itself manages to close the goal (possibly because a new simp lemma was added), then assumption has no goals to work on.

But surely an unexpectedly easy success shouldn't count as a failure!

This is exactly what I thought, and I was wrong.

[Eric Wieser]

It's not clear to me that modular_T_smul is a good simp lemma

[Eric Wieser]

At least, it doesn't seem confluent with the rest of the simp set

[David Loeffler]

@Eric Wieser Why do you say that? It was intended as a counterpart to the existing simp lemma

@[simp] lemma modular_S_smul (z : ℍ) : modular_group.S • z = mk (-z : ℂ)⁻¹ z.im_inv_neg_coe_pos

(S and T are the two standard generators of the modular group). Do you consider that one to be morally unsound too?

[Eric Wieser]

That looks like a weird simp lemma to me too, yes; usually we don't introduce constructors (mk) on the RHS like that

[Eric Wieser]

It's a good lemma but weird to be simp

[David Loeffler]

Martin Dvořák said:

But surely an unexpectedly easy success shouldn't count as a failure!

This is exactly what I thought, and I was wrong.

Well, I think we've established that it does count as a failure, but I think there's still a case to be made that it shouldn't! But tactic hacking is beyond my pay grade -- let's wait and see if any metaprogramming experts can weigh in on this.

[Eric Wieser]

Is this the intended behaviour, or am I correct that it's a bug in the simpa tactic?

To answer your question, this is intended behavior; it forces you to simplify downstream proofs (or re-evaluate the addition of a simp lemma) when the simp set gets bigger

[Eric Wieser]

David Loeffler said:

I was under the impression that simpa using foo is supposed to be more robust than plain simp -- less likely to be broken by changes to the simp-lemma set.

I think the correct conclusion is that simpa using foo is more robust than simp at foo, simp [foo]

[Adam Topaz]

I think this behaviour of simpa is fixed in lean4. You will get a warning telling you that simp suffices instead of an unhelpful failure

[David Loeffler]

Eric Wieser said:

To answer your question, this is intended behavior; it forces you to simplify downstream proofs (or re-evaluate the addition of a simp lemma) when the simp set gets bigger

If that's the case, then why do we have the rule against non-terminal simps? I thought the primary reason for that rule was that authors of downstream proofs were responsible for ensuring robustness against future additions to the simp set -- rather than anyone changing the simp set being responsible for changing a whole load of other people's downstream code! I think this principle is a good one, so I'm puzzled that the policy forsimpa is apparently the exact opposite of that for simp.

[Martin Dvořák]

I think the rule against non-terminal simps is not to prevent failures when the set of simp lemmas changes, but to make corrections easier (because the immediate goal of the simp is always known).

[Eric Wieser]

The problem with non-terminal simps is when simp, rw foo fails because foo no longer matches; and then the person editing the file has no idea what went wrong. If simp, rw foo fails because the goal is already solved it's trivial to fix the proof

[Patrick Massot]

David Loeffler said:

Martin Dvořák said:

But surely an unexpectedly easy success shouldn't count as a failure!
Well, I think we've established that it does count as a failure, but I think there's still a case to be made that it shouldn't!

Maybe I read too quickly but I certainly hope to get an error if simpa using foo succeeds without using foo. Leaving it like this would be a really really misleading proof script. Or are you saying something else?

[Eric Wieser]

Lean4 has a better approach to this where we can use warning messages for "this proof doesn't use foo" and errors for "this proof doesn't work", as Adam remarks above.

[David Loeffler]

Maybe I read too quickly but I certainly hope to get an error if simpa using foo succeeds without using foo. Leaving it like this would be a really really misleading proof script. Or are you saying something else?

Yes, you have read correctly what I am saying. It definitely does not seem reasonable to me that the result of a tactic succeeding too easily should be an opaque, incomprehensible error. However, it's clearly optimal to return an informative message instructing the user how to fix the issue, so I'm happy to concede that the Lean 4 solution is the best one.

[Patrick Massot]

Oh yes, better error messages are always welcome, but very often it's a lot of work.

[Yaël Dillies]

It emitting a warning is still annoying if you're using simpa to solve several goals in parallel: tac1; simpa

[Michael Stoll]

Maybe have a version of simpa that succeeds also when the simp was successful for cases like this?

[Eric Wieser]

I think simpa vs simpa using x has different considerations here. What does rwa do if no assumption is needed?

[Michael Stoll]

rwa seems to be happy in that case.

example (a b : ℤ) (h : a = 1) (h' : b = a) : a = 1 :=
begin
  rwa h,
end

succeds without complaint.

[Michael Stoll]

(As an aside: I think that rwa ... at h behaves a bit strangely, as it seems to only work when the goal can be closed by h after the rewrite. I.e., it seems to be equivalent to rw ... at h, exact h and not to rw ... at h, assumption. Is this impression correct, and if so, is the behavior indended?)

[Kevin Buzzard]

I did not have this impression, and this test seems to suggest that my model is OK (i.e. the goal is closed by a random assumption here)

example (a b c : ℕ) (P : Prop) (hP : P) (h' : a = b) (h : a = c) : P := by rwa h' at h

[Kevin Buzzard]

Here's the tactic code: I don't know much about tactics but I can guess what's going on here:

meta def rwa (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
rewrite q l cfg >> try assumption

(just right click on rwa to see it)

[Michael Stoll]

Ah, OK, sorry, I may have confused things.
I think, simpa [...] at h does not work as I would expect (i.e., like simp [...] at h, assumption) -- the syntax is not even accepted.

example (a b c : ℤ) (h : b = c) (h' : b = a) (h'' : c = 1) : a = 1 :=
begin
  simpa [h', h''] at h,
end

gives invalid 'begin-end' expression, ',' expected.

[Alex J. Best]

I'm confused why you want this? Surely simpa [...] using h does all you would ever need? Do you just think the syntax is inconsistent (indeed it sortof is but by now we all got used to it)?

[Michael Stoll]

Maybe my mental model of simpa was not quite correct. I guess I did not realize that simpa ... using h would also simplify h; my model was rather simp ..., exact h, with simplification of the goal only.
So thanks; I've learned something!

[Mario Carneiro]

Yaël Dillies said:

It emitting a warning is still annoying if you're using simpa to solve several goals in parallel: tac1; simpa

The linter framework is capable of handling this case. (Individual linters have to opt in to the behavior, but) if you use simpa twice with the same syntax then you only get the linter warning if both uses are unnecessary

[Mario Carneiro]

Some linter-like behavior is done directly in tactic execution, which will have the indicated failure mode. An example of a linter which does this correctly is the unreachable tactic linter - split <;> simp <;> rfl doesn't complain on rfl even if it was only used in one subgoal, but if simp closes both goals then you will get a warning on rfl saying it wasn't called

[Mario Carneiro]

(This is all regarding lean 4 behavior. In lean 3 the error message is the best we can do.)

[Yaël Dillies]

Oh perfect! Then I'm very happy with the warning solution.