linarith failure

Stream: general

[Patrick Massot]

@Rob Lewis Is the following expected?

example {K d : ℝ} (h : 0 ≤ K) (h' : 0 ≤ d) : 0 ≤ 2*K*d :=
begin
  -- linarith,  fails :-(    :-(    :-(
  suffices : 0*0*0 ≤ 2*K*d, by simpa using this,
  apply mul_le_mul ; try { linarith },
  apply mul_le_mul ; linarith ,
end

[Kenny Lau]

mul_le_mul isn't linear is it

[Patrick Massot]

I thought lin in linarith stands for "life is nice"

[Rob Lewis]

I think the try {linarith} line should be able to kill all the subgoals. It should recognize 0*0 as 0. Not sure what's failing, I'll take a look at it when I have time.

[Rob Lewis]

try {simp; linarith} works for now.

[Rob Lewis]

And it certainly shouldn't work without you applying the first mul_le_mul, as Kenny points out that isn't a linear goal.

[Rob Lewis]

Or, rather, apply mul_le_mul; simp; linarith in the second line finishes the proof.

[Patrick Massot]

Thanks. I still wish we have better tools for such things, but linarith already goes a long way

[Patrick Massot]

My Lean day has been all about wishing computation were easy in Lean. I got upset and forced my way through the computation. It reminds me of my old chain rule days

[Patrick Massot]

The result is at: https://gist.github.com/PatrickMassot/82c69e2d4c30d0b7121f9fd46b5deed1 I'd be interested in a golfed version, if someone wants to practice computing in Lean. The main definition is:

open set
variables {α : Type*} {β : Type*} [metric_space α] [metric_space β]

def lipschitz_on_with (s : set α) (K : ℝ) (f : α → β) :=
0 ≤ K ∧ ∀x y ∈ s, dist (f x) (f y) ≤ K * dist x y

example (K : ℝ) (f : α → β) : lipschitz_with K f ↔ lipschitz_on_with univ K f :=
⟨λ ⟨hK, h⟩, ⟨hK, λ x y _ _, h x y⟩, λ ⟨hK, h⟩, ⟨hK, λ x y, h x y (mem_univ x) (mem_univ y)⟩⟩

and the goal is to prove that any map which is K-Lipschitz on a ball extends to a map which globally 2K-Lipschitz

variables {E : Type*} [normed_space ℝ E] {F : Type*} [normed_space ℝ F]
lemma lipschitz_extend_from_ball {a : E} {r : ℝ} {K : ℝ} {f : E → F} (h : lipschitz_on_with (closed_ball a r) K f) :
∃ g : E → F, (∀ x ∈ closed_ball a r, g x = f x) ∧ lipschitz_with (2*K) g

The motivation was a nice proof of the inverse function theorem. But much of the niceness of this proof relies on the fact that proving the above lemma is trivial. With a 200 lines long proof the lemma, the inverse function theorem proof looks less nice.

[Rob Lewis]

The 0*0 bug was easy, it's fixed now.

[Rob Lewis]

Although, now that I look at your original problem again, I think this would have worked even without the fix.

example {K d : ℚ} (h : 0 ≤ K) (h' : 0 ≤ d) : 0 ≤ 2*K*d :=
begin
  suffices : 0*0 ≤ 2*K*d, by simpa using this,
  apply mul_le_mul; linarith
end