Working with a decidable predicate on only some values

Stream: new members

[Kevin Cheung]

In the following example, Decidable has only been defined for foo k wherek = 0 and k = 1. Since bar is a list consisting of only 0 and 1, I wonder if there is a way to filter bar using foo. What I currently have is not accepted by Lean. Any help greatly appreciated.

def foo (k : Nat) : Prop := k = 0

instance foo0 : Decidable (foo 0) := isTrue rfl
instance foo1 : Decidable (foo 1) := isFalse (by simp [foo])

def bar := [0, 0, 1, 0, 0]

#check bar.filter foo
/- Type mismatch
  foo
has type
  Nat -> Prop : Type
but is expected to have type
  Nat -> Bool : Type
  -/

example : foo 0 := by decide -- This works.
example : ¬foo 1 := by decide -- This works.
example : ¬foo 2 := by simp [foo] -- This works.
example : ¬foo 2 := by decide -- This of course does not work.

[Yakov Pechersky]

Nothing knows that bar is made up of only 0 and 1 when you do the filter. You need to help out the system to show that foo is decidable when restricted to bar. And that is the additional instance below. The equation compiler is smart enough to recognize that only 0 and 1 are in bar.

Consider this instead

def foo (k : Nat) : Prop := k = 0

instance foo0 : Decidable (foo 0) := isTrue rfl
instance foo1 : Decidable (foo 1) := isFalse (by simp [foo])

def bar := [0, 0, 1, 0, 0]

instance : DecidablePred  (fun (x : {x // x ∈ bar}) ↦ foo x)
| ⟨0, _⟩ => inferInstance
| ⟨1, _⟩ => inferInstance

#check bar.attach.filter (fun x ↦ (foo (x : {x // x ∈ bar})))

[Kevin Cheung]

Thank you!