linarith fails in a simple example

Stream: mathlib4

[Michael Stoll]

I have a tactic state as follows:

xy: ℂ
hx₀: x ≠ 0
hx₁: -Real.pi / 2 < arg x
hx₂: arg x ≤ Real.pi / 2
hy₀: y ≠ 0
hy₁: -Real.pi / 2 < arg y
hy₂: arg y ≤ Real.pi / 2
k: ℤ
hk: arg (x * y) - (arg x + arg y) = 2 * Real.pi * ↑k
H₁: -2 * Real.pi < arg (x * y) - (arg x + arg y)
H₂: arg (x * y) - (arg x + arg y) < 2 * Real.pi
H₂': k < 1
H₁': -1 < k
⊢ k = 0

Here linarith "fails to find a contradiction", but have : k = 0 := by linarith; exact this works.

WE (not minimal; see this thread for context):

import Mathlib.Analysis.SpecialFunctions.Complex.Log

lemma arg_mul {x y : ℂ} (hx₀ : x ≠ 0) (hx₁ : -Real.pi/2 < x.arg) (hx₂ : x.arg ≤ Real.pi/2)
    (hy₀ : y ≠ 0) (hy₁ : -Real.pi/2 < y.arg) (hy₂ : y.arg ≤ Real.pi/2) :
    (x * y).arg = x.arg + y.arg := by
  have := arg_mul_coe_angle hx₀ hy₀
  rw [← Real.Angle.coe_add, Real.Angle.angle_eq_iff_two_pi_dvd_sub] at this
  obtain ⟨k, hk⟩ := this
  rw [← sub_eq_zero, hk]
  have H₁ : -2 * Real.pi < arg (x * y) - (arg x + arg y)
  · sorry
  have H₂ : arg (x * y) - (arg x + arg y) < 2 * Real.pi
  · sorry
  have H₁' : -2 * Real.pi < 2 * Real.pi * k := H₁.trans_eq hk
  have H₂' : 2 * Real.pi * k < 2 * Real.pi := hk.symm.trans_lt H₂
  rw [neg_mul, ← mul_one (-(2 * Real.pi)), neg_mul_comm, mul_lt_mul_left (by positivity)] at H₁'
  simp [Real.pi_pos, Real.pi_ne_zero, -neg_mul] at H₁' H₂' ⊢
  norm_cast at H₁' H₂'
  change -1 < _ at H₁' -- why does `norm_cast` introduce `Int.negSucc 0`??
  -- `linarith` does not work here
  have hk₀ : k = 0 := by linarith
  exact hk₀

[Alex J. Best]

This is very strange, the minified example is:

import Mathlib.Tactic.Linarith
--set_option pp.raw true
--set_option trace.linarith true
example (k : ℤ) (h : k < 1) (h₁ : -1 < k)
    : k = 0 := by
  -- linarith -- works
  change -1 < _ at h₁
  -- linarith -- fails!
  have hk : k = 0 := by
    linarith
  exact hk

But I cannot see why linarith suddely fails, the first stage of the linarith traces I can see that differs is in the strengthen int inequalities step, but I have no idea why

[David Renshaw]

sometimes this kind of thing is due to mdata: mathlib4#1930

[Kyle Miller]

pp.raw shows the exact same term -- I'm going to go with a missing withContext

[David Renshaw]

This seems to fix it.

diff --git a/Mathlib/Tactic/Linarith/Preprocessing.lean b/Mathlib/Tactic/Linarith/Preprocessing.lean
index 0b0aae659..c666acc9f 100644
--- a/Mathlib/Tactic/Linarith/Preprocessing.lean
+++ b/Mathlib/Tactic/Linarith/Preprocessing.lean
@@ -212,7 +212,7 @@ If `pf` is a proof of a strict inequality `(a : ℤ) < b`,
 and similarly if `pf` proves a negated weak inequality.
 -/
 def mkNonstrictIntProof (pf : Expr) : MetaM Expr := do
