And versus currying

Stream: new members

[Brandon Brown]

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]

implication is more fundamental, and is a inductive type

[Andrew Ashworth]

one is simpler than the other

[Andrew Ashworth]

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

[Brandon Brown]

ok thanks!

[Kevin Buzzard]

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