Zulip Chat Archive

Stream: new members

Topic: The stupid way to prove the divisibility of sums


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip agro1986 (Nov 06 2019 at 14:03):

wow thanks! everyone's a wizard here :)

view this post on Zulip Kevin Buzzard (Nov 06 2019 at 20:03):

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

view this post on Zulip Johan Commelin (Nov 07 2019 at 07:03):

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


Last updated: May 14 2021 at 12:18 UTC