Zulip Chat Archive

Stream: new members

Topic: linarith and let


view this post on Zulip Kyle Miller (Jun 05 2020 at 22:09):

This question is about verification of the behavior of linarith. Suppose h : ∀ (ε : ℝ), ε > 0 → ... (the rest does not matter) and we have a > b in the context. If you do

let ε := (a - b)/2,
specialize h ε (by linarith),

the linarith fails to prove ε > 0. However, if you do

set ε := (a - b)/2 with εeq,
specialize h ε (by linarith),

the linarith succeeds proving the same fact.

Having perused the code for the tactic, it seems it looks through the context only for propositions that are inequalities. Is there any reason it doesn't also consider definitions produced by let? (Another question: is there a tactic that converts definitions into equalities?)

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:22):

This doesn't answer your question, but I avoid issues like this by using set or by using the full expression instead of a name for it

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 22:29):

Is the issue that you are using the banned predicate > instead of the officially sanctioned <? Not sure if this is relevant

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:30):

here's a #mwe

import tactic
import data.real.basic

example {P : Prop} (a b : ) (hab : b < a) (h :  ε > (0:), P) : P :=
begin
  specialize h ((a - b) / 2) (by linarith),
  exact h,
end

example {P : Prop} (a b : ) (hab : b < a) (h :  ε > (0:), P) : P :=
begin
  let ε := (a - b) / 2,
  have  : ε = (a - b) / 2, refl,
  specialize h ε (by linarith),
  exact h,
end


example {P : Prop} (a b : ) (hab : b < a) (h :  ε > (0:), P) : P :=
begin
  set ε := (a - b) / 2 with ,
  specialize h ε (by linarith),
  exact h,
end

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:32):

Thanks for the MWE. In the second example, it looks like you can replace simp only [eq_self_iff_true] with refl.

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:33):

hah thanks, I am silly

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:34):

Kevin Buzzard said:

Is the issue that you are using the banned predicate > instead of the officially sanctioned <? Not sure if this is relevant

I just tried reversing the inequalities, and linarith still doesn't seem to notice the definition of epsilon.

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:34):

I guess one of your questions is "how do i complete the following proof in tactic mode"?

import tactic
import data.real.basic

example {P : Prop} (a b : ) (hab : b < a) (h :  ε > (0:), P) : P :=
begin
  let ε := (a - b) / 2,
  specialize h ε _, exact h,

end

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:36):

My best guess at the answer is have : ε = (a - b) / 2 := by refl, linarith

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:37):

I think you're just supposed to keep the definition of \e in context

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:38):

the tactic state gives a handy little reminder how \e is defined but if you want to do math you need the theorem that \e and some other thing are equal

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:38):

Do you think there's any reason linarith doesn't consider definitions as equalities?

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:39):

(of course, other than the fact it's not programmed that way [yet])

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:39):

the difference between defeq and other kinds of equality is mysterious to me

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:39):

but notice that the refl tactic isn't free to apply. you wouldnt necessarily want it to run everytime linarith wants to do something

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:40):

I think set is essentially doing the refl tactic and substituting the definition into the rhs, but I haven't checked

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:41):

Speaking of which, I know unfold can unfold certain definitions, but how do you "unfold" the definition of, say, epsilon in an expression?

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:42):

this takes noticeably long to run on my computer:

example : 1001 + 1000 = 2001 := by refl

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:42):

Oh, got it, dsimp only [ε]

view this post on Zulip Jalex Stark (Jun 05 2020 at 22:43):

so this is the final result?

import tactic
import data.real.basic

example {P : Prop} (a b : ) (hab : b < a) (h :  ε > (0:), P) : P :=
begin
  let ε := (a - b) / 2,
  specialize h ε _, exact h,
  dsimp only [ε], linarith,
end

view this post on Zulip Kyle Miller (Jun 05 2020 at 22:48):

That seems like the best approach so far (assuming the definition of epsilon is given to you and you can't turn it into a set). It's a bit non-intuitive and backwards-feeling (ideally you could supply the positivity proof up-front), but at least the proof doesn't need you to have multiple copies of the definition of epsilon.

view this post on Zulip Mario Carneiro (Jun 05 2020 at 23:58):

Lets in the context are a little special. For most of lean automation the := ... part isn't visible - they look just like regular variables in the definition. So linarith will see that epsilon is a real number but nothing else. Some relatively recent changes have made it easier to get access to these definitions, but it still seems like a bad idea for linarith to eagerly unfold all lets because this could explode the state.


Last updated: May 17 2021 at 22:15 UTC