Zulip Chat Archive

Stream: new members

Topic: definition unpacking


view this post on Zulip 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

view this post on Zulip Alistair Tucker (Feb 18 2020 at 18:38):

Hi! I was wondering why is the second decidable_pred necessary

view this post on Zulip 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}, α → α → α

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:39):

Is this what you meant?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Alistair Tucker (Feb 18 2020 at 18:40):

I see. Can I make it do that?

view this post on Zulip 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

view this post on Zulip Alistair Tucker (Feb 18 2020 at 18:41):

Thanks! I'll try that

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:41):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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