Is there a mathlib tactic for closing arithmetic goals?

Stream: new members

[Alexander Lucas]

I have lots of goals like the following forall (i j k : Nat), i * j = i * (j - k) + k * i. I thought maybe norm_num would do it, but it seems to have no effect.

import Mathlib.Tactic.NormNum
theorem H {i j k : Nat} : i * j = i * (j - k) + k * i := by
  norm_num

The goal is the same after norm_num as it is before.
The ring tactic does change the goal a bit, but not in any especially helpful way as far as I can tell.

Hopefully I'm not missing something obvious. Thank you.

[Alexander Lucas]

I guess that example actually isn't true, since k > j means j - k < 0, which can't happen in Nats.

[Moritz Doll]

Alexander Lucas said:

I guess that example actually isn't true, since k > j means j - k < 0, which can't happen in Nats.

Subtraction a - b on natural numbers is defined as zero if b > a, so your claim is false. You want to use integers and then ring should prove your claim

[Alexander Lucas]

Thank you, yeah. Is it possible to do induction on integers though? Pick a base case n and induct for m > n?
Also, incidentally, what _is_ norm_num for? If you don't mind.

[Moritz Doll]

norm_num is for calculations with explicit numbers:

example : 4 + 1= 1 + 2*2 := by
  norm_num

[Alexander Lucas]

I see. Thanks.

[Moritz Doll]

(by calculation I mean normalizing)

[Moritz Doll]

The induction tactic works with integers, but then you have to prove your statement for the natural numbers and then for n-1 assuming n. In the natural number case you can do induction again and together with some artifical inserting of zeros you can shift the base case to any integer n.

[Moritz Doll]

But I have no idea whether there is something out of the box for that

[Moritz Doll]

without the shifting there is docs#Int.induction_on

[Alexander Lucas]

I appreciate it mate. I'll try to make that work.

[Alexander Lucas]

By looking in the file you pointed me to, I found the tactic Int.le_induction, which seems to do what I need. Here's an example using it.

def postage_ℤ : (n : ℤ) → (h : 4 ≤ n) → ∃ j k, n = 2 * j + 5 * k := by
  intro n H
  apply @Int.le_induction (fun x => (h : 4 ≤ x) → ∃ j k, x = 2 * j + 5 * k) 4
  . intro _
    exists 2, 0
  . intro z h₁ h₂
    match h₂ h₁ with
    | ⟨j', k', h₂⟩ =>
      apply @Classical.byCases (k' = 0) <;> intro h₃ _
      . exists (j' - 2), 1
        rw [h₂, h₃]
        ring
      . exists (j' + 3), (k' - 1)
        rw [h₂]
        ring
  all_goals exact H

[Maarten Derickx]

The ring tactic works better in the integers then over the natural numbers when substraction is involved. Since in general (j - k) is not a natural number. Try the following:

import Mathlib

#eval 6 - 9
#eval (6: ℤ) - 9

theorem H {i j k : ℤ} : i * j = i * (j - k) + k * i := by
  ring

[Alexander Lucas]

Thanks. I ended up coming to the same conclusion. I do have another related question. Say I have some arithmetic expression of naturals with a subexpression (j - k). Say I also have some H : k <= j. Since, under this assumption H, j - k is generally a natural number, is there a way to convey that fact to ring, directly or indirectly, such that the goal can still be closed without a bunch of manual rewriting?

[Alex J. Best]

tactic#zify

[Alexander Lucas]

Well damn, that was quick. Thanks!

[Alex J. Best]

This isn't exactly what you asked for, but zify [H], ring is what I would do in that situation :smile: