nat fighting

Stream: mathlib4

[James Gallicchio]

Kim recently used the term "nat-fighting" and I really like the phrase :) I'm gonna use this thread to document any goals over nat that IMO should be within the scope of automation (let me know if there's a similar thread I should be sending these instead!)

[James Gallicchio]

first MWE:

import Mathlib

example (i j k l : Nat)
  : i * j + k + l - k = i * j + l
  := by
  try omega
  try linarith
  try aesop
  sorry

My manual proof would be something like

  rw [Nat.add_assoc, Nat.add_comm k, ← Nat.add_assoc]
  simp

[James Gallicchio]

MWE 2 (I am trying the same tactics for all of these)

example (i j k : Nat) : i ≤ j * i + i + k := by
  sorry

manual proof something like

  rw [Nat.add_comm _ i, Nat.add_assoc]; simp

[James Gallicchio]

MWE 3

example (i j k : Nat) : i ≤ i + j * j + k := by sorry

manually

  apply Nat.le_add_right_of_le
  simp

[James Gallicchio]

My experience with omega has been very positive but I also have no idea how it works internally, so I'm surprised omega does not work but only because it works on so many problems :big_smile:

[Damiano Testa]

James Gallicchio said:

first MWE:

import Mathlib

example (i j k l : Nat)
  : i * j + k + l - k = i * j + l
  := by
  try omega
  try linarith
  try aesop
  sorry

My manual proof would be something like

  rw [Nat.add_assoc, Nat.add_comm k, ← Nat.add_assoc]
  simp

You can also do

import Mathlib

example (i j k l : Nat)
  : i * j + k + l - k = i * j + l
  := by
  move_add [k]
  exact? says exact Nat.add_sub_self_right (i * j + l) k

[Damiano Testa]

The others can also follow a similar pattern:

import Mathlib

example (i j k : Nat) : i ≤ j * i + i + k := by
  move_add [i]
  exact? says exact Nat.le_add_left i (j * i + k)

example (i j k : Nat) : i ≤ i + j * j + k := by
  move_add [i]
  exact? says exact Nat.le_add_left i (j * j + k)

[Damiano Testa]

In case this is not clear: I would love for these to be further automated! Automating proofs with this kind of rearranging was one of my motivations for writing move_add!

[James Gallicchio]

move_add is a life-saver for doing these manually, thanks for the heads up

[James Gallicchio]

oh wait, maybe this is why omega isn't working here?

example (i : Nat) : i * i ≥ 0 := by
  omega -- fails

If I add such lemmas then the proof proceeds fine.

example (i j k : Nat) : i ≤ i + j * j + k := by
  have : j * j ≥ 0 := Nat.zero_le (j * j)
  omega

[Damiano Testa]

I do not know the internals of omega, but I am a little surprised that it helps to mention that a Nat is non-negative!

[Damiano Testa]

Judging from the error message, it seems to convert to Int before doing something. Maybe there is an option to add the Nat.zero_le inequalities for the various Int-coerced Nats.

[James Gallicchio]

It's to do with the multiplication:

example (i : Nat) : i ≥ 0 := by
  omega -- works

example (i : Nat) : i * i ≥ 0 := by
  omega -- fails

example (i : Int) : i ≥ 0 → i * i ≥ 0 := by
  intro; omega -- fails

I think omega might be able to add constraints to characterize multiplication sufficiently appropriately here though?

[Damiano Testa]

The doc-string does say that it is for linear problems (and without some constraints the general problem is undecidable). I also know that omega makes an effort to work with constant multiples (e.g. try replacing one of the factors to a constant). However, maybe omega could consider products of variables as atoms.

[James Gallicchio]

Yeah, all three MWEs I listed are linear if you choose the right expressions to fix as constants

[James Gallicchio]

:shrug: and maybe I'm expecting omega to do too much. I watched an isabelle user live-code last week and have been feeling greedy ever since.

[Damiano Testa]

I do not know if this is indeed in scope for omega, but I definitely feel that it should be in scope for something!

[James Gallicchio]

I think it would be good to compile lots of these nat-fighting examples to build up a little test suite for more automation. So if anyone has more examples please do share!!

[Damiano Testa]

Maybe you can find examples looking for uses of docs#Nat.add_sub_assoc. Whenever I had to use that lemma I wished for more automation.

[Peter Nelson]

This is probably (definitely) scope creep, but I think it would also be nice to have the potential automation being discussed also work for ENat, which is still pretty rough around the edges in its API.

[Kim Morrison]

The examples above definitely represent a bug in omega (presumably in the preprocessor rather than the actual elimination algorithm) that I will try to fix asap!

We have to do some processing of terms with multiplications, just to identify scalar multiplications, but omega should certainly understand that i * j is nonnegative!

[Kim Morrison]

Well, I'm not sure it is a bug after all, but I've slightly tweaked the handling of products so these examples work: lean#4695.

Note that there is a lot that omega could be doing with atoms-that-are-products that it does not do. For example

example (i j : Nat) : i * j = j * i := by omega -- fails

is out of scope for omega.

[Kevin Buzzard]

Somehow this doesn't surprise me. My mental model is addition, subtraction and multiplication by numerical constants. Isn't that what the spec is?

[Kim Morrison]

Yes. The change I've made is that when it tries pushing the Nat->Int coercion over multiplication, it now checks if the result is an atom, and if it is, it cancels the push.

This means that i * i stays as an atom (which is then manifestly non-negative) rather than being converted into (i : Int) * (i : Int) (which is not).