Zulip Chat Archive

Stream: new members

Topic: triangle inequality


view this post on Zulip Olu Olorode (Apr 08 2020 at 10:42):

Hello all,

I am trying to prove a version of the triangle inequality for the integers (For a,b integers |a -b| < = |a| + |b|). However, I have run into some trouble. My plan was to define my own version of absolute value for the integers, then carry out a proof by cases where Lean would evaluate the value of the expressions |a - b|, |a|, and |b| to determine the validity of the proof. For example, in the case that (a - b) > 0, a>0, and b>0, then |a - b| = a - b, |a| = a, and |b| = b, so we can conclude that the inequality holds and so on. However, the most natural way to define absolute value that I have found, say def absVal (a : Z) : Z := if a < 0 then -a else a. Yet, I have no idea to just extract the value of an expression from this definition in the proof rather than getting ite. This is a multipart question.

What cases tactic is the best to use in this case and if you do not mind can you give me a short example of its use?

Is there a better way to define absolute value that does not use ite?

Is there a known statement of the triangle inequality for the real numbers in Lean? A quick google search seems to suggest no, but perhaps I was not looking in the right places.

If the answer to the above question is no, then how would one apply the triangle inequality in analysis proofs in Lean?

I would greatly appreciate your assistance.

view this post on Zulip Mario Carneiro (Apr 08 2020 at 10:44):

split_ifs is great for this

view this post on Zulip Mario Carneiro (Apr 08 2020 at 10:45):

if you have an if expression in the goal it does cases on the condition and rewrites the if away in each subgoal

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 10:50):

I think you have to use an ite for the norm but the split_ifs tactic just breaks you into a small number of cases immediately

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 10:51):

The triangle inequality for the reals will be in mathlib although it might be heavily disguised, eg there might be some proof that the reals are a seminormed topological semiring and then a proof that all such semirings satisfy the triangle inequality, or something like that

view this post on Zulip Shing Tak Lam (Apr 08 2020 at 10:51):

I think with the way the ints are defined as an inductive data type, you can define abs without ite by pattern matching?

def zabs :   
| (int.of_nat n) := n
| (int.neg_succ_of_nat n) := n + 1

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 10:52):

And then instead of the split_ifs tactic you have to use the cases tactic

view this post on Zulip Scott Morrison (Apr 08 2020 at 10:54):

.... but if you define your function by pattern matching, it's important that you subsequently provide an API for it, so that no one _has_ to prove things using cases.

view this post on Zulip Olu Olorode (Apr 08 2020 at 10:55):

Ok, this all seems very promising and answered my questions. Thanks alot!

view this post on Zulip Dan Stanescu (Apr 19 2020 at 16:01):

Kevin Buzzard said:

The triangle inequality for the reals will be in mathlib although it might be heavily disguised, eg there might be some proof that the reals are a seminormed topological semiring and then a proof that all such semirings satisfy the triangle inequality, or something like that

Would it be unreasonable, if somewhat redundant, to have the triangle inequality for the reals in a a conspicuous place like data.real.basic, given how ubiquitous it is?

view this post on Zulip Patrick Massot (Apr 19 2020 at 16:19):

It comes much earlier in the story

view this post on Zulip Patrick Massot (Apr 19 2020 at 16:19):

So you already have it in data.real.basic

view this post on Zulip Patrick Massot (Apr 19 2020 at 16:21):

FYI, here all the file that separate the proof of triangle inequality from data.real.basic: tmp.pdf

view this post on Zulip Patrick Massot (Apr 19 2020 at 16:22):

(generated by running leanproject import-graph --from algebra.order_functions --to data.real.basic tmp.pdf inside mathlib)

view this post on Zulip Dan Stanescu (Apr 19 2020 at 16:30):

Patrick Massot said:

It comes much earlier in the story

You're right,abs_add. I failed to check. Thanks Patrick!


Last updated: May 08 2021 at 19:11 UTC