Tactic `linarith` in Lean 3

Stream: general

[FR]

These days I'm trying to learn Lean. I downloaded https://github.com/leanprover-community/tutorials. Some hours ago, I met the problem below DGTLJ8YVO9D3TZSHNTK.png, but I didn't care. Now I find something more confusing. image.png image.png I wonder what happened to them.

[Floris van Doorn]

It's hard to help you from screenshots. Can you post a #mwe?

[FR]

Sorry for that, here is it. I noticed that it shows me a different type in this file (I don't know why). Maybe there is something about the problem.

[Patrick Massot]

linarith is not reducing the goal

[Patrick Massot]

You can force reduction using dsimp only before linarith

[Patrick Massot]

@Rob Lewis do you think linarith should try to beta-reduce the goal (and/or assumptions) before doing its work?

[FR]

Thank you! I found the following two lines in the origin file (I didn't notice them before).

set_option pp.beta true
set_option pp.coercions false

The first line makes it show me the type x₀ - 1 / (↑n + 1) ≤ u instead of (λ (n : ℕ), x₀ - 1 / (↑n + 1)) n ≤ u. However, there are no real effects. It's very confusing.

[Kevin Buzzard]

pp options just change what the pretty printer is printing, not the actual term as stored internally.

[Kevin Buzzard]

Forcing reduction with dsimp only is not an uncommon idiom.