linarith bug

Stream: mathlib4

[Heather Macbeth]

Have we seen this (apparent?) linarith bug before?

import Mathlib.Tactic.Linarith

example (i n : ℕ) (h : (2:ℤ) ^ i ≤ 2 ^ n) : (0:ℤ) ≤ 2 ^ n - 2 ^ i := by
  linarith
/-
tactic failed, resulting expression contains metavariables
  Linarith.lt_irrefl
    (Eq.mp
      (Eq.mpr
          (id
            (congrFun
              (congrArg Eq
                (Eq.trans
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.neg_congr
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
.............
-/

[Scott Morrison]

I have to run in a moment, and haven't got to the bottom of this. The error is in linearFormsAndMaxVar.

[Scott Morrison]

It receives inequalities: [-1 < 0, 2 ^ i - 2 ^ n ≤ 0, 2 ^ n - 2 ^ i + 1 ≤ 0] (looks correct to me), but returns [[(0, -1)]<0, []≤0, [(0, 1)]≤0] , which I think is saying -1 < 0, 0 ≤ 0, 1 ≤ 0.

[Scott Morrison]

The 2 ^ i and 2 ^ n atoms are just being dropped.

[Scott Morrison]

Then we call ring on the output of FM on that we get an equation ring can't solve, and it is returning the metavariable.

[Scott Morrison]

Found it; it's a stupid variable shadowing bug.

[Scott Morrison]

!4#3760

[Heather Macbeth]

Thanks!