## Stream: new members

### Topic: linarith and let

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

#### 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

#### 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

#### 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 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 (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.

#### Jalex Stark (Jun 05 2020 at 22:33):

hah thanks, I am silly

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

#### 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


#### Jalex Stark (Jun 05 2020 at 22:36):

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

#### Jalex Stark (Jun 05 2020 at 22:37):

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

#### 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

#### Kyle Miller (Jun 05 2020 at 22:38):

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

#### Kyle Miller (Jun 05 2020 at 22:39):

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

#### Jalex Stark (Jun 05 2020 at 22:39):

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

#### 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

#### 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

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

#### Jalex Stark (Jun 05 2020 at 22:42):

this takes noticeably long to run on my computer:

example : 1001 + 1000 = 2001 := by refl


#### Kyle Miller (Jun 05 2020 at 22:42):

Oh, got it, dsimp only [ε]

#### 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


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

#### 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