Zulip Chat Archive

Stream: general

Topic: linarith failure


view this post on Zulip Patrick Massot (Mar 05 2019 at 19:48):

@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

view this post on Zulip Kenny Lau (Mar 05 2019 at 19:48):

mul_le_mul isn't linear is it

view this post on Zulip Patrick Massot (Mar 05 2019 at 19:51):

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

view this post on Zulip Rob Lewis (Mar 05 2019 at 19:53):

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.

view this post on Zulip Rob Lewis (Mar 05 2019 at 19:53):

try {simp; linarith} works for now.

view this post on Zulip Rob Lewis (Mar 05 2019 at 19:54):

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

view this post on Zulip Rob Lewis (Mar 05 2019 at 19:55):

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

view this post on Zulip Patrick Massot (Mar 05 2019 at 19:58):

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

view this post on Zulip Patrick Massot (Mar 05 2019 at 20:07):

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

view this post on Zulip Patrick Massot (Mar 05 2019 at 20:23):

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.

view this post on Zulip Rob Lewis (Mar 05 2019 at 21:49):

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

view this post on Zulip Rob Lewis (Mar 05 2019 at 21:53):

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

Last updated: May 13 2021 at 18:26 UTC