Zulip Chat Archive

Stream: new members

Topic: order of arguments

Daan van Gent (Nov 05 2022 at 15:49):

Why is the order of arguments in

theorem sup_le_sup_left (h₁ : a  b) (c) : c  a  c  b

hypothesis h first and element c second, while

lemma inf_le_inf_right (a : α) {b c : α} (h : b  c) : b  a  c  a

is the other way around?

Eric Wieser (Nov 05 2022 at 15:54):

To me those both look backwards!

Eric Wieser (Nov 05 2022 at 15:58):

docs#sup_le_sup_right and docs#inf_le_inf_left both look right to me, in contrast

Daan van Gent (Nov 05 2022 at 16:02):

I see no difference between those and mine. Both don't agree on the order of element vs hypothesis, or is there some logic I am missing?

Andrew Yang (Nov 05 2022 at 16:46):

The order of the hypothesis should match the order of appearances in the statement.

Daan van Gent (Nov 05 2022 at 17:01):

What does that mean? The hypothesis h₁ : a ≤ b appears nowhere in the statement c ⊔ a ≤ c ⊔ b

Eric Wieser (Nov 05 2022 at 17:08):

It's more of a heuristic than an algorithm. c ⊔ a ≤ c ⊔ b is natural to think of as a ≤ b with c on the left, so in the arguments c is on the left of the a ≤ b argument.

Daan van Gent (Nov 05 2022 at 17:54):

I see, thanks! That's not something I would have guessed. I expected something like data to take precedence over propositions.

Yaël Dillies (Nov 05 2022 at 18:40):

Actually you should expect the other way because proof arguments are (usually) not inferrable from the rewrite, while data arguments are.

Last updated: Dec 20 2023 at 11:08 UTC