simp can prove it

Stream: mathlib4

[Reid Barton]

Did the "simp can prove it" linter not exist in mathlib 3?

[Eric Wieser]

It existed in a weaker form in mathlib3 for things tagged @[simp]

[Eric Wieser]

"simp can prove it" isn't a sufficient condition to make a simp lemma unecessary

[Reid Barton]

Then why is there a linter for that in mathlib4?

[Eric Wieser]

Maybe simp is clever enough that it now is sufficient?

[Eric Wieser]

The case I had in mind is docs#submodule.coe_zero vs docs#submodule.coe_eq_zero

[Eric Wieser]

Simp can obviously prove the former with the latter

[Eric Wieser]

But the former is needed to simplify f ↑0 = f 0, unless simp now knows to use coe_eq_zero.mpr rfl

[Reid Barton]

OK, I will just assume that whatever the linter says is correct

[Reid Barton]

and that it might differ from lean 3 for no reason

[Reid Barton]

It seems like the Lean 3 linter doesn't always work correctly, e.g., simp can prove list.reverse_singleton (and there is no nolints.txt entry for it)

[Reid Barton]

I also wonder about the wisdom of this linter in general? e.g. it fails on

@[simp] theorem indexOf_nil (a : α) : indexOf a [] = 0 := rfl

with the message

#check @List.indexOf_nil /- simp can prove this:
  by simp only [List.find?, List.not_mem_nil, not_false_iff, List.indexOf_of_not_mem, List.length_nil]

But isn't it better to do 1 simp step than 5?

[Chris Hughes]

I came across an interesting false positive for this linter today. simp can prove the lemma x + x = x in Algebra.Tropical.Basic but only by rewriting it using the lemma x + y = x ↔ x ≤ y, so the lemma is still required to prove f (x + x) = f x for example.

[Reid Barton]

btw, when the proof is rfl, doesn't @[simp] also affect the behavior of dsimp? But dsimp can't prove it

[Reid Barton]

I mean I guess it could be the case that all 5 of those lemmas are definitional equalities, but say they aren't

[Johan Commelin]

I guess that's good evidence that the "simp can prove it" linter should be less strictly enforced. At least in its current state.

[Reid Barton]

As I mentioned to Johan earlier, it's also nice from a modularity perspective to be able to declare that e.g. indexOf_nil should be proven by simp, and not have to delete the attribute and rely on it being proven by a jenga tower of 5 other simp lemmas

[Reid Barton]

At the moment I'm going through Data.List.Basic and leaving a commented-out -- @[simp] to lemmas affected by this, since I'm not convinced that just removing the attribute is sensible

[Reid Barton]

Of course we could also nolint these.

[Sebastien Gouezel]

Suppose that you put the simp attribute on indexOf_nil. In concrete situations where this lemma could be used by simp, will it fire or will the other lemmas (that were used to prove indexOf_nil) fire before? In the latter situation, there is indeed no use for the simp attribute on indexOf_nil, because it will never be used.

[Yaël Dillies]

In that specific case, dsimp justifies tagging indexOf_nil already.

[Heather Macbeth]

Reid Barton said:

As I mentioned to Johan earlier, it's also nice from a modularity perspective to be able to declare that e.g. indexOf_nil should be proven by simp, and not have to delete the attribute and rely on it being proven by a jenga tower of 5 other simp lemmas

Maybe we can make a new attribute simp_can_prove_it, change the simp on these lemmas to simp_can_prove_it, and have a linter which verifies that simp can prove them!

[Yaël Dillies]

In general, it would be good if the simp nf linter was checking whether a refl lemma tagged with simp can be proved by dsimp, instead of merely by simp.

[Yaël Dillies]

That would remove a bunch of nolints from mathlib.

[Johan Commelin]

/me votes for simpCanProveItThankYouVeryMuch

[Yaël Dillies]

Ah, but maybe the linter can't access the information of whether a declaration is tagged with the _refl_ attribute (or whichever one we use in mathlib)

[Yaël Dillies]

This lack of attribute inspection is a real problem :frown:

[Johan Commelin]

But it can find all decls tagged with a given attribute, right? That's all you need in this case.

[Reid Barton]

Yaël Dillies said:

In that specific case, dsimp justifies tagging indexOf_nil already.

And even if this was not the case, there is a declarative purpose even if there is no functional effect (lots of stuff we do is useless, after all).

[Yaël Dillies]

