Zulip Chat Archive

Stream: general

Topic: greek letter tactic


Patrick Massot (May 28 2018 at 11:38):

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

Andrew Ashworth (May 28 2018 at 11:42):

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

Kenny Lau (May 28 2018 at 11:42):

that's eta reduction

Kenny Lau (May 28 2018 at 11:42):

no

Andrew Ashworth (May 28 2018 at 11:42):

beta

Kenny Lau (May 28 2018 at 11:42):

that's delta reduction

Kenny Lau (May 28 2018 at 11:42):

oh

Kenny Lau (May 28 2018 at 11:43):

beta it is then

Patrick Massot (May 28 2018 at 11:43):

I say alpha!

Kenny Lau (May 28 2018 at 11:43):

no, that's also eta reduction

Patrick Massot (May 28 2018 at 11:43):

We need printable DTT cheat sheets

Kenny Lau (May 28 2018 at 11:43):

it's not even DTT

Kenny Lau (May 28 2018 at 11:50):

-- (λ (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 (May 28 2018 at 11:50):

why isn't it eta?

Kenny Lau (May 28 2018 at 11:50):

@Andrew Ashworth

Andrew Ashworth (May 28 2018 at 11:57):

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 (May 28 2018 at 11:58):

basically eta only cleans up useless lambdas

Reid Barton (May 28 2018 at 17:09):

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 (May 28 2018 at 17:25):

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 (May 28 2018 at 21:45):

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


Last updated: Dec 20 2023 at 11:08 UTC