Linarith weirdness

Stream: new members

[Peter Nelson]

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]

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]

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

[Alex J. Best]

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]

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]

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]

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.