Type mismatch after moving instNatCast to Lean

Stream: lean4 dev

[Tobias Grosser]

I am currently flashing out some of the BitVec <-> Fin interfaces in Lean working on this patch: https://github.com/leanprover/lean4/pull/5680/files.

[Tobias Grosser]

Unfortunately, I get the seemingly unrelated error in FloatArray:

  type mismatch
    fun xs i h => xs.uget i h
  has type
    (xs : FloatArray) → (i : USize) → ↑i.val < xs.size → Float : Type
  but is expected to have type
    (xs : FloatArray) → (i : USize) → i.val < ↑xs.size → Float : Type

This code worked before , but fails after adding:

  instance instNatCast [NeZero n] : NatCast (Fin n) where
  natCast n := Fin.ofNat'' n

[Tobias Grosser]

This error arises in these lines (where I added explicit type annotations to simplify debugging)

instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
  getElem xs i (h : @LT.lt Nat instLTNat (↑i.val) xs.size) := xs.uget i h

[François G. Dorais]

The instance at https://github.com/leanprover/lean4/blob/1d8555fe0bdd02c82664446309b2e167ac89c9e9/src/Init/Data/FloatArray/Basic.lean#L65C1-L67C1 should be:

instance : GetElem FloatArray USize Float fun xs i => i.toNat < xs.size where
  getElem xs i h := xs.uget i h

The issue is that i.val is actually Fin USize.size instead of Nat, which picks out the wrong coercion.

[Tobias Grosser]

This seems to work. Thank you, @François G. Dorais.

[Notification Bot]

Tobias Grosser has marked this topic as resolved.

[Tobias Grosser]

Actually, now I am in an entire new mess.

[Tobias Grosser]

It seems this cast lemmas has broken many things in Fin/Lemmas.lean.

[Tobias Grosser]

/-
application type mismatch
  Nat.le_of_lt_succ (is_lt i)
argument
  is_lt i
has type
  ↑i < n + 1 : Prop
but is expected to have type
  ↑i < (↑↑n).succ : Prop
-/
theorem is_le (i : Fin (n + 1)) : i ≤ n := Nat.le_of_lt_succ i.is_lt

[Notification Bot]

Tobias Grosser has marked this topic as unresolved.

[François G. Dorais]

It's probably not ideal to have casts both ways between Nat and Fin. It's a coin toss which applies in each case.

[Tobias Grosser]

Right.

[Tobias Grosser]

