# Zulip Chat Archive

## 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