Zulip Chat Archive

Stream: maths

Topic: By schoolkid


view this post on Zulip Chris Hughes (Nov 13 2019 at 00:57):

A 12 year old just got a prize for proving this.

example :  n : , 7  n  7  (n / 10 + 5 * (n % 10))

This can be turned into a Presburger formula right? Should omega be able to do it?

I tried turning it into a Presburger formula, but it didn't seem to work.

import tactic.omega
open nat
example (n : ) : 7  n  7  (n / 10 + 5 * (n % 10)) :=
begin
  rw [dvd_iff_mod_eq_zero, dvd_iff_mod_eq_zero],
  have := nat.mod_lt n (show 0 < 7, by norm_num),
  have := nat.mod_add_div n 7,
  have := nat.mod_lt n (show 0 < 10, by norm_num),
  have := nat.mod_add_div n 10,
  have := nat.mod_lt (n / 10 + 5 * (n % 10)) (show 7 > 0, by norm_num),
  have := nat.mod_add_div (n / 10 + 5 * (n % 10)) 7,
  repeat { revert this },
  generalize : n % 7 = a,
  generalize : n / 7 = b,
  generalize : n / 10 = c,
  generalize : n % 10 = d,
  generalize : (c + 5 * d) % 7 = e,
  generalize : (c + 5 * d) / 7 = f,
  omega -- doesn't work
end

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 07:33):

I would not be surprised if you could find some previous reference to this test in some popular maths book from the 50s, it's very dangerous calling it a new formula. But good on him. It's 7|10x+y iff 7|x+5y. If you apply the test to 14 you get 21.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 19:34):

It's m | a x + b y iff m | (an-br) x + bn y for hcf(m, n) = 1 (or something like that). I think this stuff is taught in high school.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 19:34):

What's omega?

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:34):

A tactic that proves statements in the language of the ordered group of integers

view this post on Zulip Johan Commelin (Nov 14 2019 at 19:35):

So you are allowed to add and compare integers using ≤ but you can only multiply with constants


Last updated: May 14 2021 at 20:13 UTC