Type equality up to beta-reduction

Stream: lean4

[Clément Blaudeau]

Hi! Sorry if it already answered somewhere. I have an error at typechecking, where Lean complains that some types foo and bar are not equal. Actually, they are up to beta-reduction. Consider this example:

example : Vector Bool 3 := Vector.replicate 3 true -- works fine
example : Vector Bool 3 := Vector.replicate (3: USize).toNat true -- fails

The latter fails with

type mismatch
  Vector.replicate (USize.toNat 3) true
has type
  Vector Bool (USize.toNat 3) : Type
but is expected to have type
  Vector Bool 3 : Type

Is there a way to have the typechecker "try a bit harder" to show type-equality, or give it a set of hints/tactics to use ? Or do I need to insert a coercion ?

[EDITED] added toNat

[Patrick Massot]

What makes you think USize and Nat are the same?

[Patrick Massot]

And which version of Lean are you using? The error message you quote is not what you get in the online playground.

[Patrick Massot]

By playground I mean following the link you see in the upper right corner of your code block, leading to https://live.lean-lang.org/#codez=KYDwhgtgDgNsAEAueA1YBjALgewE7wCFtsZ4BmJAXlQx1wDpdhYBLdMTBCzXAVwQC0A+AHc8AawDO8AGYsAdsABQoSLATI0WPIWKkKialrqNmMNhwQAKMsgCqAZRYAvYAEp4PfvCGywLGEklIA

[Patrick Massot]

which says:

Application type mismatch: The argument
  3
has type
  USize
but is expected to have type
  Nat
in the application
  Vector.replicate 3

[Patrick Massot]

which seems a very reasonable error message.

[Patrick Massot]

example : Vector Bool 3 := Vector.replicate ((3: USize).toNat) true also fails but indeed (3: USize).toNat doesn’t seem to be definitionally equal to 3 : Nat.

[Clément Blaudeau]

Yes indeed my minimized example was too minimized and missing a coercion from Usize to Nat.
The actual example is the one you've written:

example : Vector Bool 3 := Vector.replicate (3: USize).toNat true

How can I convince the typechecker that (3: Usize).toNat is 3 : Nat, at typechecking time ?

[Clément Blaudeau]

I've edited the first message to show the error I'm interested in

[Robin Arnez]

You'll need a cast:

example : Vector Bool 3 := (Vector.replicate (USize.toNat 3) true).cast (by simp)

The reason this doesn't work in the first place is because USize.toNat 3 is equivalent to 3 % 2 ^ System.Platform.numBits where System.Platform.numBits is an opaque system-dependent constant (i.e. they aren't definitionally equivalent and there's no way to force them to be). The solution here is to use a cast where you can use regular equality instead of definitional equality.

[Patrick Massot]

You can’t convince the type checking system that something is true by definition when it’s not.

[Niels Voss]

This seems to be a failure of canonicity (which states that every closed term of type Nat reduces to a normal form). Lean deliberately sacrifices canonicity for other properties deemed more important, so it should be expected that some things might fail, but I'm not sure why this particular example fails.

[Aaron Liu]

well you have opaque constants so

[Aaron Liu]

I certainly wouldn't want System.Platform.numBits to reduce to any numeral since it's system dependent

[Aaron Liu]

and USize wraps a BitVec System.Platform.numBits

[Aaron Liu]

Clément Blaudeau said:

How can I convince the typechecker that (3: Usize).toNat is 3 : Nat, at typechecking time ?

You add a docs#Vector.cast

[Niels Voss]

To be clear, I agree with Lean's decision to sacrifice canonicity