help with proof for decreasing_by in natToBytes

Stream: Program verification

[David Stainton 🦡]

Hi. Two questions:

1. is there a better way to convert a Nat to ByteArray? I don't care about endianness.
2. how can i write a proof for the following code where i put the sorry?

def natToBytesAux (n : Nat) (acc : List UInt8) : List UInt8 :=
  if n == 0 then acc else natToBytesAux (n / 256) (UInt8.ofNat (n % 256) :: acc)
decreasing_by sorry

def natToBytes (n : Nat) : ByteArray :=
  List.toByteArray (natToBytesAux n [])

[Shreyas Srinivas]

def natToBytesAux (n : Nat) (acc : List UInt8) : List UInt8 :=
  if n == 0 then acc else natToBytesAux (n / 256) (UInt8.ofNat (n % 256) :: acc)
termination_by n
decreasing_by
  simp_wf
  simp_all
  omega

def natToBytes (n : Nat) : ByteArray :=
  List.toByteArray (natToBytesAux n [])

[François G. Dorais]

Just change n == 0 to n = 0.

[David Stainton 🦡]

yes both of those work. thanks

[François G. Dorais]

You may also consider pushing directly onto the byte array instead of constructing an intermediate list.

[François G. Dorais]

PS: The most efficient way to do this would use the Lean innards (aka implementation details) and use memcpy... but you can't prove anything about that.

[David Stainton 🦡]

yeah, makes sense. i'm definitely interested in proving things but i have zero experience with proofs... so i've been focusing more on just learning functional programming in Lean. I've found that it's rather fun to try to translate Haskell into Lean.