## Stream: new members

### Topic: definition unpacking

#### Alistair Tucker (Feb 18 2020 at 18:37):

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 (Feb 18 2020 at 18:38):

Hi! I was wondering why is the second decidable_pred necessary

#### Kevin Buzzard (Feb 18 2020 at 18:39):

because if is syntax sugar for ite and

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


#### Kevin Buzzard (Feb 18 2020 at 18:39):

Is this what you meant?

#### Alistair Tucker (Feb 18 2020 at 18:40):

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 (Feb 18 2020 at 18:40):

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 (Feb 18 2020 at 18:40):

I see. Can I make it do that?

#### Kevin Buzzard (Feb 18 2020 at 18:40):

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 (Feb 18 2020 at 18:41):

Thanks! I'll try that

#### Kevin Buzzard (Feb 18 2020 at 18:41):

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

#### Kevin Buzzard (Feb 18 2020 at 18:44):

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 (Feb 18 2020 at 18:45):

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 (Feb 19 2020 at 18:18):

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).

Last updated: May 14 2021 at 07:19 UTC