tutorial problem 0011

Stream: general

[Miles]

In the Lean Tutorial (https://github.com/leanprover-community/tutorials) problem #0011, I was unable to prove that (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b without using the transitive property of ≤. Am I missing something?

If there isn't another way that I simply failed to see, then in my opinion, the user should either be explicitly given the transitive property as something to apply or be told that it is valid to chain expressions together with ≤ as in

calc expr1 ≤ expr2 : proof12
... ≤ expr3 : proof23

to get a final inequality expr1 ≤ expr3. Does anyone have thoughts?

[Mario Carneiro]

I don't think it says anywhere that you shouldn't use transitivity

[Miles]

Yes, but for newcomers I think it would be helpful to say explicitly that calc ... can be used in that way (thus far it had only been used for a equality or single inequality. Just a suggestion

[Huỳnh Trần Khanh]

AFAICT it is already stated in the docs of calc mode https://leanprover-community.github.io/extras/calc.html

[Miles]

Ah, thank you, that's good to know. I had not read that far into the docs before starting the tutorial.

[Patrick Massot]

@Miles , I'd like to understand what you understood here. Chain equalities and inequalities is the only purpose of calc. What did you think calc was doing? I'm asking because I'll resume teaching using this material in two weeks.

[Miles]

For context, I was coming to this tutorial from the natural number game, where it seems nothing could be taken for granted. I had proved that a ≤ a + b (and ha tells us that 0 ≤ a), but I did not believe that we had proven transitivity of ≤. Transitivity of equality is essentially given to us by the rw tactic, so chain equality of calc (which was explicitly demonstrated in file 01, line 97) seems like just a simplification of multiple uses of rw. Since we hadn't proven or been told anywhere that ≤ is transitive, I didn't think that was a fact we could assume that calc would do. It would have helped me to be told explicitly in the comments that calc can have more than one ≤ in its chain and remain valid (i.e. that ≤ is transitive). I hope that helps clarify my thinking. I'm happy to share more if it doesn't. Thanks