Type Mismatch when Simplifying Constants

Stream: lean4

[David Pearce]

I've encountered an unexpected type mismatch issue. Here's a simplified example:

abbrev UInt4 := Fin 16
abbrev U4_MAX : UInt4 := {val:=15, isLt:=(by simp_arith)}

@[simp]
def sum(items: List (Fin n))(p:n>0) : Fin n :=
  match items with
  | h::t => h + (sum t p)
  | [] => {val:=0, isLt:=(by simp_arith [p])}

example(p:16>0) : sum (1::2::[]) p = 3  :=
by
  simp_arith

This works fine, and just illustrates the setup. So then I want to add another test ...

example(p:16>0) : sum (1::U4_MAX::[]) p = 0  :=
by
  --unfold U4_MAX
  simp_arith

Now, the proof appears to go through OK but Lean is reporting this error:

src/test.lean:15:0: error: application type mismatch
  List.cons (Fin.add 1 (U4_MAX + 0))
argument has type
  Fin 16
but function has type
  Nat → List Nat → List Nat

I figured out two solutions. Firstly, we can manually unfold U4_MAX (as illustrated by the comment); or, we can annotate U4_MAX with @[simp]. But, I don't understand why I need to do this? I might understand better if U4_MAX was a def ... ?

[Kyle Miller]

I'm not seeing an error locally. Which version of Lean are you using? (#eval Lean.versionString)

[David Pearce]

Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release

[Kyle Miller]

I'm using 4.8.0-rc1

[Kyle Miller]

By the way, here's a way to handle the positivity condition:

abbrev UInt4 := Fin 16
abbrev U4_MAX : UInt4 := {val:=15, isLt:=(by simp_arith)}

@[simp]
def sum (items : List (Fin (n + 1))) : Fin (n + 1) :=
  items.foldl (init := 0) (· + ·)

example : sum (1::2::[]) = (3 : UInt4)  :=
by
  simp_arith

example : sum (1::U4_MAX::[]) = 0  :=
by
  simp_arith

[David Pearce]

Hmmm... well I can try upgrading I suppose

[Kyle Miller]

(Also, I used a fold, but that's not necessary. The main thing is that (0 : Fin (n + 1)) works without needing to pass a proof.)

[David Pearce]

Ah, I see ... yeah neat Fin (n + 1).

[Kyle Miller]

A risk with Fin (n + 1) is that if you're dealing with complicated expressions (you're not here to be clear -- the 16 in Fin 16 is very simple) then unifying against n + 1 can trigger a potentially expensive calculation. It's perfectly fine for fixed-width numeric types like this.

[David Pearce]

Well, my real code is working against UInt256 ... how does that stack up ?

[Kyle Miller]

(You might also like to know that set_option pp.numericTypes true shows all the types of all the numeric literals. Just mentioning it in case it's eventually useful.)

[Kyle Miller]

That's mod 2 ^ 256? Should be fine.

[David Pearce]

Yes, U256_MAX is defined as:

abbrev U256_MAX : UInt256 := {val:=(2^256) - 1, isLt:=(by simp_arith)}

[David Pearce]

The set_option doesn't seem to make heaps of difference in VS Code (though some)

[David Pearce]

Ah, I see in the error messages though it makes a difference

[Kyle Miller]

It affects the Infoview too

[Kyle Miller]

Regarding your first error, I would guess that adding some type ascriptions somewhere, like

example(p:16>0) : sum (1::U4_MAX::[]) p = (0 : UInt4)  := ...

would make a difference, if you don't want to upgrade.

[David Pearce]

Hmmm, no still fails:

example(p:16>0) : sum (1::U4_MAX::[]) p = (0 : UInt4)  :=
by
  --unfold U4_MAX
  simp_arith

[Kyle Miller]

I'm wondering if you happen to have anything else in context? If you copy your mwe into a fresh file, do you still see the error? (I'm wondering in particular if there's another sum that's conflicting with yours somehow...)

[David Pearce]

I can try that now

[David Pearce]

Hmmm, I don't think that's it. Moving into a different workspace which is essentially empty, and same thing. I'm running lean directly against the test.lean file. Also, moving out of any existing lean workspace ... same thing.

[Kyle Miller]

Last guess, maybe sum ((1 : UInt4)::U4_MAX::[]) p = (0 : UInt4)?

[Kyle Miller]

Oh, sorry, I didn't understand what sort of error you were reporting. You're saying that simp_arith itself isn't reporting the error, right? Is the error on example?

[David Pearce]

Oh, so wierd. Just pushing through the change to use Fin (n+1). Here's it working nicely:

bbrev UInt4 := Fin 16
abbrev U4_MAX : UInt4 := {val:=15, isLt:=(by simp_arith)}

@[simp]
def sum(items: List (Fin (n+1))): Fin (n+1) :=
  match items with
  | h::t => h + (sum t)
  | [] => {val:=0, isLt:=(by simp_arith)}

example : sum (1::2::[]) = (3:UInt4)  :=
by
  simp_arith

example : sum (1::U4_MAX::[]) = 0  :=
by
  simp_arith

Its strange though as don't need a type for 0 but do need one now for 3 in the first example!!

[David Pearce]

sum ((1 : UInt4)::U4_MAX::[]) p = (0 : UInt4)

I tried a bunch of this stuff. I understand its having problem inferring the correct type.

[Kyle Miller]

Is the error on example?

If this is the case, that means there was an error inside of simp_arith itself. There have been some bug fixes there since 4.7.0

[David Pearce]

Yes, the error was underlying example.

[David Pearce]

Almost like an internal error

[Kyle Miller]

Yes, definitely an internal error. It's saying that the proof generated by simp_arith was type incorrect.

[David Pearce]

Right, ok. I didn't understand fully what it was complaining about :joy:

[David Pearce]

Thanks

[Kyle Miller]

Error messages are still being improved! Don't be shy bringing up any that don't make sense.