linarith question

Stream: general

[Gihan Marasingha]

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]

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]

by {unfold r, linarith} should work

[Kevin Buzzard]

by {unfold r at h, linarith}

[Gihan Marasingha]

Brilliant. Thanks @Kevin Buzzard and @Eric Wieser

[Kevin Buzzard]

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]

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]

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

[Shi You]

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

截屏2021-11-30-下午9.45.32.png

[Shi You]

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

[Anne Baanen]

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

[Anne Baanen]

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

[Eric Rodriguez]

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]

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]

Thx, I solved this problem myself.