Unexpected behaviour of linarith

Stream: new members

[Jiang Jiedong]

Hi everyone! I was doing the last piece of the tutorial project. In exercise 0072, I met a subgoal that I thought linarith would solve but actually not.
The subgoal is

1 goal
A: set ℝ
x: ℝ
h: is_sup A x
u: ℕ → ℝ
hu: ∀ (n : ℕ), u n ∈ A ∧ x - 1 / (n + 1) < u n
⊢ ∀ (n : ℕ), x - 1 / (n + 1) ≤ u n

If I write

          intros n,
          specialize hu n,
          linarith,

lean will show the following message:

linarith failed to find a contradiction
state:
A : set ℝ,
x : ℝ,
h : is_sup A x,
u : ℕ → ℝ,
n : ℕ,
h_1 : u n ∈ A,
h_2 : x - 1 / (n + 1) < u n,
ᾰ : x - 1 / (n + 1) > u n
⊢ false

But don't h_2 and ᾰ form a contradiction detectable by linarith? However, if I write

          intros n,
          specialize hu n,
          by_contradiction hyp,
          push_neg at hyp,

lean returns

1 goal
A: set ℝ
x: ℝ
h: is_sup A x
u: ℕ → ℝ
n: ℕ
hu: u n ∈ A ∧ x - 1 / (n + 1) < u n
hyp: u n < x - 1 / (n + 1)

and a further line of linarith could solve the goal from here. I am very confused. What causes the different behaviour of linarith in the above two cases? What should I be careful about when I use linarith?

[Kyle Miller]

@Jiang Jiedong There are some pretty printer options set in the tutorial that can lead to confusing situations like this.

To set them to their default values, try putting set_option pp.beta false and set_option pp.coercions true on lines right before the theorem/lemma/example you are proving.

[Kyle Miller]

I am expecting you have some beta-reducible lambda expressions in one of your hypotheses. You can do dsimp only at h (for example) to do lambda calculus simplifications at the hypothesis h, if it's indeed the case there are lambdas in your expression.

[Jiang Jiedong]

Thank you! @Kyle Miller After I put set_option pp.beta false and set_option pp.coercions true, the goal changed to (λ (n : ℕ), x - 1 / (↑n + 1)) n ≤ u n, which can be solved by linarith after a line of dsimp only. I don't understand about lambda expressions and beta-reductions. There is so much to learn :)

[Kyle Miller]

λ (n : ℕ), x - 1 / (↑n + 1) can be read as the function n ↦ x - 1 / (n + 1) in more normal mathematical notation, where the up-arrow in the original (based on the context) means "this natural number should be interpreted as a real number"

[Jiang Jiedong]

Oh I see, dsimp evaluates the function λ (n : ℕ), x - 1 / (↑n + 1) at n, which linarith failed to do. Thank you very much!

[Kyle Miller]

Yep, and this sort of symbolic evaluation is known as "beta reduction"

[Kevin Buzzard]

For what it's worth, here are the most important "Greek letter reduction" codes: https://leanprover.github.io/reference/expressions.html#computation