linarith failure

Stream: mathlib4

[Heather Macbeth]

This turned up in mathlib4#1304, looks like a linarith bug to me?

import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Tactic.Linarith

variable [LinearOrderedField α] (x : α)

example (h : 0 ≤ x) : 0 ≤ x := by
  linarith -- works

example : 0 ≤ x := by
  have h : 0 ≤ x := sorry
  linarith -- linarith failed to find a contradiction

[Heather Macbeth]

Possibly related: with the same setup,

example : 0 ≤ x := by
  have h : 0 ≤ x := sorry
  linarith [h]

fails with two errors, "unknown identifier 'h'" as well as "linarith failed to find a contradiction"

[Heather Macbeth]

Also possibly related:

import Mathlib.Tactic.Linarith

variable [LinearOrderedRing α] (x : α)

example (h : 0 ≤ x) : 0 ≤ x := by linarith

fails with

tactic failed, resulting expression contains metavariables
  Linarith.lt_irrefl
    (Eq.mp (?m.1237 ▸ Eq.refl (-x + x < 0)) (add_lt_of_le_of_neg (neg_nonpos_of_nonneg h) (lt_zero_of_zero_gt a✝)))

[Heather Macbeth]

:ping_pong: these linarith failures -- I suspect the tactic is unusable while they remain. Maybe @Mario Carneiro has some ideas?

[David Renshaw]

I expect both of these linarith calls to succeed, but only the second one does.

import Mathlib.Tactic.Linarith
import Mathlib.Data.Real.Basic

lemma foo {f : ℚ → ℝ} {x a: ℚ} (N:ℕ)
    (h1 : ↑x + ↑(a ^ N - x) = f x + f (a ^ N - x))
    (h2 : ↑x ≤ f x) :
    f x = ↑x := by
  have h3 : ↑(a ^ N - x) ≤ f (a ^ N - x) := by sorry
  linarith -- "failed"

theorem bar (f : ℚ → ℝ) (x a : ℚ) (N : ℕ)
    (h1 : ↑x + ↑(a ^ N - x) = f x + f (a ^ N - x))
    (h2 : ↑x ≤ f x)
    (h3 : ↑(a ^ N - x) ≤ f (a ^ N - x)) :
    f x = ↑x := by linarith
-- succeeds

[David Renshaw]

more minimal:

import Mathlib.Tactic.Linarith
import Mathlib.Data.Real.Basic

lemma foo (a b c d : ℝ)
    (h1 : a + b = c + d)
    (h2 : a ≤ c) :
    a = c := by
  have h3 : b ≤ d := by sorry
  linarith -- "failed"

lemma bar (a b c d : ℝ)
    (h1 : a + b = c + d)
    (h2 : a ≤ c)
    (h3 : b ≤ d) :
    a = c := by linarith
-- succeeds

[David Renshaw]

same problem if I use the integers or rationals instead of the reals

[David Renshaw]

lemma bar (a : ℚ) :
    a = a := by
  have h : True := True.intro
  linarith
-- "failed"

[David Renshaw]

am I messing up the syntax somehow?

[Patrick Massot]

I have a much more spectacular failure:

import Mathlib.Data.Real.Basic

example (ε : ℝ) (h : 0 < ε) (h' : ε ≤ ε/2) : False := by
  -- rw [← sub_nonpos, sub_half] at h'
  linarith

linarith alone fails, but it succeeds if you rewrite first.

[Mario Carneiro]

this one seems more like the issue that linarith doesn't support Rat yet

[Mario Carneiro]

david's issues look like missing whnf or withMainContext somewhere

[Patrick Massot]

I was over-complicating,

example (ε : ℝ) (h : 0 < ε) : 0 ≤ ε/2 := by
  linarith

already fails...

[Mario Carneiro]

yes, linarith doesn't recognize division so this is expected

[David Renshaw]

this isEq is returning false in my example: https://github.com/leanprover-community/mathlib4/blob/0988583c8cfbda4e61eca01b42d7abaf65a7d45f/Mathlib/Tactic/Linarith/Frontend.lean#L269

[David Renshaw]

x = [mdata noImplicitLambda:1 Eq.{1} Rat _uniq.7 _uniq.7]

[David Renshaw]

I wonder if that mdata thing is messing stuff up

[Mario Carneiro]

yup, that's exactly the same bug found in abel not long ago

[David Renshaw]

is there an easy fix?

[Mario Carneiro]

whnfR after the instantiateMVars

[David Renshaw]

yep! that does it

[David Renshaw]

I'll put up a PR

[David Renshaw]

https://github.com/leanprover-community/mathlib4/pull/1930