a*a = b*c -> gcd a b > 1

Stream: maths

[Rick Love]

Good point, my final conclusion should be gcd a b > 1 (Corrected the title)

[Rick Love]

That also assumes a,b,c > 1

[Rick Love]

Ok, here is a better approach:

-- 4 * 4 = 2 * 8  -> gcd a b = 2 gcd a c = 4
-- 6 * 6 = 4 * 9  -> gcd a b = 2 gcd a c = 3
theorem multiple_factors_then_gcd (a b c k : nat):
    a > 1 -> b > 1 -> c > 1 ->
    a*a = b*c ->
    gcd a b > 1 :=
begin
    intros ha hb hc h,

    let faa := factors (a*a),
    let fbc := factors (b*c),
    let fa := factors (a),
    let fb := factors (b),
    let fc := factors (c),
    have h_faa_fbc : faa = fbc := by { dsimp [faa, fbc], rw h,},
    have h_faa_fa_fa : faa = list.append fa fa := by {
        -- cc,
        -- Is there an operation for factors(a*a) = factors(a) ∧ factors(a)
        sorry,
    },

    -- have
    sorry,

end

[Kevin Buzzard]

If all you want to do is prove the gcd is bigger than one then you can just prove that if b>1 then it has a prime factor and this prime factor divides a^2 and hence a

[Kevin Buzzard]

I should think these facts are already in mathlib

[Rick Love]

Right, I was trying to use dvd and gcd, but I'll take a look at the prime functions. That's probably the missing piece 'prime factor divides a^2 and hence a'

[Kenny Lau]

if gcd a b <= 1 then gcd a b = 0 or gcd a b = 1.

In the first case, we have a = 0 or b = 0, contradiction.

In the second case, we have gcd (a * a) b = 1, so gcd (b * c) b = 1, so b = 1, contradiction.

[Kenny Lau]

no primes required

[Rick Love]

@Kenny Lau even with that, the difficulty is programming it in lean. How would you write that? Specifically how would you set up a proof by contradiction like this. (Note, I've done plenty of rw apply, etc, but still new to using exfalso and a contradiction).

[Kenny Lau]

you can start with:

  generalize hg : gcd a b = g,
  by_contra h,
  cases g with g,

(not tested)

[Rick Love]

Well that's giving me:
image.png

How do I pull the h out to work with it?

[Johan Commelin]

What do you mean with "pull out"? Does push_neg help?

[Kenny Lau]

what's your goal state before my invocations?

[Rick Love]

Johan Commelin said:

What do you mean with "pull out"? Does push_neg help?

Yeah, that helps. I'd just been using simp, but this gives better control.