-  match (← inferType pf).getAppFnArgs with
+  match (← whnfR (← inferType pf)).getAppFnArgs with
   | (``LT.lt, #[_, _, a, b]) =>
     return mkApp (← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]) pf
   | (``GT.gt, #[_, _, a, b]) =>
@@ -233,7 +233,7 @@ into a proof of `t1 ≤ t2 + 1`. -/
 def strengthenStrictInt : Preprocessor where
   name := "strengthen strict inequalities over int"
   transform h := do
-    if isStrictIntComparison (← inferType h) then
+    if isStrictIntComparison (← whnfR (← inferType h)) then
       return [← mkNonstrictIntProof h]
     else
       return [h]

[David Renshaw]

I'll put up a PR

[David Renshaw]

I believe that it's an fvar (not an mdata as I previously guessed) that needs to be weak-head-normalized.

[David Renshaw]

mathlib4#8310

[Kevin Buzzard]

Nice detective work David!

[Alex J. Best]

Any thoughts on whether there is actually an underlying issue with change producing a sub-optimal term? Or is this just to be expected

[David Renshaw]

I looked into this a bit deeper.

In the failure case, when the strengthenStrictInt preprocessor does inferType on the h₁ : -1 < k hypothesis, it sees it as an mvar.
Adding a whnfR normalizes past that mvar, and makes the expression an app, so that the isStrictIntComparison function acts as expected.

[David Renshaw]

This makes me wonder whether we should additionally add in an instantiateMVars.

[David Renshaw]

Or maybe add that instead of whnfR.

[David Renshaw]

Alex J. Best said:

Any thoughts on whether there is actually an underlying issue with change producing a sub-optimal term? Or is this just to be expected

I think it's expected that change will produce a metavariable.

[Michael Stoll]

So the problem was caused by a combination of

  norm_cast at H₁' H₂'
  change -1 < _ at H₁' -- why does `norm_cast` introduce `Int.negSucc 0`??

and the fact that change produced a sub-optimal term for linarith to work with.

Is the norm_cast thing a bug?

import Mathlib.Tactic

example (n : ℤ) : (-37 : ℤ) = n := by
  norm_cast -- goal is `Int.negSucc 36 = -n`
  sorry

[David Renshaw]

Maybe the norm_cast thing is a delaborator bug?

[Alex J. Best]

Yeah that certainly looks like a bug too, but not the cause of this later one.

[Michael Stoll]

show_term norm_castgives

refine Eq.mpr (id (congrFun (congrArg Eq (Mathlib.Data.Int.Cast.Basic._auxLemma.3 36)) n)) ?_

where Mathlib.Data.Int.Cast.Basic._auxLemma.3 is not actually a lemma name ("unknown identifier"). It seems to be an auto-generated lemma from Mathlib.Data.Int.Cast.Basic.

[Michael Stoll]

And docs#Int.cast_negSucc has a norm_castattribute.

[Michael Stoll]

Trying attribute [-norm_cast] Int.cast_negSucc, I get the message "attribute cannot be erased".

[Michael Stoll]

The docs don't show the norm_castattribute, BTW. The source code is

open Nat

namespace Int

variable {R : Type u} [AddGroupWithOne R]

@[simp, norm_cast]
theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
  AddGroupWithOne.intCast_negSucc n

Does norm_cast apply these lemmas right-to-left?

[Michael Stoll]

The strange thing is that rw [← Int.cast_negSucc] does not work.

[Michael Stoll]

But I guess I would have to rewrite with the aux lemma, but I don't find a way to actually see it...

[Yaël Dillies]

norm_cast applies right to left, push_cast left to right.

[Michael Stoll]

The auto-generated lemma seems to look like this (found by copying into a file importing Mathlib and using whatsnew in):

theorem test : ∀ {R : Type u} [AddGroupWithOne R] (n : ℕ),
  -↑(n + 1) = (Int.negSucc n : R) :=
fun {R} [AddGroupWithOne R] n => (cast_negSucc n).symm

Then

example (n : ℤ) : (-37 : ℤ) = n := by
  refine (test 36).trans ?_
  rw [Int.cast_id]
  sorry

has the same effect as norm_cast.

[Michael Stoll]

Should the norm_cast attribute be removed? Or is it there for a good reason?

[Michael Stoll]

@Mario Carneiro Would you agree that it would make sense to remove the norm_cast attribute from Int.cast_negSucc? The way it is now, norm_cast exposes the ugly implementation details of Int.

[Mario Carneiro]

docs#Int.cast_negSucc

[Mario Carneiro]

Is it being used backwards by norm_cast? It doesn't seem like it would expose any implementation details if used in the forward direction

[Mario Carneiro]

norm_cast is supposed to categorize the lemmas it is given into a few groups depending on the shape, which determines whether it is used in the "push" or "pull" phases

[Michael Stoll]

Yes; see the example further up:

import Mathlib.Tactic

example (n : ℤ) : (-37 : ℤ) = n := by
  norm_cast -- goal is `Int.negSucc 36 = n`
  sorry

[Michael Stoll]

(deleted)

[Mario Carneiro]

that is, it could be an issue in the categorization, what happens if you use @[norm_cast squash] or so?

[Michael Stoll]

No idea. I don't know about the internal workings of norm_cast; I just came across a situation like the one in the example and thought that this is likely a bug.

[Mario Carneiro]

the question is whether it is something that better tagging can fix

[Mario Carneiro]

or if it is a bug in the tactic

[Michael Stoll]

I've now tried

@[simp, norm_cast squash]
theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
  AddGroupWithOne.intCast_negSucc n

and this makes the example behave as expected.
But I don't know if this has perhaps bad side effects, but I can try to find out.

[Michael Stoll]

#8365

[Scott Morrison]

Can we please merge https://github.com/leanprover/std4/pull/351 first?

[Michael Stoll]

What is that supposed to do?

[Scott Morrison]

It moves norm_cast to Std, and also sets up norm_cast lemmas in Std.

[Scott Morrison]

It's possible we can make the changes independently.

[Michael Stoll]

But docs#Int.cast_negSucc is in Mathlib.Data...
Anyway, the concrete use case where this came up was superseded by a better proof, so from my POV it is not urgent.

[Mario Carneiro]

yeah, this issue has nothing to do with std

[Michael Stoll]

In any case, #8365 is green now, so nothing broke.

[Michael Stoll]

What is squash meant to do, BTW?

[Michael Stoll]

Can #8365 be merged now?