Lean: problems with visually indistinguishable instances

Question

I will describe a problem which I have in fact solved, but with considerable pain. My question is whether there are better methods for dealing with similar issues.

Lean was giving me messages that did not seem to make sense. After various manoeuvres to try to simplify and isolate the problem, I got a message like this (in which n1, r and k are all natural numbers).

invalid type ascription, term has type
  (n1 * r) ^ k = n1 ^ k * r ^ k
but is expected to have type
  (n1 * r) ^ k = ?m_1

Visually, it appears that the term h = mul_pow n1 r k in question has precisely the expected type, so this message is confusing. Eventually I entered set_option pp.all true, and thereby got a much longer and more explicit version of the above message. From this I saw that in the goal, multiplication and powers were defined in the usual way for natural numbers. However, in the term h there was all sorts of stuff about linear orders that I did not expect. I later worked out that I had inadvertently given ℕ an alternative monoid structure based on its structure as a lattice under the divisibility relation, and that that had been used by mul_pow when I defined h. After removing the import that defined this unwanted instance, the problem went away.

Answer 1

People ask these on the Lean Zulip and because they're hard to debug my instinct is usually to try to help. Here's a checklist which I think describes my usual approach to the problem.

1. When faced with issues of this nature the problem is almost always that the visually identical issues are not actually identical, like in your example; however sometimes they really are identical and the problem is a typeclass issue (e.g. the theorem you're trying to apply doesn't apply because even though the match should work, the theorem only applies to additive groups and you're trying to apply it to the naturals; unfortunately the error message you get is the same). So that's the first gotcha -- check that everything else is OK.

2. Set pp.all true and verify (by eye, or perhaps using a text editor) that the visually identical terms really are not identical. Sometimes this is harder than it looks, because definitionally equal diamonds in mathlib (e.g. a field is a ring is a semigroup v a field is a monoid is a semigroup or whatever) might not look syntactically equal. You can look at the error message with pp.all true on and then literally copy the terms which you suspect that Lean is claiming are not definitionally equal and see if Lean can prove they're equal with rfl. If it can't, you know you've isolated the problem. Sometimes the terms really still do look equal; when this happens it can be a universe issue.

3. Sometimes the problem is easy to solve: e.g. if one term mentions _inst_4 and other one doesn't, but the other term mentions _inst_5 and the first one doesn't, then you have done something like made R a normed_ring and a division_ring, and both of these extend ring so you've given R two distinct ring structures and that's your problem. The correct approach here would be to make R a normed_division_ring.

4. If the terms are small then you can usually stare at them and figure out what's going on. You might have found a diamond in mathlib, and if you have then we'd be interested to know about it on the Lean Zulip; please minimise and post a fully working example.

5. If the terms are huge then go back to step 2, take those two terms which Lean is complaining that it can't prove are equal, and try and prove they're equal in tactic mode using the congr' tactic. This will match all the parts of the terms which do align and you might well be left with two much simpler terms which aren't definitionally equal; that's your problem.

6. If all else fails, remember that set_option pp.all true is just actually the following 11 options:

* `pp.implicit true`
* `pp.proofs true`
* `pp.coercions true`
* `pp.notation false`
* `pp.universes true`
* `pp.full_names true`
* `pp.beta false`
* `pp.numerals false`
* `pp.strings false`
* `pp.binder_types true`
* `pp.generalized_field_notation false`

You can switch these options on one by one to see when things start diverging. The ones I usually start with are pp.notation, pp.implicit and pp.proofs.