Lots of 1 + 1 + 1 + 1

Stream: mathlib4

[Heather Macbeth]

Mario Carneiro said:

Thomas Murrills said:

One of the reasons might be the following: simp expands natural numbers into 1 + 1 + 1 + ... + 1 when they appear as arguments to the argument of Int.ofNat (sometimes). For example,

example (x : ℤ) : x = Int.ofNat (12 * 2) := by simp

leaves us with the goal

x = (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) * (1 + 1)

This is certainly a problem (which has been mentioned elsewhere although I don't think it has a dedicated issue for it), although I don't think it is specific to Int.ofNat. I think you can cause the same behavior using Nat.cast, it's a problem in simp and/or our simp set.

Some tactics currently produce a lot of 1 + 1 + 1 ...

@Thomas Murrills and @Mario Carneiro were just discussing this in the context of making norm_num work for OfScientific. And @Rob Lewis and I encountered this when using zify.

Mario pointed out that we should have a dedicated issue for this, which I would be happy to open, except that I don't understand the underlying cause. Mario, do you mean that somewhere there is a lemma wrongly tagged @[simp], and this needs to be tracked down?

[Mario Carneiro]

My working theory is that simp is applying the lemma \u (n + 1) = \u n + 1 to \u 5 by solving the unification problem 5 =?= ?n + 1 -> ?n := 4. This seems to be over-aggressive in this case, although I can see use cases for it when unfolding recursive functions on numerals

[Mario Carneiro]

One possible fix is just to say that \u (n + 1) = \u n + 1 is no longer allowed to be a default simp lemma and it has to be applied explicitly

[Mario Carneiro]

Another observation is that this should not be a legal unification at reducible transparency, because 4 + 1 = 5 is not (should not be?) a reducible rfl

[Heather Macbeth]

Interesting. I'd like to keep using simp with lemmas expressing (complicated) functions f (n + 1) in terms of f n, the way we could in mathlib3, like:

import algebra.big_operators.basic

open_locale big_operators

example : ∑ i in finset.range 5, i = 10 := by simp [finset.sum_range_succ]

[Heather Macbeth]

So it seems like we want a fix which is targeted to ↑.

[Heather Macbeth]

Mario Carneiro said:

One possible fix is just to say that \u (n + 1) = \u n + 1 is no longer allowed to be a default simp lemma and it has to be applied explicitly

Like this, if you think it would work.

[Heather Macbeth]

Although I suppose that in the example i just gave, finset.sum_range_succ was not a simp lemma, I had to provide it explicitly!

[Jireh Loreaux]

Heather, we can't target ↑ specifically anymore though, or do you mean Int.ofNat?

[Heather Macbeth]

Please take what I wrote as musing rather than a concrete suggestion; I don't understand the mathlib4 coercion setup yet!

[Thomas Murrills]

Here's one possible solution I found. It seems that simp tries Nat.cast_ofNat first, but the synthesized instance doesn't match the inferred instance, so it then tries Nat.cast_succ, which peels off a + 1. (This is the same issue that makes many Invertible lemmas unwieldy.)

It seems that using type inference instead and changing [NatCast R] to {_ : NatCast R} in the arguments to the Nat.cast_ofNat lemma (in Mathlib.Data.Nat.Cast.Defs) fixes the problem in the couple of cases I've tried:

@[simp, norm_cast] theorem Nat.cast_ofNat {_ : NatCast R} [Nat.AtLeastTwo n] :
  (Nat.cast (OfNat.ofNat n) : R) = OfNat.ofNat n := rfl

However, I know there are performance issues with ofNat (hence norm_num), so I don't know if this is a good solution. (Also it doesn't fix whatever's wrong with the norm_num extension I'm working on, so there's still something going on!)

[Yury G. Kudryashov]

Is there a document that describes how do ofNat, NatCast, Zero, One, Nat.atLeastTtwo etc interact?

[Gabriel Ebner]

but the synthesized instance doesn't match the inferred instance

I've also noticed that. It seems to be because Nat.cast is not reducible. And we have two instances for NatCast Int: one with Int.ofNat and one with Nat.cast. (Where the second of course uses Int.ofNat as well, but it's hidden behind the non-reducible Nat.cast definition.)

[Gabriel Ebner]

Is there a document that describes how do ofNat, NatCast, Zero, One, Nat.atLeastTtwo etc interact?

Not really.

• ofNat is the built-in function used for numeric literals (i.e., it is never applied to x + 1 or anything)
• NatCast is the coercion Nat → R
• Zero and One are the neutral elements in additive and multiplicative structures, resp.
• You should be able to write 0 and 1 for the neutral elements, so we have [Zero A] : OfNat A (nat_lit 0) and [One M] : OfNat M (nat_lit 1) instances
• You should also be able to write 42 in a ring, so we have [NatCast R] : OfNat R n. But that would be a diamond with the 0 and 1 instances, so we add an extra [AtLeastTwo n] argument to make sure the instance only gets used for numbers >= 2. Remember that 0 and Nat.cast 0 are not defeq in general.

[Thomas Murrills]

Gabriel Ebner said:

but the synthesized instance doesn't match the inferred instance

I've also noticed that. It seems to be because Nat.cast is not reducible. And we have two instances for NatCast Int: one with Int.ofNat and one with Nat.cast. (Where the second of course uses Int.ofNat as well, but it's hidden behind the non-reducible Nat.cast definition.)

Interesting! It seems this is a recurring issue.

Is there a reason that typeclass search doesn’t first try using type inference to get the instance? It seems like it’s going to type-infer the instance and check it for defequality to the synthesized instance when it’s possible to do so anyway, so why doesn’t typeclass search just use the available inferred instance (when it exists) instead of synthesizing something else and failing?

[Thomas Murrills]

Or, is the “right” solution making sure that everything has the right reducibility somehow? (I don’t know if this would take care of the problematic Invertible simp lemmas, though.)

[Gabriel Ebner]

Regardless of what we do about the not-absolutely-necessary defeq check in simp, we should still make the instances defeq. Though I can never quite remember the guidelines here. Usually we compare instances using semireducible transparency (because they're implicit arguments). I don't know what's going on here.

[Thomas Murrills]

Hmm…in the general case, does this mean micromanaging instances to avoid diamonds?

It would be helpful if we had some more tools for handling diamonds! I can see a couple of different overall directions for such tools, but have no idea which, if any, would be useful/unproblematic:

• change typeclass search (or simp?) so that we prefer ordinary type inference to typeclass search for filling [] args when possible, thus choosing the “right” instance whenever we can (would this cause performance issues? could we use some “simple” form of type inference that would be enough in most cases?)
• create linters that search for diamonds (not sure if this is even a tractable problem? or, on the other hand, if it already exists in some capacity?)
• have a way of satisfying such a linter by “establishing” defequality somehow among overlapping instances in the circumstances in which they overlap (do we have this?)
• have a procedure for automatically normalizing any overlapping instances somehow once we know they’re defeq

Would any of these be useful directions to pursue as a broader project?

[Thomas Murrills]

(Oops, I guess I lost focus…this counts as a separate topic, I think :) )

[Yury G. Kudryashov]

About unification vs typeclass search for simp. I'm porting topology.constructions, and one of the issues I have to work around is that simp can't unfold a definition (e.g., instTopologicalSpaceProd) that takes [TopologicalSpace α] if it is called with an argument which is not the instance infer_instance can find.