Proving decidable_pred

Stream: general

[Joshua E Cook]

In the code below, why does part1 typecheck but part1' give an error that I must prove decidable_pred increasing? How do I approach proving decidable_pred increasing?

def infixes (n : ℕ) : list ℕ → list (vector ℕ n)
  | (hd :: tl) :=
    let sub := list.take n (hd :: tl) in
    if h : sub.length = n then
      ⟨ sub, h ⟩ :: (infixes tl)
    else []
  | [] := []

def part1 (x: list ℕ) : ℕ :=
  let f := λ x : vector ℕ 2, list.pairwise (<) x.val in
  list.length (list.filter f (infixes 2 x))

def increasing : vector ℕ 2 → Prop
  | ⟨ items, _ ⟩ := list.pairwise (<) items

def part1' (x: list ℕ) : ℕ :=
  list.length (list.filter increasing (infixes 2 x))

[Yakov Pechersky]

Will you actually be executing these functions or do you want to just conceptually prove things about them?

[Joshua E Cook]

I'm executing them. (This is my attempt at better learning Lean by solving Advent of Code problems.)

[Yakov Pechersky]

list.filter works by evaluating the function that you give it as a predicate to branch on. You have to provide an instance proving that for any vector nat 2, increasing can be computed into a tt or ff value. In this particular case, it'll probably be just relying on existing instance that days that list.pairwise is decidable if the underlying relation is decidable. I'm sure that's somewhere in mathlib

[Eric Wieser]

I'd recommend not defining increasing with a pattern match like that

[Eric Wieser]

Those pattern matches get in the way of lots of automation

[Eric Wieser]

This works fine:

def increasing (items : vector ℕ 2) : Prop := list.pairwise (<) items.val
instance : decidable_pred increasing := λ l, list.decidable_pairwise l.val

def part1' (x: list ℕ) : ℕ :=
  list.length (list.filter increasing (infixes 2 x))