Zulip Chat Archive

Stream: new members

Topic: if `x|a*b` then `x|a` or `x|b`

Lars Ericson (Jan 10 2021 at 23:32):

I'm looking for a lifeline here:

import data.nat.basic
import tactic

lemma expand_dvd (a b:  ) : a  b    c, b = a * c :=
  exact iff.rfl,

lemma dvd_mul_a_b_then_a_or_b {a b x : } (h: (x  (a*b))) : x  a  x  b :=
  have h1 := exists_eq_mul_right_of_dvd h,
  by_cases ha : x  a,
  refine or.inr _,
  cases h1 with c hc,
  have h2 := (expand_dvd x b).2,
  apply h2,

The tactic state is

1 goal
h: x  a * b
ha: ¬x  a
hc: a * b = x * c
h2: ( (c : ), b = x * c)  x  b
  (c : ), b = x * c

It seems like an obvious fact but I'm blanking out and I don't see it already in docs#dvd

Kevin Buzzard (Jan 10 2021 at 23:34):

Do you know the maths proof? I'm particularly interested in your answer this time, because in this case you're wasting your time -- what you're trying to prove here is false. You have to know the maths proof.

Bryan Gin-ge Chen (Jan 10 2021 at 23:41):

slim_check can find lots of counterexamples:

import tactic.slim_check

lemma dvd_mul_a_b_then_a_or_b {a b x : } (h: (x  (a*b))) : x  a  x  b :=
by slim_check
Found problems!

a := 1198
b := 18
x := 4
(0 shrinks)

a b x : ℕ,
h : x ∣ a * b
⊢ x ∣ a ∨ x ∣ b

Kevin Buzzard (Jan 10 2021 at 23:42):

Oh nice! It's about time I stopped forgetting that slim_check exists.

Adam Topaz (Jan 10 2021 at 23:49):

I wonder... Can slim check work in "reverse" trying to find additional hypotheses that will "fix" a statement?

Kevin Buzzard (Jan 10 2021 at 23:50):

h : false will fix this one

Adam Topaz (Jan 10 2021 at 23:50):

Yeah, it needs to be a bit more clever than that :wink:

Kevin Buzzard (Jan 10 2021 at 23:51):

Lars -- if x is 0 or 1 or prime you're OK. But I'm not sure if a computer could spot that!

Kevin Buzzard (Jan 10 2021 at 23:53):

The smartest thing to do on this occasion would be to try values of x sequentially, figure out which ones seem to work, and then to query oeis.org to try and find out what's going on. But even here there's a subtlety -- you have to know that it's a condition on x which gives you the interesting theorem, as opposed to a condition on a or b.

Kevin Buzzard (Jan 10 2021 at 23:54):

lol https://oeis.org/A158611

Adam Topaz (Jan 10 2021 at 23:54):

Oooh searching oeis is a very interesting idea!

Kevin Buzzard (Jan 10 2021 at 23:55):

In the old days you had to search Don Zagier, which was much more inconvenient.

Kevin Buzzard (Jan 10 2021 at 23:57):

I remember when people started uploading pari code to OEIS which produced the sequences -- I thought it was a neat idea. Now I'm thinking that if enough people started uploading Lean code to produce the functions, you really could get something neat :-) Can we port the pari code to Lean?

Julian Berman (Jan 11 2021 at 00:05):

is there a tactic that knows how to instead look at the type of the goal and suggest hypotheses based on things in mathlib already with that goal type?

Adam Topaz (Jan 11 2021 at 00:06):

There's the #find command

Lars Ericson (Jan 11 2021 at 00:10):

@Kevin Buzzard you're right, I didn't consider the possibility that x could be a product of a factor in a and a factor in b.

I was actually trying to prove this lemma which is also false by slim_check:

import data.nat.basic
import tactic.slim_check

lemma neg_dvd_mul {a b x : } (ha: ¬(x  a)) (hb: ¬(x  b)) : ¬ (x  (a*b)) :=
by slim_check

The counterexample is

a := 34
b := 6
x := 12

Lars Ericson (Jan 11 2021 at 00:10):

Thank you @Bryan Gin-ge Chen for slim_check.

Kevin Buzzard (Jan 11 2021 at 00:11):

or x=4, a=b=2.

Last updated: Dec 20 2023 at 11:08 UTC