## 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 :=
begin
exact iff.rfl,
end

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


The tactic state is

1 goal
abx: ℕ
h: x ∣ a * b
ha: ¬x ∣ a
c: ℕ
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)
-------------------

state:
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.

#### 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: May 15 2021 at 23:13 UTC