triangle inequality

Stream: new members

[Olu Olorode]

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]

split_ifs is great for this

[Mario Carneiro]

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]

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]

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]

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]

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

[Scott Morrison]

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

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

[Dan Stanescu]

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]

It comes much earlier in the story

[Patrick Massot]

So you already have it in data.real.basic

[Patrick Massot]

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

[Patrick Massot]

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

[Dan Stanescu]

Patrick Massot said:

It comes much earlier in the story

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