tutorial 0079

Stream: new members

[Kyle Miller]

At the end of my proof for this exercise, what remains is to show -M ≤ f x given -f x ≤ M, and for some reason linarith is not working for me. The proof I'm trying is

-- 0079
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 hf' := λ (x : ℝ) (H : x ∈ Icc a b), continuous_opposite (hf x H),
  rcases bdd_above_segment hf' with ⟨M,bdd⟩,
  use -M, intros x inc, specialize bdd x inc,
  linarith,
end

I know the proof is "good" since I can insert the following two lines before linarith to rewrite the inequalities as 0 ≤ M + f x and 0 ≤ f x + M:

  rw ← sub_nonneg, rw ← sub_nonneg at bdd,
  simp at bdd, simp,

and then linarith will do its job.

The linarith tactic still seems unhappy even if I clear out everything from the current context but the inequality and the types of the variables. Strangely, the exercise's solution successfully uses linarith with almost exactly the same context.

(My best guess is that the lambda expression is being beta reduced only in the goal viewer, but for some reason linarith can't deal with that; however, linarith! doesn't work either. Whatever is going on, I'm not sure how to deal with it properly.)

[Mario Carneiro]

Do you have a #mwe?

[Mario Carneiro]

Have you tried have : -f x ≤ M := inc, show -M ≤ f x, linarith?

[Mario Carneiro]

if there is any funny business going on in the types of inc or the goal this should fix it

[Kyle Miller]

Mario Carneiro said:

Do you have a #mwe?

I thought referencing a tutorial exercise counted as a #mwe, especially for a proof as short as this, though I do appreciate how having a self-contained example would be better.

It does turn out that

have : -f x ≤ M := bdd, linarith,

is enough to make linarith happy. What is frustrating is that in the goal window, bdd : -f x ≤ M is literally one of the hypotheses. How can I figure out what makes linarith fail here? Expanding on what I said earlier, all I can guess is that the goal window automatically beta reduces (λ (x : ℝ), -f x) x, but somehow this is not equivalent to -f x in the eyes of linarith.

[Alex J. Best]

A link to the tutorial exercise would be good (in place of a MWE). There are a couple of things out there that could be called tutorial (the old lean one, the new community one), I guess you mean the new one though?

[Mario Carneiro]

For a question like this it is really best to actually extract a MWE not using the tutorial. Use the usual techniques: put it in its own file, stub out everything that doesn't matter while preserving the interesting failure until you have something that is actually a test case for linarith

[Kyle Miller]

Alex J. Best said:

A link to the tutorial exercise would be good (in place of a MWE). There are a couple of things out there that could be called tutorial (the old lean one, the new community one), I guess you mean the new one though?

I'm following what you get from leanproject get tutorials, and its README said to just create a zulip thread like 'tutorials NNNN'. Here's a link to the solution, which is almost the same as mine: https://github.com/leanprover-community/tutorials/blob/master/src/solutions/09_limits_final.lean#L317

The difference seems to be the way it constructs the hypothesis I called hf', which seems to effectively incorporate the have : -f x ≤ M := bdd fix.

[Mario Carneiro]

the point of a MWE isn't just so that people know what you are talking about, it is so that the problem is isolated. This is half of the way to the solution and you may find you have solved the problem before you even post it

[Kyle Miller]

Mario Carneiro said:

the point of a MWE isn't just so that people know what you are talking about, it is so that the problem is isolated. This is half of the way to the solution and you may find you have solved the problem before you even post it

I get that, and I'm working on making a MWE (and figuring out some basics to do so that haven't been covered by the tutorials so far...), but, while I can see why it appears the question is about linarith, it's actually this: is there any general advice for how to deal with a misleading goal window? (And a followup: is there a tactic that will do whatever have : -f x ≤ M := bdd is doing without my having to type out a hypothesis?)

To be somewhat more complete about what I mean by misleading, in the linked solution, the context right before the use of linarith has hM : -f x ≤ M and for mine it has bdd : -f x ≤ M, yet for some reason this is different. This is rather frustrating for someone just learning Lean.

[Bryan Gin-ge Chen]

set_option pp.implicit true (or set_option pp.all true) will disable some of the pretty-printing which can help distinguish such goals. Try #help options to see all such options.

Unfortunately, there's still a ton of frustrating things about learning and using Lean...

[Kyle Miller]

Bryan Gin-ge Chen said:

set_option pp.all true

Thanks for the suggestion; I wasn't aware of the pretty print options. Setting set_option pp.beta false and then doing have bdd': -f x ≤ M := bdd results in a context containing

bdd : (λ (x : ℝ), -f x) x ≤ M,
bdd' : -f x ≤ M

This suggests my theory about beta reduction might be correct. Is there a tactic that will beta reduce something like the left-hand-side of bdd? (Or am I fundamentally mistaken that this should be possible?)

[Bryan Gin-ge Chen]

dsimp at bdd works.

[Kyle Miller]

Bryan Gin-ge Chen said:

dsimp at bdd works.

It looks like I should have tried simp at bdd. Thanks, this is enough of a solution for me for now.

[Kyle Miller]

It turns out the tutorial file contains set_option pp.beta true at the top, which is what led to all this confusion. Is there a reason for it being there?

Here's a MWE showing how it's confusing:

import data.real.basic
open real

set_option pp.beta true -- this is at the top of 09_limits_final.lean

example {x : ℝ} (H : x ≥ 0) : (x ≥ 0) :=
begin
  have H' : (λ x, -x) x ≤ 0,
    simp, exact H,
  clear H,
  linarith, -- fails, because H' is not actually -x ≤ 0, despite what the goal window shows.
end

(Adding simp at H' before linarith saves the proof.)

[Mario Carneiro]

this is why the option is disabled by default in the first place

[Kevin Buzzard]

(deleted)

[Patrick Massot]

I really think people should stop asking for a mwe when a message topic is tutorial NNNN. This whole mwe thing is very unwelcoming but it is usually necessary, we have no other option in general. Here everybody interested in helping beginners can type leanproject get tutorials and wait 15 seconds. You don't have to do it for every question, the tutorials haven't change since they were released, and I don't plan to change them (the plan is #mil taking over).

[Patrick Massot]

Let me turn to the question now. In my course where these exercises began their life, I have set_option pp.beta true on top of many files, because this is a course in mathematics, and it doesn't make any sense to write non-beta reduced things in the real world. To be honest I have no idea why Lean tolerates non beta-reduced terms, I guess it's for performance reasons. Now the surprising thing is I think no student ever met this issue. It would be very annoying otherwise. In the tutorials project context the situation is different, the focus is more on teaching Lean and less on teaching how to prove stuff. So here it definitely makes sense to remove that pp option, and add a paragraph of explanations about dsimp only at bdd before the first exercise where it could show up. PR welcome.