Mathlib4 `calc` issue?

Stream: mathlib4

[David Pearce]

Hi, I was working through converting a proof to calc style and came across this strangeness:

--import Mathlib.Tactic

def pow256_shr (n : Nat) (m : UInt8) (k : Nat) (p : n < 256^k) : (m.val * 256^k + n < 256^(k+1)) := by
  have mLt : (m.val : Nat) < 256 := m.val.isLt
  calc
    _ < 256 * 256^k := by sorry
    _ = 256^(k+1) := by sorry

On Lean 4.7.0 the above succeeds (ignoring sorry) for now. However, if I uncomment the import Mathlib.Tactic line, then it fails. Here, Mathlib is imported with this line in the lakefile.lean:

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"v4.7.0"

I'm confused what's going on here?

[Eric Wieser]

This works:

import Mathlib.Tactic
def pow256_shr (n : Nat) (m : UInt8) (k : Nat) (p : n < 256^k) :
    (m.val.val * 256^k + n < 256^(k+1)) := by
       -- ^^^^ added this
  have mLt : (m.val : Nat) < 256 := m.val.isLt
  calc
    _ < 256 * 256^k := by sorry
    _ = 256^(k+1) := by sorry

[Eric Wieser]

The issue is that the new imports changed the meaning of the theorem!

[Patrick Massot]

I think that not providing the LHS on the first calc line is also not helping Lean.

[Eric Wieser]

It's already too late by then though, the statement was wrong as soon as the by began

[Eric Wieser]

With Mathlib.Tactic imported, the type of the 256 is now Fin 256 not Nat; and so the theorem is false!

[Patrick Massot]

Sure, these are independent comments.

[Eric Wieser]

I've not seen an algebraic case where dropping the first calc term causes an issue

[Eric Wieser]

(It certainly happens with morphisms, where you have to give the LHS on every line, repeating the RHS of the previous line!)

[David Pearce]

Eric Wieser said:

With Mathlib.Tactic imported, the type of the 256 is now Fin 256 not Nat; and so the theorem is false!

So, this is the key thing. Using Mathlib changes the types given to constants? That seems ... unexpected to me.

[Yury G. Kudryashov]

You don't specify types of LHS and RHS, so Lean has to guess. Mathlib adds more instances, so Lean can put everything to Fin 256 now instead of casting to Nat.

[Yury G. Kudryashov]

Instead of adding extra .val, you can specify that LHS has type Nat.

[Kyle Miller]

The rule for arithmetic is that it looks at the whole arithmetic expression tree, finds the types of everything (if known), and then figures out what everything can be coerced to. It turns out m.val is a Fin UInt8.size, so it goes with that.

It doesn't affect anything here, but this algorithm can go wrong if there's a loop in the coercions. We fixed this with ZMod the last time this discussion came up, but Fin is not well-behaved: (((16 : Nat) : Fin 5) : Nat). We'll have to fix that one...

[Kevin Buzzard]

In my mind the difference between ZMod and Fin is that ZMod has a coercion from Nat but no coercion to Nat (it's the quotient), and Fin has a coercion to Nat but not a coercion from Nat (it's the subobject). However I'm aware that this doesn't correspond to reality -- people want to load more and more structure onto Fin n to get it to be some kind of substitute for ZMod.

[Yury G. Kudryashov]

Currently Fin has coercions both ways.

[Yury G. Kudryashov]

On the one hand, this (and related OfNat instances) allow expressions like (3 : Fin 5). OTOH, sometimes this leads to confusion.

[Kyle Miller]

You don't need the coercion to make expressions like (3 : Fin 5) work though, and the bidirectional coercion causes issues with elaboration:

import Mathlib.Tactic

#eval decide <| (3 : Fin 2) = (3 : Nat)
-- true
#eval decide <| (3 : Nat) = (3 : Fin 2)
-- false

It's not good that this depends on imports. Without the import, both are false.

[Kyle Miller]

This one's because mathlib has docs#Fin.instCommRing, which enables the Nat -> Fin n coercion, but since Fin is a subtype, it has a Fin n -> Nat coercion too.

[Kyle Miller]

Johan had fixed this for ZMod by removing the ZMod n -> Nat coercion here, but that's not an option for Fin. It's meant to be a subtype of the natural numbers.

[Kyle Miller]

Some thoughts about solving this problem:

• We could make Fin.instCommRing not be a global instance, but that seems heavy handed.
• We could make the NatCast coercions somehow be opt-in. I'm not sure what that would look like (is it instances you activate? an explicit coercion notation you use?)
• We could get the core expression tree elaborator to be more picky with what coercions it should consider. There are valid reasons for inserting Fin n -> Nat coercions, but inserting non-injective coercions seems problematic.

[Yury G. Kudryashov]

Fin is a custom structure, not a subtype (though we think about it as a subtype).

[Yury G. Kudryashov]

I would vote for removing Fin.instCommRing. We can have it as a scoped instance (e.g., if someone will write a norm_num extension for Fin)

[Yury G. Kudryashov]

But I like the idea "if you want a ring, use ZMod". Note: I may change my mind when I see the diff.