Applying (λ x, x + b) and (+ b) give different expressions

Stream: general

[Eric Wieser]

I'm seeing some odd behavior where(λ x, x + b) and (+ b) have the same pretty-printed representation, yet behave differently under function application

variables {a b : ℕ} {s : set ℕ}

-- same
#check (λ _x, _x + b) -- λ (_x : ℕ), _x + b : ℕ → ℕ
#check (+ b)          -- λ (_x : ℕ), _x + b : ℕ → ℕ

-- different?
#check (λ x, x + b) a -- (λ (x : ℕ), x + b) a : ℕ
#check ((+ b) : _) a  -- (λ (x : ℕ), x + b) a : ℕ
#check (+ b) a        -- a + b : ℕ

What's going on here?

[Bhavik Mehta]

Aren't these definitionally the same thing?

[Eric Rodriguez]

i was gonna say it was just b-red, but pp.beta causes even more confusion:

set_option pp.beta true

-- different?
#check (λ x, x + b) a -- a + b : ℕ
#check ((+ b) : _) a  -- (λ (_x : ℕ), _x + b) a : ℕ
#check (+ b) a        -- a + b : ℕ

[Eric Wieser]

Yes, they're all defeq, but I need syntactic equality to make the elaborator behave

[Mario Carneiro]

Don't use set_option pp.beta true, it performs beta reduction in the pretty printer which makes it hard to tell what term you are actually looking at

[Mario Carneiro]

I would guess that this is parser magic, it sees that you have applied a function slice operator to some arguments and pre-composes it

[Eric Rodriguez]

Mario Carneiro said:

Don't use set_option pp.beta true, it performs beta reduction in the pretty printer which makes it hard to tell what term you are actually looking at

why is β-red in the pretty printer bad? I've got a lot of λs flying about so they make my proofs a lot easier

[Mario Carneiro]

because they aren't making your proofs easier, they are making your proofs look easier

[Mario Carneiro]

it doesn't do anything at all to the state

[Mario Carneiro]

if you want to do beta reduction use dsimp only

[Mario Carneiro]

if you want to pretend beta reduction doesn't exist then use pp.beta

[Mario Carneiro]

but then you will get weird errors when on identical (looking!) states rw will work in one case and fail in the other

[Eric Rodriguez]

wow, surprised that hasn't bit me yet. turned it off; thanks!