## Stream: new members

### Topic: triangle inequality

#### 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.

#### Mario Carneiro (Apr 08 2020 at 10:44):

split_ifs is great for this

#### 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

#### 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

#### 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

#### 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


#### Kevin Buzzard (Apr 08 2020 at 10:52):

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

#### 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.

#### Olu Olorode (Apr 08 2020 at 10:55):

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

#### 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?

#### Patrick Massot (Apr 19 2020 at 16:19):

It comes much earlier in the story

#### Patrick Massot (Apr 19 2020 at 16:19):

So you already have it in data.real.basic

#### 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

#### 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)

#### 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