Stream: new members

Topic: The stupid way to prove the divisibility of sums

agro1986 (Nov 06 2019 at 13:53):

Hi all. So, I proved that if d|a, d|b, then for any integers m, n, I have d | (ma + nb)

import tactic.ring
variables {a b c d: ℤ}
def divides (a b: ℤ): Prop := ∃(d: ℤ), b = a * d

theorem divides_linear_sum (hda: divides d a) (hdb: divides d b):
∀ (m n: ℤ), divides d (m * a + n * b) :=
begin
assume m, assume n,
cases hda with q hq,
cases hdb with r hr,
use m * q + n * r,
rw [hq, hr],
ring,
end


Now "obviously" this holds for the special case m = n = 1. However I couldn't write the proof in a concise way.

theorem divides_sum (hda: divides d a) (hdb: divides d b):
divides d (a + b) :=
have h : divides d (1 * a + 1 * b), from divides_linear_sum hda hdb 1 1,
have simplify: 1 * a + 1 * b = a + b, from
begin
ring,
end,
simplify ▸ h


I thought I could proof it in 1 step using divides_linear_sum hda hdb 1 1. The problem was, when I gave divides_linear_sum hda hdb 1 1 I got divides d (1 * a + 1 * b) which isn't the same as divides d (a + b) syntactically. Any pointers (like how to write it concisely in tactics mode)? Thanks!

Kenny Lau (Nov 06 2019 at 13:57):

theorem divides_sum (hda: divides d a) (hdb: divides d b):
divides d (a + b) :=
by convert divides_linear_sum hda hdb 1 1; rw one_mul


Kenny Lau (Nov 06 2019 at 13:58):

theorem divides_sum (hda: divides d a) (hdb: divides d b):
divides d (a + b) :=
by simpa only [one_mul] using divides_linear_sum hda hdb 1 1


agro1986 (Nov 06 2019 at 14:03):

wow thanks! everyone's a wizard here :)

Kevin Buzzard (Nov 06 2019 at 20:03):

It's just practice. After a while your head ends up full of tricks

Johan Commelin (Nov 07 2019 at 07:03):

@agro1986 Btw, did you know that you can replicate the notation $a | b$ in Lean?

Last updated: May 14 2021 at 12:18 UTC