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: Dec 20 2023 at 11:08 UTC