definition unpacking

Stream: new members

[Alistair Tucker]

variable [decidable_pred (λ x : ℝ, 0 < x)]
def p (x : ℝ) : Prop := 0 < x
variable [decidable_pred (λ x : ℝ, p x)]
def H (x : ℝ) : int := if p x then 1 else 0

[Alistair Tucker]

Hi! I was wondering why is the second decidable_pred necessary

[Kevin Buzzard]

because if is syntax sugar for ite and

ite : Π (c : Prop) [h : decidable c] {α : Sort u_1}, α → α → α

[Kevin Buzzard]

Is this what you meant?

[Alistair Tucker]

Well I can see that I need to assert that it's decidable. But I thought I'd done that with the first variable decidable_pred

[Kevin Buzzard]

Oh, you mean how come Lean can't figure out that it's decidable from what you have? Because it doesn't try to unfold p.

[Alistair Tucker]

I see. Can I make it do that?

[Kevin Buzzard]

import data.real.basic

variable [decidable_pred (λ x : ℝ, 0 < x)]
def p (x : ℝ) : Prop := 0 < x
instance foo : decidable_pred (λ x : ℝ, p x) := by unfold p; apply_instance
def H (x : ℝ) : int := if p x then 1 else 0

[Alistair Tucker]

Thanks! I'll try that

[Kevin Buzzard]

There's an even slicker version using attributes which I can never remember.

[Kevin Buzzard]

If you're doing mathematics then you can just open_locale classical and everything will be decidable, just like it is in mathematics.

[Kevin Buzzard]

import data.real.basic

noncomputable theory

open_locale classical

def p (x : ℝ) : Prop := 0 < x
def H (x : ℝ) : int := if p x then 1 else 0

[Floris van Doorn]

Either of the following two will also work:

import data.real.basic

variable [decidable_pred (λ x : ℝ, 0 < x)]
@[derive decidable] def p (x : ℝ) : Prop := 0 < x
def H (x : ℝ) : int := if p x then 1 else 0

This first just syntax for Kevin's solution.

import data.real.basic

variable [decidable_pred (λ x : ℝ, 0 < x)]
@[reducible] def p (x : ℝ) : Prop := 0 < x
def H (x : ℝ) : int := if p x then 1 else 0

reducible means Lean will unfold p during type-class resolution (when checking that it is decidable).