linarith and let

Stream: new members

[Kyle Miller]

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

[Jalex Stark]

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

[Kevin Buzzard]

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

[Jalex Stark]

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 hε : ε = (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 hε,
  specialize h ε (by linarith),
  exact h,
end

[Kyle Miller]

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

[Jalex Stark]

hah thanks, I am silly

[Kyle Miller]

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.

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Jalex Stark]

this takes noticeably long to run on my computer:

example : 1001 + 1000 = 2001 := by refl

[Kyle Miller]

Oh, got it, dsimp only [ε]

[Jalex Stark]

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

[Kyle Miller]

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.

[Mario Carneiro]

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.