Merge condense lists into lists of ranges

Stream: new members

[Iocta]

Why does by decide fail here?

import Mathlib

open List

set_option diagnostics true


structure Range where
  first : Int
  last : Int
deriving Repr



def mergeListsOfDisjointRanges (xs ys : List Range) : List Range :=
  match xs, ys with
  | [], ys => ys
  | xs, [] => xs
  | (x'::xs'), (y'::ys') =>
    let lastx := xs'.getLastD x'
    if lastx.last + 1 = y'.first
    then xs.dropLast ++ [⟨lastx.first, y'.last⟩] ++ ys'
    else xs ++ ys


def XS : List Int := [1, 2, 3, 4, 6, 8, 9, 10, 15]


def condense : List Int → List Range :=
  foldl mergeListsOfDisjointRanges [] ∘ map (fun x => [Range.mk x x])

example : condense XS = [⟨1,4⟩, ⟨6,6⟩, ⟨8,10⟩, ⟨15,15⟩] := by decide


/-

failed to synthesize
  Decidable
    (condense XS =
      [{ first := 1, last := 4 }, { first := 6, last := 6 }, { first := 8, last := 10 }, { first := 15, last := 15 }]) -/

[Edward van de Meent]

you likely need DecidableEq Range

[Edward van de Meent]

yup, playground confirms

[Edward van de Meent]

a simple deriving DecidableEq fixes it

[Edward van de Meent]

(to be more verbose about how i got there: lean complains it doesn't know Decidable (condense XS = bla), where condense XS has type List Range. Deciding if two lists are equal is done elementwise, so you (likely) need DecidableEq Range. there is "likely" because deciding equality can happen in other ways)