norm_num and abs

Stream: new members

[Rado Kirov]

I have been using norm_num tactic to deal with all equalities and inequalities that have no variables, but was surprised that it failed to prove the following

example : |(1:ℚ) / 5| < 1 / 3 := by norm_num

while it has no problem showing

example : |(1:ℚ) / 5| = 1 / 5 := by norm_num

and

example : (1:ℚ) / 5 < 1 / 3 := by norm_num

minimal repro
https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQP0CmIISc6AjAFxwA+AFFYFiEAlHAPRwCsNcAvHOXZc4lflgCecAHbQQAfSkBXEDgC0quABMIBAM5SA5PADu0ANb4iJMgCZq9Jqw7c4AHgFCAzCLGSZUeSUVdThTKDNdS2JSdE97BkoWIRd3QQ5vUTgJHDg4KGM4AG0KAF0c6VkFZSjrdAAWagSk5zcPdJ8sv0qgnCA

[Jakub Nowak]

You can post code, instead of the link to live.lean-lang.org

import Mathlib

lemma l1: |(1:ℚ) / 5| = 1 / 5 := by norm_num
-- doesn't work
lemma l2: |(1:ℚ) / 5| < 1 / 3 := by norm_num
-- works
lemma l3: |(1:ℚ) / 5| < 1 / 3 := by
  rw [l1]
  norm_num
lemma l4: (1:ℚ) / 5 < 1 / 3 := by norm_num

There's a button in the upper-right corner of the code box, that opens live.lean-lang.org with that code. This is also preferred than posting a link, as this allows to view the code directly in your message without having to open the link.

[Rado Kirov]

Oh neat, I haven't noticed that button. In any case the repro is minimal, basically already in the post.

[Jakub Nowak]

I think there aren't extension to norm_num for abs (at least not for ℚ).

norm_num uses some parts of simp too, that's why it was able to solve l1. Notice that l3 and l4 can be solved by norm_num1, but cannot be solved by simp.
On the other hand l1 can be solved by simp, but cannot be solved by norm_num1.

[Ruben Van de Velde]

I'd say this is in scope for norm_num, but probably nobody's gotten around to writing the code for it

[Rado Kirov]

Should I file a GitHub issue somewhere? Also if someone points me in the right direction I can attempt to make a PR

[Ruben Van de Velde]

I've had a lot of help from @Robin Arnez when trying to extend norm_num

[David Renshaw]

I took a swing at it. Here's how far I got before getting frustrated with typeclasses and Qq: mathlib4#29223

[David Renshaw]

Please feel free to pick up where I left off.

[Rado Kirov]

Nice, thanks for sharing! Lots of new things to learn. I do have experience writing compilers and AST transformations for JS/TS but this feels a whole different world. Sounds like a fun challenge. Any documentation on writing tactics I should start with?

[David Renshaw]

I couldn't stop myself from finishing the remaining cases: mathlib4#29223