Zulip Chat Archive

Stream: new members

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


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

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

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

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 23:42):

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

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

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 23:50):

h : false will fix this one

view this post on Zulip Adam Topaz (Jan 10 2021 at 23:50):

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

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

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

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 23:54):

lol https://oeis.org/A158611

view this post on Zulip Adam Topaz (Jan 10 2021 at 23:54):

Oooh searching oeis is a very interesting idea!

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 23:55):

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

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

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

view this post on Zulip Adam Topaz (Jan 11 2021 at 00:06):

There's the #find command

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

view this post on Zulip Lars Ericson (Jan 11 2021 at 00:10):

Thank you @Bryan Gin-ge Chen for slim_check.

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 00:11):

or x=4, a=b=2.


Last updated: May 15 2021 at 23:13 UTC