Is there a linarith type tool for Nat subtraction and order

Stream: Is there code for X?

[Terence Tao]

Hi again. I'm finding it really fiddly to work with the natural number subtraction operation; in principle there are enough tools in Std.Data.Nat.Lemmas to manipulate things, but it's hard to dig out exactly the right tool for the purpose and it would be great if there was a linarith type tool that did everything. Here is a typical example:

import Mathlib

example (a b c: ℕ) (ha: a ≤ c) (hb: b ≤ c) (h:c-a=c-b) : a = b := by
  have h' : c-(c-a) = c-(c-b) := by rw [h]
  rw [Nat.sub_sub_self ha, Nat.sub_sub_self hb] at h'
  exact h'

I understand why ring doesn't work here (Natural numbers aren't a ring), and I guess linarith can't handle the branching inherent in the Nat subtraction operation, but perhaps some more advanced tool is available?

The other alternative is to try to cast things to a larger group, such as the integers, where either linarith or ring would become useful. Is there a tool to give something like ((n-m):\Z) = if m \leq n then (n:\Z)-(m:\Z) else (0:\Z)? By the way I struggle to get the casting operators to work exactly the way I want them to here: lean seems to consistently interpret ((n-m):\Z) as (n:\Z)-(m:\Z) rather than the desired ((n:\N)-(m:\N)):\Z) unless I introduce a new variable such as let k:\N := n-m. It's to the point where I really struggle to write any expression with manual casts (which by the way also was one reason why I wanted to have tools to extract out complicated expressions directly, because typing out manually often gets the casting wrong even if I cut-and-paste directly from the tactic goal infoview).

[Scott Morrison]

There is such a tool, called omega, which will decide all such problems. There was a partial implementation in Lean 3, currently none in Lean 4, but we are hoping to have it done by the end of the year.

[Mario Carneiro]

The way to force lean to interpret the subtraction as a Nat.sub is (n - m : \N)

[Mario Carneiro]

elaboration proceeds from the outside in, and coercions are done only at the last possible moment, meaning they end up on the leaves of the expression by default

[Mario Carneiro]

People will definitely tell you to just avoid Nat.sub entirely though

[Terence Tao]

Yeah Scott already warned me :). But I need to do things like perform a reflection $k \mapsto n-k$ on a set of natural number exponents $\{0,\dots,n\}$ for a polynomial, so it's really inconvenient to leave the natural numbers for say the integers just to gain access to a better subtraction operation because that breaks the fact that monomial exponents of a polynomial are naturally in \N rather than \Z.

[Adam Topaz]

We also have the zify tactic which might be useful?

[Adam Topaz]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Zify.html

[Adam Topaz]

However this doesn’t do anything nearly as powerful as linarith.

[Mario Carneiro]

I think you might be able to do it by linarith (a bit wastefully) if you tell lean that c - a + a = c and similarly for all other subtractions in the problem

[Terence Tao]

It helps a little bit but not much.

In any case I was at least able to get the lemma relating natural number subtraction with integer subtraction, which may suffice for at least some of my applications. The proof is surprisingly fiddly though (but perhaps there is a slicker way).

example (n m : ℕ) : (n-m:ℕ) = if m ≤ n then (n:ℤ)-(m:ℤ) else (0:ℤ) := by
  split
  . have h : m ≤ n := by assumption
    symm; rw [sub_eq_iff_eq_add]
    suffices : n = (n-m) + m
    . nth_rewrite 1 [this]
      simp
    rw [Nat.sub_add_cancel h]
    rfl

  suffices : (n - m) = 0
  . zify at this; assumption
  rw [Nat.sub_eq_zero_iff_le]
  linarith

[Terence Tao]

Mario Carneiro said:

I think you might be able to do it by linarith (a bit wastefully) if you tell lean that c - a + a = c and similarly for all other subtractions in the problem

OK, that works, and is another workaround, thanks.

example (a b c: ℕ) (ha: a ≤ c) (hb: b ≤ c) (h:c-a=c-b) : a = b := by
  have ha' : (c-a) + a = c := Nat.sub_add_cancel ha
  have hb' : (c-b) + b = c := Nat.sub_add_cancel hb
  linarith

[Mario Carneiro]

which you could golf to linarith [Nat.sub_add_cancel ha, Nat.sub_add_cancel hb]

[Terence Tao]

