How to create instance of Decidable?

Stream: new members

[MrQubo]

I cannot grasp how to create instances of Decidable. Can someone help me for example write this instance?

import Mathlib

variable {α : Type}

def funPos (f : α → Nat) : Prop := ∀ a : α, f a > 0

instance instDecidable_funPos [FinEnum α] : DecidablePred (@funPos α)
  := λ f ↦
  let b := (FinEnum.toList α).all (λ a ↦ f a > 0)
  _

I know how to compute the result as Bool. But how to make instance of Decidable from this?

[Matthew Jasper]

instance instDecidable_funPos [FinEnum α] : DecidablePred (@funPos α)
  := λ f ↦
  if h : (FinEnum.toList α).all (λ a ↦ f a > 0) then
    .isTrue (by simpa [funPos] using h)
  else
    .isFalse (by simpa [funPos] using h)

[Johannes Tantow]

import Mathlib

variable {α : Type}

def funPos (f : α → Nat) : Prop := ∀ a : α, f a > 0

instance instDecidable_funPos [FinEnum α] : DecidablePred (@funPos α)
  := fun f =>
    decidable_of_bool
    ((FinEnum.toList α).all (λ a ↦ f a > 0)) (by simp [funPos])

[Eric Wieser]

If you replace def with abbrev then optimistically you can use inferInstance as the whole proof

[MrQubo]

Eric Wieser said:

If you replace def with abbrev then optimistically you can use inferInstance as the whole proof

You're right, this works:

import Mathlib

variable {α : Type}

abbrev funPos (f : α → Nat) : Prop := ∀ a : α, f a > 0

instance instDecidable_funPos [FinEnum α] : DecidablePred (@funPos α) := inferInstance

But what is abbrev?

[Kevin Buzzard]

a def which Lean (and specifically here, the typeclass system) sees through easily (a reducible inline def)

[MrQubo]

So, in this case, typeclass system can replace funPos with it's definition?

Hm, so it seems like, there is somewhere Decidable instance for \forall?

[Kevin Buzzard]

You can use #synth to see which instance it's finding.

[MrQubo]

Kevin Buzzard said:

You can use #synth to see which instance it's finding.

Thanks! It's λ _ ↦ Fintype.decidableForallFintype.