Can some tactic take care of this easy algebra?

Stream: new members

[Adam Dingle]

In a proof I've gotten to a point that looks like this (where a, b : Nat):

ih1: b * ((a - b) / b) + (a - b) % b = a - b
⊢ b * ((a - b) / b + 1) + (a - b) % b = a

Now, this looks super easy: all I have to do is add b to both sides of ih1, then factor it into the expression on the left. I could look up the names of several lemmas to perform rewrite steps that will get me there. But that seems like a bother. Is there some tactic that can just finish off the job for me?

[Yagub Aliyev]

I am new here. I could complete the proof with an extra assumption b ≤ a. Also not sure what to import first.

import Mathlib.Tactic

theorem addb' (a b: Nat) (ih1: b * ((a - b) / b) + (a - b) / b = a - b) (ineq': b ≤ a) : b * ((a - b) / b + 1) + (a - b) / b = a := by

let c := b * ((a - b) / b) + (a - b) / b
ring_nf
have h : c =b * ((a - b) / b) + (a - b) / b
tauto
rw[← h] at ih1
rw[Nat.add_assoc]
rw[← h]
have ih : a-b=c
tauto
apply Nat.eq_add_of_sub_eq at ih
rw[Nat.add_comm]
tauto
exact ineq'

[Timo Carlin-Burns]

@Yagub Aliyev you're right that the proof needs b ≤ a, but it looks like you proved a slightly different goal which replaces (a - b) % b with (a - b) / b.

[Timo Carlin-Burns]

Here is a proof of the original goal assuming b ≤ a. In fact, ih1 is not needed.

import Mathlib.Tactic

@[simp]
theorem Int.sub_emod_self {a b : ℤ} : (a - b) % b = a % b := by
  simp [Int.sub_emod]

theorem Int.sub_ediv_self (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (a - b) / b = a / b - 1 := by
  simp [Int.sub_ediv_of_dvd a (Int.dvd_refl b), hb]

example (a b : Nat) (hba : b ≤ a) :
    b * ((a - b) / b + 1) + (a - b) % b = a := by
  zify [hba]
  by_cases hb : (b : ℤ) = 0
  . simp [hb]
  simp [Int.sub_ediv_self _ hb, Int.ediv_add_emod]

[Kevin Buzzard]

Note that slim_check finds counterexamples to the original claim (e.g. a = 0, b = 1).

[Timo Carlin-Burns]

To answer your question about tactics for easy algebra, ring, linarith, and polyrith often help, but they don't work well with natural subtraction or integer division, since those are not very algebraically well-behaved operations. If you have evidence that those operations are well-behaved in your instance (for natural subtraction b ≤ a and for integer division b ∣ a), then you can use zify or qify to convert the goal into one about integer subtraction or rational division instead. And lastly there's omega, which is like linarith for natural numbers. It doesn't solve this goal because it doesn't understand %.

[Yagub Aliyev]

Timo Carlin-Burns said:

Yagub Aliyev you're right that the proof needs b ≤ a, but it looks like you proved a slightly different goal which replaces (a - b) % b with (a - b) / b.

Yes, Thank you. I misread the question.

[Adam Dingle]

Thanks to everyone for the super helpful responses.

You're all right that b ≤ a is necessary to prove my claim. I didn't mention it because I failed to take into account that subtraction is not well-behaved over Nat, i.e. it's not always true that a - b + b = a. For that reason the condition b ≤ a is necessary.

The situation I originally described arose when I was trying to prove "b * (a / b) + a % b = a" as an exercise. (I know that it's a library theorem anyway.) I used induction over a. In the inductive case it's indeed true that b ≤ a, so that condition is available.

Thanks for mentioning slim_check, qify, polyrith and omega. I wasn't aware of any of them since I think they're not mentioned in the Lean tutorials such as "Theorem Proving in Lean" and "Mathematics in Lean". I'll add them to my tactic vocabulary. For working with ℕ or ℤ, omega seems very powerful and useful.

Given h1 : b ≤ a, I've now realized that it's easy to get from ih1 to my goal:

 zify [h1] at ih1
 zify [h1]
 linarith

[Timo Carlin-Burns]

Nice! Here's a way to save one more line (⊢ means the goal)

 zify [h1] at ih1 ⊢
 linarith

[Adam Dingle]

Aha - I wasn't aware of that syntax. Great, thanks!