## Stream: new members

### Topic: Linarith weirdness

#### Peter Nelson (Aug 16 2020 at 04:52):

I'm trying to do problem 79 from the tutorials, and I have the following.

lemma bdd_below_segment {f : ℝ → ℝ} {a b : ℝ} (hf : ∀ x ∈ Icc a b, continuous_at_pt f x) :
∃ m, ∀ x ∈ Icc a b, m ≤ f x :=
begin
have negfcont : ∀ x ∈ Icc a b, continuous_at_pt (λ x, -f(x)) x,
{ intros x xicc,
apply continuous_opposite,
exact hf x xicc, },

have negfub := bdd_above_segment negfcont,

cases negfub with m hm,

use -m,
intros x xicc,
specialize hm x xicc,
linarith,

end


Before the last linarith line, my last hypothesis is hm: -f x ≤ m my goal is -m ≤ f x. However, linarith can't finish this. My solution seems isomorphic to the one in the solutions file.

I'm sure I'm missing something simple, but I'm stumped. Can anyone help me with this?

#### Kyle Miller (Aug 16 2020 at 04:58):

I'll check, but in the meantime, try uncommenting set_option pp.beta true at the top. You should then see that hypothesis or goal is not what you think it is. Use dsimp only or dsimp only at hm to beta reduce the lambda expression.

#### Alex J. Best (Aug 16 2020 at 04:59):

library_search will find the lemma that does this in this case.

#### Alex J. Best (Aug 16 2020 at 05:00):

I'm not sure why linarith doesn't but by setting set_option trace.linarith true we can see that it makes it to [f x - -m < 0, -f x - m ≤ 0]

#### Kyle Miller (Aug 16 2020 at 05:00):

Ok, I just checked. The hypothesis is actually

hm : (λ (x : ℝ), -f x) x ≤ m,


The issue is that linarith does not try to beta reduce terms when it figures out all the variables and coefficients.

#### Kyle Miller (Aug 16 2020 at 05:02):

I remember it being especially frustrating running into this exact issue in this exact exercise when I was first learning Lean. (I've been meaning to submit a PR to remove the set_option pp.beta true from the tutorial, but I haven't gotten around to it.)

#### Kyle Miller (Aug 16 2020 at 05:04):

Another thing you can do instead of dsimp only at hm is

change -f x ≤ m at hm,


which tells Lean to try to unify hm with the given expression, replacing hm with the given expression. You can put _ holes in a change tactic, too.

Last updated: May 11 2021 at 21:10 UTC