That's probably the simplest solution in most cases, since pretty much the only use case for natural number subtraction is in the regime where Nat.sub_add_cancel applies, the other values of subtraction being an artificial placeholder.

[Mario Carneiro]

your theorem should also be a trivial variation on one which is in the library (and if not that should be fixed)

[Heather Macbeth]

Or

example (a b c: ℕ) (ha: a ≤ c) (hb: b ≤ c) (h:c-a=c-b) : a = b := by
  zify [ha, hb] at h
  linarith

[Mario Carneiro]

example (n m : ℕ) : (n-m:ℕ) = if m ≤ n then (n:ℤ)-(m:ℤ) else (0:ℤ) := by
  split
  . next h => exact Int.ofNat_sub h
  . next h => rw [Nat.sub_eq_zero_of_le (Nat.le_of_not_le h)]; rfl

[Mario Carneiro]

and these are simp lemmas so golfed:

example (n m : ℕ) : (n-m:ℕ) = if m ≤ n then (n:ℤ)-(m:ℤ) else (0:ℤ) := by
  split <;> simp [Nat.le_of_not_le, *]

[Jireh Loreaux]

Note: we also have some lemmas specialized to reflection, like docs#Finset.sum_range_reflect in case this is the kind of thing you need.

[Heather Macbeth]

Terence Tao said:

I need to do things like perform a reflection $k \mapsto n-k$ on a set of natural number exponents $\{0,\dots,n\}$ for a polynomial, so it's really inconvenient to leave the natural numbers for say the integers just to gain access to a better subtraction operation because that breaks the fact that monomial exponents of a polynomial are naturally in \N rather than \Z.

Another approach here could be to work with (e.g. sum over) the antidiagonal docs#Finset.Nat.antidiagonal, which effectively gives access to both k and n - k as an ordered pair as well as the standard lemmas about them.

[Terence Tao]

Yeah, Scott suggested that to me last week. I started experimenting with that but ran into some syntactical issues trying to understand summing over sets of pairs and so figured it would be easier to work in the more conventional setting of indexing by natural numbers and using subtraction as necessary, figuring that it would be easier to prove lemmas about subtraction than to prove lemmas about the antidiagonal. I can see that the latter is a more conceptually elegant way to proceed, though it does require translating large parts of my intended proof from its conventional setting to this new framework that would be less familiar to most readers. So we encounter this tradeoff again...

[Terence Tao]

Basically the ideal situation should be that there is a workable subset of Lean that is mutually intelligible with a workable subset of Mathematical English, with only moderate amounts of effort required on both sides to work in that subset. So, on the Lean side for instance, there should be tools that let one talk about objects the "wrong" way, e.g., unnecessarily indexing things by natural numbers, in order to enter the mutually intelligible subset, with only a minor cost in time and elegance. On the Math side, one may have to replace some of the more handwavy approaches to proofs with a more formal and pedantic version, but again this should ideally only require a modest cost in length of explanation (in particular, the Mathematical English proof should still spend most of the time on the underlying mathematical ideas and only a minimum on formal technicalities).

[Terence Tao]

