## Stream: general

### Topic: linarith question

#### Gihan Marasingha (Jan 02 2021 at 12:50):

In proving acc nat.lt 0, why doesn't the bottom line below work even though the penultimate line (in which I replacer with its definition) does work?

import tactic

@[reducible]
def r := λ (m n : ℕ), m < n

example : acc r 0 := acc.intro 0 (λ y h, absurd h (nat.not_lt_zero y))
example : acc r 0 := ⟨0, (λ y h, absurd h (nat.not_lt_zero y))⟩
example : acc (λ (m n : ℕ), m < n) 0 := ⟨0, (λ y h, by linarith)⟩
-- example : acc r 0 := ⟨0, (λ y h, by linarith)⟩  /- Doesn't work -/


I see exactly the same behaviour if I replace r with nat.lt.

#### Kevin Buzzard (Jan 02 2021 at 12:54):

linarith failed to find a contradiction
state:
y : ℕ,
h : r y 0
⊢ false


I don't think linarith has much hope with that one.

#### Eric Wieser (Jan 02 2021 at 12:54):

by {unfold r, linarith} should work

#### Kevin Buzzard (Jan 02 2021 at 12:55):

by {unfold r at h, linarith}

#### Gihan Marasingha (Jan 02 2021 at 12:55):

Brilliant. Thanks @Kevin Buzzard and @Eric Wieser

#### Kevin Buzzard (Jan 02 2021 at 12:56):

So the answer to your question is (1) your error message tells you exactly what state Lean was in when it failed, and (2) if you understand the scope of the linarith tactic you will know that it won't do random unfolding for you (why should it? It might fall into a rabbithole).

#### Kevin Buzzard (Jan 02 2021 at 12:57):

I remember learning this a while ago -- I was surprised linarith couldn't prove a < b when one of the hypotheses was h : a < b \and (something else).

#### Kevin Buzzard (Jan 02 2021 at 12:57):

But then it was patiently explained to me how you can't expect every tactic to be a kitchen sink tactic.

Last updated: May 08 2021 at 09:11 UTC