Idiom

Stream: new members

[Richard Copley]

Is there a more idiomatic way to do rewrite [(by ring : (a + b) * (a + b) = a * a + b * b + 2 * (a * b))] in Lean 4?

The context is below (line 22). This is just a trivial learning example that I set for myself, from a question which came up on Libera IRC ##math. I'd appreciate any other hints on how a more experienced user of Lean 4 would write this proof.

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Tactic.Ring

theorem toy (a b : ℕ) : a * b ∣ (a + b)^2 → a = b := by
  have C : ∀ {a b : ℕ}, a * b ∣ a * a + b * b → a ∣ b * b := by
    intro a b h
    rewrite [Nat.dvd_add_iff_right (Nat.dvd_mul_right a a)]
    exact Nat.dvd_trans (Nat.dvd_mul_right a b) h
  rewrite [Nat.pow_two]
  if hz : a = 0 then
    rewrite [hz, Nat.zero_add, Nat.zero_mul, ← Nat.mul_self_inj, Nat.zero_mul]
    exact symm ∘ Nat.eq_zero_of_zero_dvd
  else
    let d := Nat.gcd a b
    have dpos : 0 < d := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero hz)
    have ⟨⟨a', (h₁ : a = d * a')⟩, ⟨b', (h₂ : b = d * b')⟩⟩ := Nat.gcd_dvd a b
    have hcoprime : Nat.coprime a' b' := by
      rewrite [← (Nat.div_eq_iff_eq_mul_right dpos ⟨a', h₁⟩).mpr h₁]
      rewrite [← (Nat.div_eq_iff_eq_mul_right dpos ⟨b', h₂⟩).mpr h₂]
      exact Nat.coprime_div_gcd_div_gcd dpos
    rewrite [(by ring : (a + b) * (a + b) = a * a + b * b + 2 * (a * b))]
    rewrite [← Nat.dvd_add_iff_left (Nat.dvd_mul_left _ _)]
    rewrite [h₁, h₂]
    repeat rewrite [(by intro x y ; ring :
      ∀ (x y : ℕ), d * x * (d * y) = d * d * (x * y))]
    rewrite [← Nat.mul_add, Nat.mul_dvd_mul_iff_left (Nat.mul_pos dpos dpos)]
    intro h
    apply congr_arg (fun x => d * x)
    apply Nat.dvd_antisymm
    . rewrite [← Nat.coprime.dvd_mul_right hcoprime]
      exact C h
    . rewrite [← Nat.coprime.dvd_mul_right hcoprime.symm]
      exact C ((Nat.add_comm ..) ▸ (Nat.mul_comm ..) ▸ h)

[Alex J. Best]

At the moment, not really, some people like using the similar rw [show (a + b) * (a + b) = a * a + b * b + 2 * (a * b) by ring] more but that is basically the same. Seeing as you are rewriting a subterm you can't use convert_to which would be a more idiomatic way if you wanted to change the whole goal.

[Richard Copley]

Thank you. That is nice to know.

[Ruben Van de Velde]

How about rw [add_mul_self_eq]

[Richard Copley]

Ruben Van de Velde said:

How about rw [add_mul_self_eq]

Thanks! Followed by rewrite [(by ring : a * a + 2 * a * b + b * b = a * a + b * b + 2 * (a * b)]? Or rewrite [add_rotate, mul_assoc, add_assoc]?

[Eric Wieser]

add_right_comm should be enough

[Richard Copley]

Great! But not quite. Still need the mul_assoc.
Do you think that's better?

[Yury G. Kudryashov]

Another option is to use calc with ring.