Stream: new members

Topic: Unexpected behaviour of linarith

Jiang Jiedong (Apr 23 2023 at 11:41):

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,
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 (Apr 23 2023 at 12:04):

@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 (Apr 23 2023 at 12:05):

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 (Apr 23 2023 at 17:43):

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 (Apr 23 2023 at 17:45):

λ (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 (Apr 23 2023 at 18:03):

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 (Apr 23 2023 at 18:17):

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

Kevin Buzzard (Apr 23 2023 at 21:50):

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

Last updated: Dec 20 2023 at 11:08 UTC