Signed integers

Stream: mathlib4

[Chris B]

Is there a plan for the implementation of signed integers? Is it appropriate to make an analog for Fin n along these lines?

structure Zfin (n : Nat) where
  val : Int
  isLt : val.natAbs < n

[Sebastian Ullrich]

Do you mean bounded/unboxed integers? I think it's clear we will eventually need Int8 etc., though isLt will have to take the asymmetry of the negative and positive range into consideration.

[Sebastian Ullrich]

Oops, I thought this was #lean4... but maybe it's still relevant

[Chris B]

Sebastian Ullrich said:

though isLt will have to take the asymmetry of the negative and positive range into consideration.

Lol that's so stupid. I was referencing a thing about C data types, and apparently there was a version of the C99 standard that had symmetrical signed integers (-127 ~ 127).

Do you have an implementation in mind? I'm working on something that needs a bounded Z, I'm interested in whether there are arguments for one implementation or another.

[Sebastian Ullrich]

It's probably silly for formalization purposes, but thinking about the compiler, the simplest solution would probably be to make Int8 a wrapper struct around UInt8.

[Chris B]

Ok, I'll try that out.

[Chris B]

@Sebastian Ullrich

I'm not sure whether this is compatible with the attribute/implementation magic that goes on in the prelude, but if this will save you some typing I can add some tests and PR this later: https://gist.github.com/ammkrn/79281ae3d3b301c99a84821c18dcb5f1

[Chris B]

Also what is it about the bitwise and/or stuff and USize operations that doesn't play well withrfl?

[Henrik Böving]

rfl solves goals by definitional equality, it's rather sensitive to the input:

variable (x : Nat)

example : x + 1 = Nat.succ x := by rfl -- works
example : 1 + x = Nat.succ x := by rfl -- does not work

and I'd guess these small differences between "obviously equal" and "definitionally equal" is what's happening with your bitwise operations

[Chris B]

For USize I think it's something else. USize.add and UInt8.add are defined in the same way, using addition for Fin, but they produce different behaviors:

/- OK -/
example : (1 : UInt8) + (0 : UInt8) = (1 : UInt8) := by rfl
/- type mismatch
  rfl
has type
  1 + 0 = 1 + 0 : Prop
but is expected to have type
  1 + 0 = 1 : Prop -/
example : (1 : USize) + (0 : USize) = (1 : USize) := by rfl

[Chris B]

For the bitwise stuff I guess it's because bitwise is partial while shiftLeft and shiftRight are not. I'm still not used to that.

[Gabriel Ebner]

That's because USize.size does not reduce in the kernel. And 1 + 0 = (1 + 0) % USize.size here.

[Chris B]

Interesting, thanks.