my attempt proving gcd(a, b) = gcd(b, a)

Stream: new members

[agro1986]

Hi everyone. I tried defining gcd and then proving that gcd(a, b) implies gcd(b, a):

variables {a b c d: ℤ}

def divides (a b: ℤ): Prop := ∃(d: ℤ), b = a * d

def gcd (a b d: ℤ): Prop :=
  ¬(a = 0 ∧ b = 0) ∧
  divides d a ∧
  divides d b ∧
  ∀ (c: ℤ), divides c a ∧ divides c b → c ≤ d

theorem gcd_sym (h: gcd a b d): gcd b a d :=
  begin
    let hnonzero := h.left,        -- ¬(a = 0 ∧ b = 0)
    let hda := h.right.left,       -- divides d a ∧
    let hdb := h.right.right.left, -- divides d b ∧
    let hgreatest := h.right.right.right,
    apply and.intro,
      exact (assume hzero: b = 0 ∧ a = 0,
        hnonzero ⟨hzero.right, hzero.left⟩),
    apply and.intro,
      assumption,
    apply and.intro,
      assumption,
    assume c,
      let hc_lt_d := hgreatest c,
      assume hc_divides,
        exact hc_lt_d ⟨hc_divides.right, hc_divides.left⟩
  end

Would you define gcd differently? (e.g., something that means the same thing but is more canonical to write in Lean)

Also, the proof is a bit long for basically flipping some terms. Any way you would streamline it? Thanks a lot!

[Anne Baanen]

My instinct would be to define gcd : ℤ → ℤ → ℤ using Euclid's algorithm (and prove it is the unique number that satisfies the condition in your gcd proposition). The proof would then state gcd a b = gcd b a.

[Anne Baanen]

But I'm pretty much an intuitionist, so take that as you want :P

[Johan Commelin]

@agro1986 Could you explain a bit of your background/motivation/goal? Such a bigger picture could help us with answering more specific questions. Are these training exercises, or do you want to formalise a particular piece of maths, or do you have another goal?

[Kevin Buzzard]

Here's a more compressed tactic mode proof:

theorem gcd_sym (h: gcd a b d): gcd b a d :=
  begin
    rcases h with ⟨hne0, hda, hdb, hdmin⟩,
    split, exact mt and.comm.mp hne0,
    split, assumption,
    split, assumption,
    rintros c ⟨ha, hb⟩,
    exact hdmin c ⟨hb, ha⟩
  end

[Kevin Buzzard]

and here's a term mode proof:

theorem gcd_sym (h: gcd a b d): gcd b a d :=
⟨mt and.comm.mp h.1, h.2.2.1, h.2.1, λ c hc, h.2.2.2 _ ⟨hc.2, hc.1⟩⟩

[agro1986]

@Johan Commelin for now, training exercise to familiarize myself with the language :). I'm rereading an elementary number theory textbook while challenging myself to write the definitions and proofs using Lean

[agro1986]

@Tim Baanen hmm, that's an interesting way to think about it. Write the algorithm for it, and then using Lean prove that it satisfies certain properties...

However when I try something like this:

def add (a: ℤ) (b: ℤ): ℤ := a + b

def add_sym (a: ℤ) (b: ℤ): add a b = add b a :=
  begin
    -- ???
  end

I don't have any idea to first prove the super obvious definitionally 100% correct fact that h: add a b = a + b :(. Any pointers?

[Mario Carneiro]

rfl

[Mario Carneiro]

in tactic mode, unfold add will change the goal to a + b = b + a

[Kevin Buzzard]

Because it's true by definition, you can use the change tactic. For example change a + b = b + a should work.

[agro1986]

@Mario Carneiro Great!

def add_sym (a: ℤ) (b: ℤ): add a b = add b a :=
  begin
    unfold add,
    ring,
  end

change tactic also works! Thanks @Kevin Buzzard

[agro1986]

@Kevin Buzzard Thank you for the compressed tactic mode proof also. It's kind of a magical experience that with Lean, you can just paste the proof and then I can interactively walk through it while seeing how the state changes. rcases and rintros with their pattern matching is so useful.

[Reid Barton]

I think a better definition would conclude ∀ (c: ℤ), divides c a ∧ divides c b → divides c d. Then asssume d >= 0. You don't need the ¬(a = 0 ∧ b = 0) part.