Zulip Chat Archive

Stream: new members

Topic: And versus currying

Brandon Brown (May 21 2021 at 02:32):

Let's say I want to state the theorem that the ≤ relation on nats is transitive, I can do it in two ways, one using and and the other with currying. I believe they are equivalent. It looks like mathlib uses currying; why should I prefer one approach over the other?

trans1 :  x y z, x  y  y  z  x  z
trans2 :  x y z, x  y  y  z  x  z

Andrew Ashworth (May 21 2021 at 02:47):

implication is more fundamental, and is a inductive type

Andrew Ashworth (May 21 2021 at 02:47):

one is simpler than the other

Andrew Ashworth (May 21 2021 at 02:49):

suppose you want to apply the hypothesis x <= y to trans2 - it's impossible without some busywork constructing an and structure

Brandon Brown (May 21 2021 at 02:51):

ok thanks!

Kevin Buzzard (May 21 2021 at 06:05):

They're logically equivalent but they're not definitionally equivalent and, as Andrew says, the version with the implications is more primitive and hence easier to use. The version with all the arrows looks weird to a mathematician because we don't usually write stuff like that, but if you put stuff before the colon then it looks totally normal: trans1 (x y z : A) (hxy : x <= y) (hyz : y <= z) : x <= z

Last updated: Dec 20 2023 at 11:08 UTC