I took this code from mathlib (https://github.com/leanprover-community/mathlib4/blob/81d66bb893988a10f0e7f3b5baa2f8bc0f35993f/Mathlib/Data/Fin/Basic.lean#L432), where this setup seems to work.

[Mario Carneiro]

Well not really, Kyle has frequently complained about essentially this issue. You should avoid binary operators between a Nat and a Fin unless you have a ↑ on one side because it's ambiguous.

[Tobias Grosser]

Interesting.

[Tobias Grosser]

I guess this means moving NatCast to Lean proper is a bad idea.

[Tobias Grosser]

Thank you for the insight.

[Mario Carneiro]

I think NatCast is already in lean proper?

[Mario Carneiro]

it just doesn't have an instance for Fin until it gets one indirectly in mathlib because it's a ring

[Tobias Grosser]

NatCast ist, but the following instance is not:
https://github.com/leanprover-community/mathlib4/blob/81d66bb893988a10f0e7f3b5baa2f8bc0f35993f/Mathlib/Data/Fin/Basic.lean#L432C1-L433C29

instance instNatCast [NeZero n] : NatCast (Fin n) where
  natCast n := Fin.ofNat'' n

[Tobias Grosser]

(Also, it seems to get this instance directly, AFAIU the code above)

[Mario Carneiro]

ah, that may be true but I think that's just to avoid diamond issues

[Tobias Grosser]

Right.

[Tobias Grosser]

I am working towards upstreaming: https://github.com/opencompl/lean-mlir/blob/main/SSA/Projects/InstCombine/ForMathlib.lean and am trying to see where each theorem fits best (Lean vs. Mathlib)

[Tobias Grosser]

The objective is to define:

instance : CommRing (BitVec w) :=
  toFin_injective.commRing _
    toFin_zero toFin_one toFin_add toFin_mul toFin_neg toFin_sub
    toFin_nsmul toFin_zsmul toFin_pow toFin_natCast toFin_intCast

[Tobias Grosser]

To unbreak https://github.com/leanprover/lean4/pull/5323.

[Mario Carneiro]

well, I see a ring-shaped issue with upstreaming that

[Tobias Grosser]

Can you expand on this.

[Mario Carneiro]

CommRing is largely agreed to be the domain of mathlib

[Mario Carneiro]

so if you need that specifically then I don't think it can be upstreamed

[Tobias Grosser]

Ah, I want to upstream the CommRing instance into Mathlib.

[Mario Carneiro]

oh, well then there are no problems, and also this thread is in the wrong stream?

[Tobias Grosser]

Henrik's patch to Lean4 which transitions uint to bitvec breaks the mathlib build, due to a missing CommRing instance for BitVec.

[Tobias Grosser]

So this thread covers both Lean4 and Mathlib.

[Tobias Grosser]

So I am trying to break apart the changes that must be made to keep things in the right domains.

[Tobias Grosser]

AFAIU BitVec lemmas should go into lean, but CommRing into mathlib.

[Mario Carneiro]

I'm confused, can you explain the context and situation here?

[Tobias Grosser]

Right, some context might be useful. :smile:

[Tobias Grosser]

There is this Lean4 patch currently proposed to Lean: https://github.com/leanprover/lean4/pull/5323

[Mario Carneiro]

hm, I'm already mild negative on this, I thought we didn't want to involve BitVecs in math

[Tobias Grosser]

I see.

[Tobias Grosser]

So you feel uint counts as 'math'?

[Mario Carneiro]

yes

[Mario Carneiro]

at least, it's going to make it a lot harder to avoid bitvecs in unrelated code going forward

[Mario Carneiro]

but anyway, I guess this is an independent discussion. How does this result in needing a CommRing instance on BitVec?

[Mario Carneiro]

(which by the way clearly looks like "involving bitvecs in math" so my worries are not unfounded)

[Tobias Grosser]

The CommRing instance of UInt requires updating: https://github.com/leanprover-community/mathlib4/blob/lean-pr-testing-5323/Mathlib/Data/UInt.lean#L77

[Mario Carneiro]

Some time ago there was a push to get mathlib to avoid even mentioning the type BitVec, so this is a bit of reversal

[Tobias Grosser]

So it seemed natural to me to first define CommRing for BitVec and then using this definition.

[Mario Carneiro]

but that said I think we should have the instance

[Mario Carneiro]

but shouldn't the proof basically look just like those UInt proofs? Transfer an injective function and then all the proofs are rfl

[Mario Carneiro]

also, what is up with this deprecation?

warning: ././././Mathlib/Data/UInt.lean:26:0: `UInt8.eq_of_val_eq` has been deprecated, use `UInt8.eq_of_toBitVec_eq` instead

The API should let me step over the bitvec step if I want to

[Tobias Grosser]

I guess there are several parts of this conversation. I am mostly interested in defining CommRing (BigVec w).

[Mario Carneiro]

I think the answer to that is to just upstream everything to mathlib

[Tobias Grosser]

To keep the conversation focused (and complexity at a level that is suitable for my mathlib skills), maybe its best if I create a simple PR for the CommRing instance.

[Tobias Grosser]

I will propose a patch for https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/BitVec.lean.

[Tobias Grosser]

Thank you.

[Henrik Böving]

Mario Carneiro said:

but shouldn't the proof basically look just like those UInt proofs? Transfer an injective function and then all the proofs are rfl

There is a single proof that is not refl as explained in the PR

[Henrik Böving]

Mario Carneiro said:

but anyway, I guess this is an independent discussion. How does this result in needing a CommRing instance on BitVec?

Using the BitVec instance to define the UInt one should be the right way to go because we want to have BitVec in between UInt and Fin now no?

[Henrik Böving]

Mario Carneiro said:

also, what is up with this deprecation?

warning: ././././Mathlib/Data/UInt.lean:26:0: `UInt8.eq_of_val_eq` has been deprecated, use `UInt8.eq_of_toBitVec_eq` instead

The API should let me step over the bitvec step if I want to

You can do that by using the proper lemma in BitVec, I don't think we shoudl expose the transitive closure of our abstraction level shfit lemmas as explicit lemmas

[Tobias Grosser]

OK, the CommRing instance seems to work: https://github.com/leanprover-community/mathlib4/pull/17700

[Tobias Grosser]

I am currently cleaning this up.

[Mario Carneiro]

Henrik Böving said:

Mario Carneiro said:

also, what is up with this deprecation?

warning: ././././Mathlib/Data/UInt.lean:26:0: `UInt8.eq_of_val_eq` has been deprecated, use `UInt8.eq_of_toBitVec_eq` instead

The API should let me step over the bitvec step if I want to

You can do that by using the proper lemma in BitVec, I don't think we shoudl expose the transitive closure of our abstraction level shfit lemmas as explicit lemmas

We should if that's the API people were using before

[Mario Carneiro]

just because core wants to define things this way doesn't mean downstream users want to deal with this too

[Mario Carneiro]

There are now 3 steps from UInt8 to Nat, I don't want to have to apply 3 lemmas instead of 1

[Henrik Böving]

Well there should just, not be a need to do this in almost all situations after the API is finished.

[Mario Carneiro]

Henrik Böving said:

Mario Carneiro said:

but shouldn't the proof basically look just like those UInt proofs? Transfer an injective function and then all the proofs are rfl

There is a single proof that is not refl as explained in the PR

Not explained as far as I can tell, but mentioned once. What's the issue exactly?

[Henrik Böving]

https://github.com/leanprover/lean4/pull/5323#issuecomment-2407062190

I addressed all comments and everything in batteries and mathlib apart from a singular sorry here: https://github.com/leanprover-community/mathlib4/blob/lean-pr-testing-5323/Mathlib/Data/UInt.lean#L77 is fixed. This was previously rfl but is now not rfl anymore. It also appears there is very little API around this thing so I don't quite see how to do a nice proof here without definition bashing.

[Mario Carneiro]

Henrik Böving said:

Well there should just, not be a need to do this in almost all situations after the API is finished.

There should not be a need to relate unsigned integers to natural numbers?

[Mario Carneiro]

@Henrik Böving yes I see that, that's what I call a mention

[Mario Carneiro]

it's just restating what you said

[Mario Carneiro]

what is not refl and why?

[Henrik Böving]

The proof that is linked?

[Mario Carneiro]

I see a sorry, do you want me to compile it to find out the goal?

[Mario Carneiro]

it also doesn't answer the why

[Mario Carneiro]

which change broke it?

[Henrik Böving]

Having the redefinition of UInt in terms of BitVec and then fixing the file you are looking at in a way that Kim deemed reasonable broke it.

[Mario Carneiro]

this is completely not answering the question

[Mario Carneiro]

you are saying all of the things I knew before looking at the PR

[Mario Carneiro]

what specifically did you change and why is it causing this breakage

[Tobias Grosser]

I guess I can compile it and see what's going on. Might be a learning experience for me as well.

[Henrik Böving]

The proof state is

x✝ : ℤ
⊢ (↑x✝).val = ↑x✝

where the lhs casts Int to UInt8 and the rhs casts int to Fin. I presume that the fact that .val is now not the only projection of the structure anymore broke the rfl thing, I do not know why it broke precisely.

[Tobias Grosser]

I can reproduce this proof state in my build:

x✝ : ℤ
⊢ (↑x✝).val = ↑x✝

[Tobias Grosser]

Francois advised me to use .toNat instead of .val at some point.

[Tobias Grosser]

Maybe the same ambiguity is biting us here.

[Mario Carneiro]

I don't think ambiguity can explain a non-refl proof, this is a change of definitions

[Tobias Grosser]

How do I track this down?

[Tobias Grosser]

https://github.com/leanprover-community/mathlib4/commit/0aa61183b0ba32a07b90fc6fb5fea72f876fde17 seems harmless.

[Mario Carneiro]

So if we work out the definitions:

• ↑(x : Int) : UInt8 is defined as mk (↑(x : Int) : BitVec 8) (note that it's BitVec and not Fin now)
• which resolves via the IntCast (BitVec 8) instance, which comes from... nowhere?

[Mario Carneiro]

master has a CommSemiring instance but not a CommRing instance for BitVec

[Mario Carneiro]

so I'm not sure who is providing this intcast instance

[Mario Carneiro]

basically the problem in 0aa6118 is that line 70 (which was not touched) uses the mk function which has silently changed type

[Tobias Grosser]

Right.

[Tobias Grosser]

But should this line not break, if there is no IntCast instance for UInt via BitVec?

[Mario Carneiro]

but I'm not sure how this typechecks in the first place

[Mario Carneiro]

that line should be a type error if there is no IntCast instance for BitVec

[Mario Carneiro]

so such an instance must exist somehow

[Henrik Böving]

Yeah it sits in core

[Mario Carneiro]

and its definition is apparently not defeq to the original definition which used mod on Fin n

[Henrik Böving]

https://loogle.lean-lang.org/?q=IntCast+%28BitVec+%3Fw%29

[Tobias Grosser]

Interesting.

[Tobias Grosser]

Thank you for understanding this.

[Mario Carneiro]

So what is the IntCast (Fin n) definition defeq to?

[Mario Carneiro]

that is the RHS of the goal

[Mario Carneiro]

it seems like the LHS should be defeq to x % Int.ofNat 256 which looks okay

[Tobias Grosser]

I am afraid I don't fully follow.

[Tobias Grosser]

How did you derive this?

[Mario Carneiro]

Because of structure eta, we only really care about the nat part of the expression, the rest is just proofs. So all the mk wrappers do nothing, and val just cancels those wrappers out anyway. The only part that matters is the nat part of src#BitVec.ofInt , which is (i % (Int.ofNat (2^n))).toNat

[Mario Carneiro]

actually I guess the .toNat part could also be troublesome

[Mario Carneiro]

there was something in the PR description about removing some variant of mod, maybe this is the issue?

[Tobias Grosser]

I feel the mod issue is unrelated.

[Henrik Böving]

That variant of mod was removing UIntx mod Nat in favor of just having UintX mod UIntX

[Tobias Grosser]

The definition of BitVec.ofInt is historically grown.

[Tobias Grosser]

Where do I find the intCast instance of Fin, which was used before?

[Tobias Grosser]

Loogle does not help: https://loogle.lean-lang.org/?q=IntCast+%28Fin+%3Fw%29

[Mario Carneiro]

Henrik Böving said:

That variant of mod was removing UIntx mod Nat in favor of just having UintX mod UIntX

That's not a valid replacement?

[Mario Carneiro]

if you mod by something larger than 256 it's not equivalent to reducing the denominator first

[Mario Carneiro]

but I don't think it's implicated here, at least I haven't found any calls to modn appearing in these functions

[Mario Carneiro]

what does #synth IntCast (Fin 256) give you @Tobias Grosser ?

[Tobias Grosser]

Ring.toIntCast

[Henrik Böving]

modn was only used to define left and right shift such that it doesn't cause UB in core and that def can be easily done with just UInt

[Mario Carneiro]

you should be able to hover the expression until you find something that's actually about Fin

[Mario Carneiro]

I don't think it's about UB, the function has different semantics

[Henrik Böving]

It is about UB in core

[Mario Carneiro]

I agree that in the case of modding by a constant like 8 it makes no difference

[Henrik Böving]

Shifting to the left on a UIntX by more than X is UB. So the shifter is changed. This was previously modn and is now just mod

[Tobias Grosser]

@Ring.toIntCast (Fin 256) CommRing.toRing : IntCast (Fin 256)

[Mario Carneiro]

that's C semantics, not lean

[Tobias Grosser]

@CommRing.toRing (Fin 256) (Fin.instCommRing 256)

[Mario Carneiro]

in lean shifting to the left should just result in multiplication by 2^n and then modding by the byte size

[Henrik Böving]

Yes, but the Lean function has to reflect what we implemented in the C runtime. And this is what is implemented in the C rutnime.

[Henrik Böving]

I've been over this discussion already internally and it was decided to keep it the way it is at least for now.

[Mario Carneiro]

suggesting that users replace uses of modn with mod is dangerous because it's not semantics preserving

[Tobias Grosser]

Mario Carneiro said:

suggesting that users replace uses of modn with mod is dangerous because it's not semantics preserving

Interesting observation.

[Mario Carneiro]

if you want to remove native support for modn it can still be simulated with a branch on the value

[Mario Carneiro]

if h : b < UIntN.size then a % <<b, h>> else a

[Henrik Böving]

You can discuss that one out with reviewers on the PR if you like.

[Mario Carneiro]

Tobias Grosser said:

@CommRing.toRing (Fin 256) (Fin.instCommRing 256)

I don't see anything in src#Fin.instCommRing which would give the value of intCast, so it's probably getting the default implementation, which is not a mod expression

[Tobias Grosser]

Where do I find the default implementation?

[Henrik Böving]

Besides, it's not like modn is deleted, it's just that there is this signular change of not havign modn coming up in shfits anymore and generally preferring mod over modn in API lemmas when applicable.

[Tobias Grosser]

/-- Default value for `IntCast.intCast` in an `AddGroupWithOne`. -/
protected def Int.castDef {R : Type u} [NatCast R] [Neg R] : ℤ → R
  | (n : ℕ) => n
  | Int.negSucc n => -(n + 1 : ℕ)

[Mario Carneiro]

Henrik Böving said:

Besides, it's not like modn is deleted, it's just that there is this signular change of not havign modn coming up in shfits anymore and generally preferring mod over modn in API lemmas when applicable.

In this case, modn should either not be deprecated or should have a deprecation which does not just point at UintN.mod but uses text to explain what the options are

[Mario Carneiro]

Replacing modn with mod in shifts is perfectly fine, the part I find questionable is the removal of the functions (which may have been in use downstream)

[Mario Carneiro]

and I have confirmed that Fin.instCommRing uses src#Int.castDef

[Henrik Böving]

Henrik Böving said:

You can discuss that one out with reviewers on the PR if you like.

^

[Henrik Böving]

There is two people on the PR that think this change is fine, you don't think it's fine, I don't care what happens as long as it gets merged.

[Tobias Grosser]

Mario Carneiro said:

and I have confirmed that Fin.instCommRing uses src#Int.castDef

Right.

[Tobias Grosser]

I guess now we now why the casts have changed semantics.

[Tobias Grosser]

I feel the new definition is a bit more correct than the old one.

[Tobias Grosser]

Meaning, it implements two's complement conversion or sth similar.

[Tobias Grosser]

I guess it is obvious to you why the refl proof breaks and how to fix it?

[Mario Carneiro]

The implementation of intCast for Fin should also use mod

[Mario Carneiro]

I think you just need to add a line to src#Fin.instCommRing for this

[Mario Carneiro]

although maybe it is better to separately define IntCast (Fin n) and then add it to the structure before the where

[Tobias Grosser]

And I guess I would define Fin.ofInt as well?

[Mario Carneiro]

surely this already exists?

[Tobias Grosser]

https://loogle.lean-lang.org/?q=Fin.ofInt

[Tobias Grosser]

unknown identifier 'Fin.ofInt'

[Mario Carneiro]

@loogle Int -> Fin ?n

[loogle]

:shrug: nothing found

[Mario Carneiro]

src#BitVec.ofInt seems to be reinventing such a function

[Mario Carneiro]

in fact I think you could just copy and paste that function with n instead of 2^n

[Tobias Grosser]

Like this:

protected def ofInt (n : Nat) (i : Int) : Fin n := ⟨(Int.toNat (i % (Int.ofNat n))), by sorry⟩

[Mario Carneiro]

yes, and then instance intCast : IntCast (Fin n) := \<Fin.ofInt\> and instance : CommRing (Fin n) := { ..., Fin.intCast n with ... }

[Tobias Grosser]

OK.

[Mario Carneiro]

hopefully you should be able to confirm that adding those lines makes the sorry in question rfl again

[Mario Carneiro]

Although, if the goal is to make this file only go via toBitVec instead of val, then probably the CommRing UIntN proof should be lifting from toBitVec (which would make this proof rfl anyway since now both sides will be using the bitvec ofInt implementation), but you will also need that CommRing (BitVec n) instance in that case

[Henrik Böving]

That was the original goal of this thread as explained above yes.

[Tobias Grosser]

OK, this gives a clear path forward.

[Tobias Grosser]

Thanks a lot.

[Henrik Böving]

But thanks for figuring out the defeq issue for us :thumbs_up:

[Eric Wieser]

Should the definition use docs#Int.natMod ?

[Mario Carneiro]

it's defeq to it either way