# Zulip Chat Archive

## 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,
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 (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