I proved divisibility is transitive!

Stream: new members

[agro1986]

I was learning number theory before discovering Lean, so it's pretty exciting that I can describe and prove the statement "If a divides b, and b divides c, then a divides c"!

variables {a b c: ℤ}

constant divides: ℤ → ℤ → Prop

axiom divides_expand: divides a b → ∃(d: ℤ), a * d = b
axiom divides_conclude: (∃(d: ℤ), a * d = b) → divides a b

theorem divides_trans (hab: divides a b) (hbc: divides b c):
divides a c :=
  have h1: ∃m, a * m = b, from divides_expand hab,
  have h2: ∃n, b * n = c, from divides_expand hbc,
  exists.elim h1 (assume m: ℤ, assume hamb: a * m = b,
    exists.elim h2 (assume n: ℤ, assume hbnc: b * n = c,
      have c = a * (m * n) , from calc
           c = b * n       : hbnc.symm
         ... = (a * m) * n : congr_arg _ hamb.symm
         ... = a * (m * n) : mul_assoc _ _ _,
      have a * (m * n) = c, from this.symm,
      have ∃mn, a * mn = c, from ⟨m * n, this⟩,
      divides_conclude this
  ))

theorem two_divides_four: divides 2 4 :=
  have 2 * 2 = (4: ℤ), from refl _,
  have ∃(d: ℤ), 2 * d = 4, from ⟨2, this⟩,
  divides_conclude this

axiom four_divides_twenty: divides 4 20 -- same as above

theorem two_divides_twenty: divides 2 20 :=
  divides_trans two_divides_four four_divides_twenty

Still a beginner, so feel free to nitpick or correct the way I'm writing it :)

[Johan Commelin]

Instead of axioms you could use def

[Johan Commelin]

And in fact, I think a \| b already makes sense in plain Lean for integers a and b. So you can even have nice notation.

[Kevin Buzzard]

USE TACTIC MODE

[Johan Commelin]

Kevin, are you talking to a mathematician or a computer scientist?

[Kevin Buzzard]

They're doing number theory!

[Kevin Buzzard]

Not only that, but look at it! You can do it all in half the space in tactic mode.

[Kevin Buzzard]

And it's easier to follow

[Kevin Buzzard]

import tactic.ring

variables {a b c: ℤ}

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

theorem divides_trans (hab: divides a b) (hbc: divides b c):
divides a c :=
begin
  cases hab with d hd,
  cases hbc with e he,
  use d * e,
  rw [he, hd],
  ring,
end

theorem two_divides_four: divides 2 4 :=
begin
  use 2,
  norm_num
end

theorem four_divides_twenty: divides 4 20 := ⟨5, by norm_num⟩

theorem two_divides_twenty: divides 2 20 :=
  divides_trans two_divides_four four_divides_twenty

Tactic mode is much tidier in this situation don't you think?

[Kevin Buzzard]

I guess what is happening here is that I am reflecting the theory in the way I see it -- "if b=d*a and c=e*b and I want to solve c=x*a for x then I'm going to use d*e and then it's just boring calculations".

[Kevin Buzzard]

I guess it's a cases of what people find beautiful/interesting. I've noticed that computer scientists can get excited by all these details but I don't want to see the pain that @agro1986 just went through proving $c=bn=(am)n=a(mn)$. On the other hand I get excited by the definition of a perfectoid space and computer scientists say "it's just a definition!"

[agro1986]

@Kevin Buzzard Wow, tactics mode makes it so concise and is exactly what I'm looking for! Thanks! I'm learning TPiL and haven't reached tactics yet but will start learning it from your rewrite :)

[Kevin Buzzard]

So I guess my comments would be: like Johan, I agree that you should avoid axioms; you never need them when doing mathematics (we already have plenty). I found ∃ (d: ℤ), b = a * d easier to use than ...a * d = b because I could do rewrites without having to use \l. I personally cannot stand all this have have have in the weird mode promoted by TPIL in chapters 2 to 4, I think tactic mode packages it all up in a much more coherent manner. My instinct is to use big tools at all times because then I don't have to think, but I think the only time I used ring I could have used mul_assoc (perhaps my life was easier than yours because I switched the definition of divides?), and both times I used norm_num I could have used refl.

