greek letter tactic

Stream: general

[Patrick Massot]

Is there a tactic doing only that greek letter which transforms (λ a, f a) x to f x?

[Andrew Ashworth]

I think dsimp with one of its special options does it, but I don't remember exactly what it is

[Kenny Lau]

that's eta reduction

[Kenny Lau]

no

[Andrew Ashworth]

beta

[Kenny Lau]

that's delta reduction

[Kenny Lau]

oh

[Kenny Lau]

beta it is then

[Patrick Massot]

I say alpha!

[Kenny Lau]

no, that's also eta reduction

[Patrick Massot]

We need printable DTT cheat sheets

[Kenny Lau]

it's not even DTT

[Kenny Lau]

-- (λ (a : X), f a) x = f x
example : (λ a, f a) x = f x :=
by dsimp { eta := false, beta := false }

-- (λ (a : X), f a) x = f x
example : (λ a, f a) x = f x :=
by dsimp { eta := true, beta := false }

-- f x = f x
example : (λ a, f a) x = f x :=
by dsimp { eta := false, beta := true }

[Kenny Lau]

why isn't it eta?

[Kenny Lau]

@Andrew Ashworth

[Andrew Ashworth]

i don't know how dsimp does it, but I remember it as eta is the sorta useless thing that turns lam x, f x --> f, while beta is (lam x, f x) y --> f y

[Andrew Ashworth]

basically eta only cleans up useless lambdas

[Reid Barton]

An amazing feature I only discovered recently: set_option pp.beta true will hide those useless (λ a, f a) x in displayed types

[Chris Hughes]

The slightly annoying thing about that is sometimes it won't rewrite because it's not reduced, and you get frustrated trying to work out why.

[Kevin Buzzard]

You need to set pp.beta true in rw as well :-)