linarith and let

Stream: mathlib4

[Dan Velleman]

In the following example, linarith fails:

import Mathlib.Tactic

example : True := by
  let n := 1
  have h : n < 2 := by linarith
  trivial

Shouldn't this work?
I could be mistaken, but I think it used to work. Did something change?

[Fengyang Wang]

I might be over explaining, but here's how I understand it.
You have let n := 1. This is a let-binding: n is definitionally equal to 1. The kernel can unfold n to 1. However, this is not a hypothesis h : n = 1, and linarith does not unfold let-bindings. It operates though

1. Collect hypotheses
2. Negate the goal
3. Search for a contradiction

So you may fix it with

• Parse let as a hypothesis

example : True := by
  let n := 1
  have h : n < 2 := by
    have : n = 1 := by rfl
    linarith
  trivial

• Use omega, which unfolds let

example : True := by
  let n := 1
  have h : n < 2 := by
    omega
  trivial

• Take it as a decidable proposition

example : True := by
  let n := 1
  decide          -- norm_num, native_decide, etc. all work

[Dan Velleman]

That makes sense. But I think this used to work. Did linarith used to unfold let-bindings, and was it changed? Or am I remembering wrong?

[Fengyang Wang]

Dan Velleman said:

That makes sense. But I think this used to work. Did linarith used to unfold let-bindings, and was it changed? Or am I remembering wrong?

Your question intrigues me on what linarith can and cannot unfold. Here's a snippet that shows the behavior of whnfR(Weak Wead Normal Form with Reducible transparency) that linarith operates on

import Lean

open Lean Meta Elab Term Tactic

elab "#demo_whnfR" t:term : command => do
  Command.liftTermElabM do
    let e ← elabTerm t none
    let e ← instantiateMVars e

    IO.println s!"Original:  {← ppExpr e}"

    -- whnfR: reducible transparency (default for linarith)
    let whnfR_result ← withTransparency .reducible <| whnf e
    IO.println s!"whnfR:     {← ppExpr whnfR_result}"

    IO.println ""


-- Reducible definitions are unfolded
@[reducible] def myId (x : Nat) : Nat := x
#demo_whnfR myId 42
-- Original:  myId 42
-- whnfR:     42

-- ## Non-reducible definitions are NOT unfolded
def myConst (x : Nat) : Nat := x
#demo_whnfR myConst 42
-- Original:  myConst 42
-- whnfR:     myConst 42  (unchanged!)

As for why it is implemented this way, then we are going into deep type theory and the meta-programming. I also took a look at lean3 doc for linarith, it doesn't invoke explicitly whnfR, so I can't conclude anything of how it might behave. But it's reasonably possible that you remembered the lean3 application of linarith

RM: Even with transparency enabled linarith! (lean4), it does not invoke ζ-reduction and does not unfold let binding

example : True := by
  let n := 1
  have h : n < 2 := by
    linarith!     --linarith still failed to find a contradiction
  trivial

But in practice, we may as well resort to aesop?

[Artie Khovanov]

A general workaround is the tactic set. Usage: set a := t with h gives a let-bound to t with h : a = t. set also automatically rewrites all occurences of t in the context into a.

[Kyle Miller]

@Artie Khovanov let (eq := h) a := t gives you that h : a = t (I think this was released 6mo ago or so)

[Artie Khovanov]

Oh nice, wasn't aware! Is this in core?

[Kyle Miller]

Yep!

[Kyle Miller]

@Dan Velleman One piece of the puzzle here seems to be that it's specific to Nat. It succeeds if you use Int (or other rings):

example : True := by
  let n : ℤ := 1
  have h : n < 2 := by linarith
  trivial

[Kyle Miller]

I haven't checked changes to linarith, but it seems like it has something to do with the order in which it decides on what the atoms are vs when it coerces everything to Int

[Kyle Miller]

Do you specifically want this to work with Nat?

[Jakub Nowak]

lia works. Isn't linarith going to be depracated in favor of lia?

[Dan Velleman]

@Kyle Miller My interest in Lean is primarily for education. I don't think this is very important, but if a student stumbled over this I think they would find it confusing. And I wouldn't want to have to give an explanation about identifying atoms and coercing to Int.

[Aaron Liu]

Jakub Nowak said:

lia works. Isn't linarith going to be depracated in favor of lia?

no, lia only does linear integer arithmetic, but linarith does linear arithmetic in any linearly ordered ring

[Kyle Miller]

@Dan Velleman That's fair — and I my little digging into atoms and coercions is just meant to be a hint for whoever wants to try digging deeper into this.

My feeling is that linarith ought to add equalities for each of the let bindings in scope. Or I guess it could zeta reduce every relevant let binding first. There doesn't seem to be any obvious, reliable way to fix this through tweaks of just the Nat->Int coercion preprocessor.

Worst case, you can explain to students that linarith is unreliable for natural numbers, since it's for linear arithmetic, and Nat doesn't have negatives. It doesn't seem necessary to get into the weeds of atoms and coercions to explain why it works only sometimes for Nat. (I get it though that then this takes explaining that Nat isn't a subset of Int.)