Le.le simp_arith Int issue

Stream: mathlib4

[N.J. Lohmann]

Hi I'm new here, so please correct me if this isn't the right location for the topic.

I was just playing around with inequalities involving Int's, when this happened

import Mathlib.Init.Algebra.Order
import Mathlib.Data.Int.Order.Basic

def transIntContradiction {a b c : ℤ} (h: a < b) (h₂: b < c) : c < a ↔ False := by
  have hh: a < c := by apply Int.lt_trans h h₂
  simp_arith
  apply Int.le_of_lt hh
  done

it highlights transIntContradiction red with the message

application type mismatch
  LE.le a
argument has type
  ℤ
but function has type
  ℕ → ℕ → PropLean 4

replacing simp_arithwith simp solves the issue.
Is this behavior expected and if so why?

I'm using Mathlib b0cc02 and lean4:nightly-2023-05-31.

[Yury G. Kudryashov]

It looks like simp_arith applies lemmas about natural numbers without looking at the actual types.

[N.J. Lohmann]

if this is a bug, for which modules should I look out, to try a fix (although I'm not sure if that's in my reach yet)?

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

Sorry, this was a bad answer.

[Yury G. Kudryashov]

There is a TODO in Lean.Meta.Tactic.LinearArith.Simp saying "TODO: add support for Int and arbitrary ordered comm rings"

[Yury G. Kudryashov]

So,

• the tactic is in the core Lean;
• the developers know about the bug;
• you can try to fix it but this is going to involve quite some metaprogramming and you should ask someone else to help.

[Yury G. Kudryashov]

In the meantime, I think that information about this limitation of simp_arith should be added to #tpil4. Feel free to make a PR to https://github.com/leanprover/theorem_proving_in_lean4

[Jireh Loreaux]

bug reports aside, isn't the real answer here just to use linarith?

[Yury G. Kudryashov]

I assumed that the question was "what's wrong with simp_arith", not "how do I prove it".

[Jireh Loreaux]

Yeah, but "I'm new here" makes me suspect the OP is just unaware of linarith.

[N.J. Lohmann]

thanks for the update! So I guess, this is indeed out of my scope. Yes I'm aware of linarith, but wanted to try some of the syntax from the new docs (theorem proving in lean), so the main question was if the behavior is intentional or a bug.