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

Stream: new members

[Lars Ericson]

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]

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]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

h : false will fix this one

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

lol https://oeis.org/A158611

[Adam Topaz]

Oooh searching oeis is a very interesting idea!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

There's the #find command

[Lars Ericson]

@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]

Thank you @Bryan Gin-ge Chen for slim_check.

[Kevin Buzzard]

or x=4, a=b=2.