## 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.

#### Shi You (Nov 30 2021 at 13:48):

I found an error regarding to the tactic linarith

example : finitelySolvable x (λ x, x ^ 2 - 5 * x + 6 = 0) :=
Exists.intro {2,3}
begin
split,
{
assume h1,
have h2: (x - 2) * (x - 3) = 0, linarith,
show x = 2 ∨ x = 3, from equation_solve x 2 3 h2
},
{
assume h1,
have h2: x = 2 ∨ x = 3, exact h1,
show _,  from or.elim h2 (λ t, by linarith) (λ t, by linarith)
}
end


#### Shi You (Nov 30 2021 at 13:49):

if x = 2, then the equation should hold true.

#### Anne Baanen (Nov 30 2021 at 13:50):

What happens if you inform linarith to use t : x = 2, by writing λ t, by linarith [t]?

#### Anne Baanen (Nov 30 2021 at 13:52):

Alternatively, since the outcome should be a specific number, you should be able to write λ t, by norm_num [t].

#### Eric Rodriguez (Nov 30 2021 at 13:54):

it would also be nice if you have the deifnition of finitelySolvable, because we can't try this out ourselves on our own computers

#### Rob Lewis (Nov 30 2021 at 14:08):

This problem isn't linear, so it's not in scope for linarith. nlinarith would solve it. But as Anne says, norm_num is probably the better approach.

#### Shi You (Dec 02 2021 at 11:40):

Thx, I solved this problem myself.

Last updated: Dec 20 2023 at 11:08 UTC