(This is a bit off-topic, by the way, but this (20 min) video is an excellent demonstration of the concept of "mutual intelligibility of workable subset": https://www.youtube.com/watch?v=ryVG5LHRMJ4&ab_channel=KingMingLam )

[Heather Macbeth]

To go from idiomatic prose to idiomatic Lean you often need to abstract, i.e. strategically forget some information about the objects you have around.

• This was the case with the indexing of natural numbers yesterday (abstract by replacing Fin n with an arbitrary fintype and a hypothesis about its size being n)
• this is arguably the case with Nat-subtraction (abstract by replacing n - m with "a natural c satisfying (m ≤ n ∧ n = m + c) ∨ (n < m ∧ c = 0) ")
• this was perhaps the case with a question yesterday (one should replace "a set in the type α" with "a map into α")
• when people write traditional elementary real analysis and need it to be re-wired into filter language, often morally the change to the arguments consists of replacing max a b with "a real number c satisfying a ≤ c and b ≤ c"

[Heather Macbeth]

Terence Tao said:

So, on the Lean side for instance, there should be tools that let one talk about objects the "wrong" way, e.g., unnecessarily indexing things by natural numbers, in order to enter the mutually intelligible subset, with only a minor cost in time and elegance.

Speculatively: there could be automation which knows all these "standard abstraction rules" ...

[Terence Tao]

Mario Carneiro said:

I think you might be able to do it by linarith (a bit wastefully) if you tell lean that c - a + a = c and similarly for all other subtractions in the problem

This is a rather belated response, but perhaps one should simply improve linarith in the context of natural number arithmetic by having it automatically search for hypotheses of the form a \leq c and converting them to c - a + a = c before running the rest of the linarith algorithm? Similar to how field_simp searches for non-vanishing hypotheses before performing its simplifications.

[Mario Carneiro]

I think this preprocessor actually existed in lean 3, it may not have been ported yet

[Mario Carneiro]

...maybe not, but it's definitely a good idea in any case. @Rob Lewis Do you recall if we ever added something like this to linarith?

[Mario Carneiro]

(BTW I would slightly amend the algorithm to look for Nat.sub applications in the hypotheses and introduce the corresponding c - a + a = c lemma when it can find a proof of a <= c, rather than converting every nat inequality into a nat.sub equation. The reason is because it is very common for linarith to see a nat inequality, and much less common for linarith to see a Nat.sub application, and the new assumption is only helpful if that particular Nat.sub application already appears in the goal or hypotheses.)

[Bolton Bailey]

Potentially relevant: This idea I proposed a few weeks ago to improve/supercharge zify with linarith to automatically do the casework on natural subtraction. I'm pretty sure this would accomplish the things this augmented linarith would accomplish while also being useful in cases where linarith on it's own wouldn't solve the goal.

[Rob Lewis]

Mario Carneiro said:

...maybe not, but it's definitely a good idea in any case. Rob Lewis Do you recall if we ever added something like this to linarith?

I don't think this particular optimization was there. It's not totally clear to me how it interacts with the zify preprocessing, which will also use inequalities in the context to try to push nat->int casts through subtraction.

[Rob Lewis]

As Bolton says, zify could work harder here too. But I do think there's benefit to zify staying simple and predictable, and calling linarith itself as a discharger may not be that...

[Rob Lewis]

Making linarith better on Nat is a losing battle from the start. It feels wrong to complicate other things to eke out a few more examples, when the proper solution is an entirely different tactic :upside_down:

[Damiano Testa]

In Lean3 I had a remove_subs tactic that would find Nat.subs, do cases on them depending on whether the "obvious" inequality was satisfied and tried to solve the branch where the difference was zero by some simple discharge.

Ideally, after running that, you were left with only the "non-junk" subtractions and all the hypotheses in place.

If you think that this might be a good "preprocessing", before zify/linarith can try to take over, I can be easily convinced to port the tactic!

[Ruben Van de Velde]

zify!

[Terence Tao]

After playing with a few more natural number subtraction problems, I think one reasonably simple solution would be to introduce a zify! tactic which behaves like zify except that any hypothesis a \leq b that is needed to push-cast b-a is automatically added to the list of goals if it is not already provided (or if it is not listed in the hypotheses). Any outstanding such goals would typically then be solved by linarith (though if there were nested subtractions then another round of zify! may be needed). Most of the use cases I can think of (in which the a \leq b type hypotheses are always satisfied) could then be handled by some finite number of applications of zify! and linarith, without needing to have zify! actually call linarith in any way. (One could then also design a zify!! tactic that calls linarith to attempt to verify any missing order hypotheses once they have been completely push-casted to the integers by a recursive appeal to zify!!.)

Here is an example of how such a strategy would work. The proposed tactic zify! would simply apply zify and rw [Int.coe_nat_sub] repeatedly until neither of them have any further effect. Similarly, zify!! would apply zify! and linarith repeatedly until neither had any further effect.

import Mathlib

example (n m : ℕ) (h: m+2 ≤ n) : n - (1+m+1) = n - m - 2 := by
  zify
  rw [Int.coe_nat_sub, Int.coe_nat_sub, Int.coe_nat_sub]
  . zify
    linarith
  . linarith
  . zify
    rw [Int.coe_nat_sub]
    . linarith
    linarith
  linarith

[Scott Morrison]

Depending on your timeline, I wouldn't put too too much effort into tactics like this. The new omega will take care of things like this out of the box. I'm hoping it will be ready by the end of the year, and an incomplete version (i.e. still gives proofs, but doesn't solve all problems in its spec) hopefully sooner.