iteration, ranges, and Fin n

Stream: new members

[JJ]

i am attempting to iterate through and mutate a fixed-size array. i am encountering some issues, however. the following code fails to compile with failed to synthesize: Decidable (prev = pixel). i don't quite understand what this means, though. does anyone have any tips on what could be causing this?

import Batteries
open Batteries

abbrev UInt6 := BitVec 6
abbrev Byte := UInt8

structure Pixel where
  (r g b a : Byte)

def index? (seen : Vector Pixel 64) (pixel : Pixel) : Option UInt6 := do
  for i in [0:64] do
    -- failed to synthesize: Inhabited Pixel
    if seen[i]! = pixel then
      return i
  failure

also, the []! probably shouldn't be necessary, given that [0:64] is exclusive on the 64 and Vector has a fixed size 64. it appears to be though. what is the cause of this?

my guess would be that Range is not appropriately treating its elements as Fin n, but i am not quite sure. i have also tried to manually apply the Membership.mem.upper theorem, but it does not appear to prove what i was hoping it to. (i have yet to learn the theorem proving parts of lean, though.)

[Daniel Weber]

What is the definition of Pixel?

[JJ]

whoops, sorry, updated

[Alexander Hilbert]

There is a def finRange (n : ℕ) : List (Fin n) in Mathlib.Data.List.Range.
Maybe you can use that to get rid of []!.

[Daniel Weber]

You should derive BEq and DecidableEq for Pixel

[JJ]

thanks, that was it!

[JJ]

the []! thing still confuses me a bit. i did play around some, and found [] works fine for a Fin 64 (which makes sense). so, i guess lean's iterators on ranges are not treating their elements as being Fin n, despite them being evidently so?

[JJ]

re: derivations, i also had to derive Inhabited. that's a cool little tidbit for why it's needed on the documentation page. docs#Inhabited