Very profound. I must review my life choices.

[Reid Barton]

Done for now; there are 4 more linter errors (the weird ones involving simp lemmas not simplifying themselves, and the private simp lemma one).

[Johan Commelin]

Are the "not simplifying themselves" cases due to timeouts? Or some other reason?

[Reid Barton]

I don't think that was the reason. They looked sort of complicated

[Reid Barton]

one had an argument with a default value involving a tactic and stuff

[Eric Wieser]

Chris Hughes said:

I came across an interesting false positive for this linter today. simp can prove the lemma x + x = x in Algebra.Tropical.Basic but only by rewriting it using the lemma x + y = x ↔ x ≤ y, so the lemma is still required to prove f (x + x) = f x for example.

The mathlib 3 linter is written in a way that allows this; it instead asks simp to simplify the LHS of the relation, and only complains if the result is the RHS. Crucially, it doesn't give the lemma the LHS and RHS at the same time, which is necessary for your example

[Reid Barton]

Oh I think this probably explains some of the other cases I found where "simp could prove it" in Lean 4 but not Lean 3.

[Johan Commelin]

Have people been throwing away @[simp] too often during the port, because of this linter nagging?

[Gabriel Ebner]

Chris Hughes said:

I came across an interesting false positive for this linter today. simp can prove the lemma x + x = x in Algebra.Tropical.Basic but only by rewriting it using the lemma x + y = x ↔ x ≤ y, so the lemma is still required to prove f (x + x) = f x for example.

This is not at all what's happening here.

#check @add_self /- simp can prove this:
  by simp only [le_refl, Tropical.add_eq_left] -/

And add_eq_left is the conditional simp lemma x ≤ y → x + y = x. The le_refl is only used to discharge the hypothesis. So this will also work in f (x + x).

[Gabriel Ebner]

Eric Wieser said:

Chris Hughes said:

I came across an interesting false positive for this linter today. simp can prove the lemma x + x = x in Algebra.Tropical.Basic but only by rewriting it using the lemma x + y = x ↔ x ≤ y, so the lemma is still required to prove f (x + x) = f x for example.

The mathlib 3 linter is written in a way that allows this; it instead asks simp to simplify the LHS of the relation, and only complains if the result is the RHS. Crucially, it doesn't give the lemma the LHS and RHS at the same time, which is necessary for your example

The mathlib 4 linter too. (Well technically it's the std4 linter now. :shrug:)

[Chris Hughes]

Gabriel Ebner said:

Chris Hughes said:

I came across an interesting false positive for this linter today. simp can prove the lemma x + x = x in Algebra.Tropical.Basic but only by rewriting it using the lemma x + y = x ↔ x ≤ y, so the lemma is still required to prove f (x + x) = f x for example.

This is not at all what's happening here.

#check @add_self /- simp can prove this:
  by simp only [le_refl, Tropical.add_eq_left] -/

And add_eq_left is the conditional simp lemma x ≤ y → x + y = x. The le_refl is only used to discharge the hypothesis. So this will also work in f (x + x).

I've seen a lot where simp proves it with these conditional lemmas. Is there any significant performance penalty to using a lot of these conditional lemmas to prove things instead of unconditional lemmas?

[Kevin Buzzard]

This also comes up in mathlib4#1307 -- "simp can prove this" linter errors in lemmas which are tagged simp in mathlib3 and either the mathlib3 linter missed them or some unfolding is being done more eagerly. What are we doing here? Just removing the @[simp] tag and blundering on?

[Heather Macbeth]

:ping_pong:
Heather Macbeth said:

Maybe we can make a new attribute simp_can_prove_it, change the simp on these lemmas to simp_can_prove_it, and have a linter which verifies that simp can prove them!

This idea was kind of a joke but it might also be useful; it would serve a similar purpose to assert_not_exists.

[Heather Macbeth]

For now, I think we should at least add a porting note. But it shouldn't be hard to invent a dummy attribute simp_can_prove_it and replace bad simp tags with that, even if we don't immediately write any meta code associated to the new attribute.

[Johan Commelin]

@Kevin Buzzard At the very least, please leave a trace: -- @[simp] -- Porting note: simp can prove this.

[Johan Commelin]

But typically, it seems that you should investigate why simp can suddenly prove this. In Data.List.Basic it was often because of a quasi-dubious simp lemma in Std.

[Kevin Buzzard]

Right -- that was what I suggested in the PR.