[Kevin Buzzard]

You can learn tactic mode by going here: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Kevin Buzzard]

@agro1986 when I started here two years ago ring didn't exist and all these calculations had to be done by hand. My undergraduates found all this rw add_assoc very hard work and then Mario stepped in and wrote it and it was a real game-changer. https://xenaproject.wordpress.com/2018/06/13/ab3/ . Since then Rob Lewis wrote linarith which was another game changer -- we were doing basic undergraduate analysis in Lean and the tactic made a whole bunch of inequality-chasing on the real numbers much easier.

[agro1986]

@Johan Commelin Thanks for the suggestion! I guess because there are so many choices (e.g., variable vs constant, axiom vs def vs theorem) It'll be a while before I can get a "feel" on which is the best to use

[Bryan Gin-ge Chen]

Tactics are wonderful since you can inspect the tactic state, but they can make things less transparent since they are often used as a black box. I think it's not an issue in this specific case, but I could imagine that in some instances, a proof using high-powered tactics like ring and norm_num for elementary facts could end up depending on the proof of the same fact (or something stronger) somewhere else in mathlib. I once lost points in a representation theory course for appealing to Jordan-Hölder without proving it myself; I sort of see this as roughly analogous.

[Kevin Buzzard]

We don't have tactics which are sufficiently powerful to deserve the name "black box" yet :D

[agro1986]

@Kevin Buzzard Thanks for the natural number game link! Will check it out. Great point about b = a * d easier to use than a * d = b. Actually a * d = b is the written form straight out of my number theory textbook haha. Gotta start thinking more about subtle things like that.

[Bryan Gin-ge Chen]

The state of my meta knowledge means that every tactic is a black box. (Much like Jordan-Hölder was, in fact :sweat_smile:)

[Kevin Buzzard]

yeah, don't trust mathematicians, they somehow think that a*d=b and b=a*d are the same.

[Kevin Buzzard]

At least, proper mathematicians do.

[Kevin Buzzard]

example : 12345 * 54321 = 670592745 := by norm_num
example (a b : ℤ) : (a + b)^3 = a^3+3*a*b^2+3*a^2*b+b^3 := by ring

If you want to call these black boxes then fair enough, but my feeling is that if a new 1st year maths undergraduate asserted either of these claims to a lecturer here and claimed they were true, the lecturer would not ask for a proof -- the techniques used are in both cases "standard". So I would rather call applications of these tactics "enabling mathematicians to do mathematics the way they expect to be able to do it" rather than elevating what is going on to the level of "black box". Of course you see from that blog post that there's a heck of a lot going on with the ring example! But because the answer is "obvious" we mathematicians shouldn't need to care about what's going on.

[Kevin Buzzard]

Why are there red boxes around the ^ signs by the way? @Bryan Gin-ge Chen that's the sort of thing you know :D

[Bryan Gin-ge Chen]

Yes, I think we're mostly in agreement. I guess I would feel more comfortable if I knew how to inspect all the "dependencies" of a theorem.

[Kevin Buzzard]

In this case they are a mass of mathematicial trivialities which have some computer science content, reflecting the fact that mathematics is not the same as type theory

[Bryan Gin-ge Chen]

The red boxes are because Zulip is relying on pygments for syntax highlighting and that's out of date. I think there were discussions right around when I joined about fixing it but I guess they never went anywhere.

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

In this case they are a mass of mathematicial trivialities which have some computer science content, reflecting the fact that mathematics is not the same as type theory

Oh -- in the norm_num case they are also reflecting the fact that computer scientists care about runtime. We mathematicians all know the proof is just rfl because we know it will work and we don't care how long it will take.

[Bryan Gin-ge Chen]

In this case they are a mass of mathematicial trivialities

Right, my point is just that there is potentially an issue here for new people trying to prove simple things.