Tactics for Nat arithmetic

Stream: lean4

[Jeremy Salwen]

Are there tactics I can use to handle basic Nat arithmetic? Here is an example that I was trying to solve with simp,ring, nlarith, to no avail. I couldn't even get the fnterm to cancel out without manually reassociating terms, etc.

MWE:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring


def fn (l: List ℕ) (n:ℕ): ℕ := sorry

theorem demo (x y: ℤ ) (Q:x = y+1): fn tail 0 + (accum * 10 + Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail =
  fn tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
    accum * 10 ^ Nat.succ (List.length tail) := by
    ring

[Dean Young]

(deleted)

[Kevin Buzzard]

It's not clear to me that your goal is true. It seems to me that it would follow if you knew that (x + y) - z = x + (y - z) in the particular case x = accum * 10, y = Char.toNat head and z = Char.toNat (Char.ofNat 48), and this is not true for naturals in general because of stupid natural subtraction. You would be OK if you know z <= y but it's not the job of tactics like ring to supply this proof obligation; this is one of the reasons you're having no luck. Modulo that issue, in Lean 3 you would probably be able to use the ring_exp tactic but I'm not sure that this has been ported yet. A good first move would be rw [Nat.succ_eq_add_one, pow_add, pow_one] (which now takes you into ring territory) but now automation is blocked on the missing proof that z <= y.

[Kevin Buzzard]

theorem demo (x y: ℤ ) (Q:x = y+1): fn tail 0 + (accum * 10 + Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail =
    fn tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
    accum * 10 ^ Nat.succ (List.length tail) := by
  rw [Nat.succ_eq_add_one, pow_add, pow_one]
  have h : Char.toNat (Char.ofNat 48) ≤ Char.toNat head := sorry -- is this true? If not your goal is probably false
  rw [Nat.add_sub_assoc h]
  ring

[Jeremy Salwen]

Ok interesting, it looks like the difficulty here was an unexpected difference in the association on either side of the equation. Once that is fixed, ring will almost solve it, it just needs Nat.succ_eq_add_one:

theorem demo (x y: ℤ ) (Q:x = y+1): fn tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
  fn tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
    accum * 10 ^ Nat.succ (List.length tail) := by
  rw [Nat.succ_eq_add_one]
  ring

A few follow-up questions:

1. Is Nat.succ bad for using these sorts of arithmetic tactics, so I should always manually eliminate it? (Maybe this could be done automatically?)
2. Outside of a proof assistant, the way I would approach this proof is to check if it is true in Z, and then check that each step of my proof also holds in N. Is there a tactic that would do something like this?
3. The reason why this stumped me so much was because the ring tactic wasn't making any progress despite the fact that it was very close to working. It would be more user friendly if there was a tactic that would distribute and eliminate matching terms even if it wasn't able to solve it, as this would highlight the problematic terms that remain.

[Alex J. Best]

For 2. there is a mathlib(4) tactic called zify that is used to do this sort of thing, automatically translating to a Z version of an N goal.
For 1. It's probably a good idea yes.
And for 3. That is indeed annoying, sometimes you can rewrite and equality to a subtraction equals zero and use ring_nf to normalize and see what's left

[Yaël Dillies]

@Damiano Testa, doesn't your tactic aim to do 3.?

[Kevin Buzzard]

Please no more lean 3 tactics! All they do is cause trouble for the port right now.

[Jeremy Salwen]

For

1. I had a look at the source code for the ring tactic, but I couldn't figure out a good place to add Nat.succ normalization.
2. zify seems to require the user to know ahead of time which inequalities are necessary to solve in Z. Is there a version that will generate additional goals instead?
3. I would be interested in knowing what Damiano's tactic is :)

I'd love to try to help improve things so they are more user friendly and discoverable. For someone who is more experienced it probably doesn't make much of a difference, but for a newbie like me it can save hours of being confused!

[Yaël Dillies]

Damiano's tactic is tactic#move_add

[Jeremy Salwen]

Here is another example of a Nat equality that was causing me problems. Ultimately I had to introduce three lemmas to make zify convert everything to Z, and ring still wouldn't solve it without apply Int.eq_of_sub_eq_zero first.

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring


def fn (b n:ℕ): List ℕ  := sorry

theorem demo (b n i:ℕ) (h: i< List.length (fn b n)):
  i = List.length (fn b n) - 1 - (List.length (fn b n) - 1 - i)  :=  by
  have h₂: List.length (fn b n) - 1 ≥ (List.length (fn b n) - 1 - i) := by simp
  have h₃: List.length (fn b n) ≥ 1 := by calc
    List.length (fn b n) > i := h
    _ ≥ 0 := by simp
  have h₄: i ≤ List.length (fn b n) - 1 := by apply Nat.le_pred_of_lt; exact h
  zify [h₂, h₃, h₄]
  apply Int.eq_of_sub_eq_zero
  ring

[Kevin Buzzard]

theorem demo (b n i:ℕ) (h: i< List.length (fn b n)) :
    i = List.length (fn b n) - 1 - (List.length (fn b n) - 1 - i)  :=
    Eq.symm (Nat.sub_sub_self (Nat.le_sub_of_add_le h))

We have enough library stuff to make a term mode proof pretty painless. The Eq.symm is because you shouldn't be stating theorems like that -- when you write A = B the convention is to have A the more complicated side; this is the convention which aligns with the way rw works for example. In general you would use a tactic like omega to do this but we don't have an omega in Lean 4 yet.