Zulip Chat Archive

Stream: general

Topic: linarith question


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 02 2021 at 12:54):

by {unfold r, linarith} should work

view this post on Zulip Kevin Buzzard (Jan 02 2021 at 12:55):

by {unfold r at h, linarith}

view this post on Zulip Gihan Marasingha (Jan 02 2021 at 12:55):

Brilliant. Thanks @Kevin Buzzard and @Eric Wieser

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip 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