Why does Lean allow invalid UInt8 literals? - Stack Overflow

admin管理员组

文章数量:1122832

def x := (0xFFFF : UInt8)

That compiles with no errors, which I find surprising given Lean's focus on proving correctness. Is there a good reason for this or is it simply an oversight? Also what does it do at runtime?

Bonus question: is there a more elegant way to write a UInt8 literal? E.g. in Rust you can do 0xFFu8.

def x := (0xFFFF : UInt8)

That compiles with no errors, which I find surprising given Lean's focus on proving correctness. Is there a good reason for this or is it simply an oversight? Also what does it do at runtime?

Bonus question: is there a more elegant way to write a UInt8 literal? E.g. in Rust you can do 0xFFu8.

• lean

Share Improve this question Follow asked yesterday TimmmmTimmmm 96.3k7979 gold badges401401 silver badges569569 bronze badges 2

• You can also do def x : Fin 3 := 37 (and then example : x = 1 := rfl). It's not an oversight, and there is a reason (it saves you from having to supply the proof; it just wraps mod n, the idea is that it makes the code easier to write for the user). Whether you think it's a good reason is another matter (I also feel that this is a very dubious design decision). – Kevin Buzzard Commented yesterday
• "given Lean's focus on proving correctness" - Not sure where this impression came from. I'd say the opposite: Lean seems to cut corners as match as possible. Wraparound for u8 overflow yet underflow like 2 - 3 gets clamped at 0 for no reason. But these are minor issues, things like implicit currying that may break all your code if you accidentally miss an argument are the evilest imaginable. – user7860670 Commented yesterday

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 1

As mentioned in the comment, allowing this is not inconsistent with "focusing on proving correctness"; for bounded integers, numeric literals which exceed the bounds of the type are just defined to wrap around, so you can do #eval (0xFFFF : UInt8) and will find that this evaluates to 255.

The reasons for this behavior are mainly due to the way numeric literals are implemented in Lean 4. This works using a typeclass called OfNat: when Lean encounters a numeric literal n with expected type α, it will attempt to synthesize an instance of OfNat α n. So to get the desired behavior of rejecting literals which are out of bounds, you would need to somehow give an instance of OfNat α n only if n is small enough. This is not something that Lean's typeclass system supports in a straightforward way, so usually instances of OfNat are defined for all n and just implement some kind of wrapping behavior.

However, it is in fact possible to get the desired behavior using a somewhat obscure trick as demonstrated by the following code:

class When (p : Prop) [Decidable p] : Prop where
  isTrue : p

instance : @When p (.isTrue h) := @When.mk p (_) h

-- Just a wrapper around `UInt8` to avoid clashing with the existing `OfNat` instance.
inductive MyUInt8 : Type where
  | mk : UInt8 -> MyUInt8

instance [When (n < 256)] : OfNat MyUInt8 n where
  ofNat := ⟨n.toUInt8⟩

#check (0xFF : MyUInt8) -- works
#check (0xFFFF : MyUInt8) -- failed to synthesize `OfNat MyUInt8 65535`

As discussed in the thread linked above, this approach has some limitations and therefore should not be considered a good solution to the problem, which is presumably why the Lean core developers do not use it in the OfNat instaces defined in Lean core.

It is possible that the Lean developers will rework numeric literals in the future and introduce a less hacky and more general solution than the When hack described above. Getting this right will be tricky, as it is a potentially very disruptive change, so I wouldn't expect to see any movement on this front soon.

Regarding your bonus question: if the expected type is known, you do not need to annotate the type for the numeric literal. So for example you could write

def x : UInt8 := 0xFF

本文标签： Why does Lean allow invalid UInt8 literalsStack Overflow