induction_ineq_nsqlefactn the hard way

Stream: new members

[Jiekai]

example (d : ℕ): 0 < 4 + (d + 1) :=
begin
  sorry
end

How should I prove this?

previous discussion

[Jiekai]

It's much harder than doing proofs in the tutorial and NNG.

[Yakov Pechersky]

Do you know how to prove 0 < 4? Do you know how to prove 4 <= 4 + x? Do you know how to chain inequalities?

[Damiano Testa]

You could either rearrange the parentheses, to exploit that the RHS is a successor and hence positive, or, I think, add_pos is a thing...

[Yakov Pechersky]

Yes, Damiano is right. Do you know how to prove 0 < succ n? What's nice about mathlib is that it mostly has a very "discoverable" naming scheme for lemmas.

[Jiekai]

pos_of_ne_zero?

[Damiano Testa]

... except that you have a succ instead of a ne_zero...

[Yakov Pechersky]

docs#nat.zero_lt_succ

[Jiekai]

succ_ne_zero

[Damiano Testa]

I was going to say succ_pos! :lol:

[Yakov Pechersky]

but there is also a docs#nat.succ_pos too!

[Jiekai]

ooh, I see. thanks

[Yakov Pechersky]

You were transforming the succ into an ne_zero statement, but that's another lemma too! These really basic lemmas are usually named exactly as you'd read them left-to-right. So something like 0 < 2 is zero_lt_two. And x <= x + y is nat.le_add_right.

[Damiano Testa]

Keep in mind that this kind of "low-level" arguments require some training: any mathematician would simply file this as "it is a sum of positive natural numbers, of course it is positive". However, you really have to give a precise reason to Lean and, successors being positive seems the most direct here.

[Yakov Pechersky]

Damiano, what would be the term-mode proof for your "most direct" claim?

[Jiekai]

theorem induction_ineq_nsqlefactn
  (n : ℕ)
  (h₀ : 4 ≤ n) :
  n^2 ≤ n! :=
begin
   have t0 := nat.exists_eq_add_of_le h₀,
   cases t0 with k hk,
   rw hk,
   clear hk h₀ n, -- necessary?
   induction k with d hd,
   { norm_num, },
   have step0 : d.succ = d + 1,
   { refl, },
   rw step0,
   clear step0,

   have step1 : (4 + (d + 1)) * (4 + (d + 1) - 1)! = (4 + (d + 1))!,
   {
     apply nat.mul_factorial_pred,
     sorry
   },

   have step2 : (4 + (d + 1)) ^ 2 ≤ (4 + d) ^ 2 * (4 + (d + 1)),
   {
     sorry
   },

   have step3 : (4 + d) ^ 2 * (4 + (d + 1)) ≤ (4 + d)! * (4 + (d + 1)),
   {
     sorry
   },

end

I'm giving up. It's getting out of control. :cry:

[Damiano Testa]

what I had in mind, was more something along the lines of

  rw ← add_assoc,
  exact nat.succ_pos _,

[Damiano Testa]

If I really had to to it in term mode, I would probably go with

example (d : ℕ): 0 < 4 + (d + 1) :=
nat.succ_pos _

but I would not like the abuse...

[Damiano Testa]

(I am not sure why my comments were sent in the opposite order in which I typed them)

[Yakov Pechersky]

Because of the way that addition on nats is defined, nat.succ_pos _ is enough!

[Damiano Testa]

Yes, indeed, but I think that the now-first approach is more "friendly".

[Yakov Pechersky]

I'd do zero_lt_four.trans_le le_self_add

[Yakov Pechersky]

Or

example (d : ℕ) : 0 < 4 + (d + 1) :=
(nat.zero_lt_succ (4 + d)).trans_le (add_assoc 4 d 1).le

[Damiano Testa]

Ah, I forget how high the zero_lt_n lemmas go! I would have proven 0 < 4 with succ_pos _ again!

[Yakov Pechersky]

@Jiekai , do these help you? docs#nat.factorial_succ docs#add_sq?

[Yakov Pechersky]

Again, found them by guessing the names.

[Damiano Testa]

(My zulip seems to have some issues and my messages come out delayed and out of order.)

[Patrick Massot]

This is all very instructive, but let's not forget to mention the correct answer is of course that Lean can prove it without any help, simply write:

example (d : ℕ) : 0 < 4 + (d + 1) :=
by linarith

[Yakov Pechersky]

My solution

import tactic

open_locale nat

theorem pow_two_le_factorial
  (n : ℕ)
  (h₀ : 4 ≤ n) :
  n^2 ≤ n! :=
begin
  obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h₀,
  clear h₀,
  rw [add_comm, nat.factorial_succ, sq],
  refine nat.mul_le_mul le_rfl _,
  induction k with d hd,
  { norm_num },
  rw [nat.succ_add, nat.succ_add, nat.factorial_succ],
  refine (nat.succ_le_succ hd).trans _,
  rw [nat.succ_mul, nat.succ_le_iff],
  simpa using nat.factorial_pos d
end

[Jiekai]

so much to learn! :octopus:

[Johan Commelin]

import tactic

open_locale nat
open nat

theorem pow_two_le_factorial (n : ℕ) (h₀ : 4 ≤ n) :
  n^2 ≤ n! :=
begin
  obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h₀,
  suffices : k + 4 ≤ (k + 3) * (k + 2),
  { simpa [add_comm, mul_assoc, pow_two] using mul_le_mul' this (factorial_pos (k+1)), },
  calc k + 4 ≤ (k + 4) + (k^2 + 4 * k + 2) : self_le_add_right _ _
         ... ≤ (k + 3) * (k + 2)           : by ring_nf,
end

[Kevin Buzzard]

@Jiekai I had a really hard time doing the first year undergraduate problem sheets which I was giving to my students when I was learning lean.

[Jiekai]

I played with NNG last year and had a lot of fun. Then haven't touched lean for more than a year.

Recently I'm thinking about learning some math for fun and thought lean could be useful. My near-term goal is to understand the Fundamental theorem of arithmetic in mathlib.

[Kevin Buzzard]

The first challenge would be figuring out how to state it, and before that you have to decide whether it's a theorem about naturals or integers

[Jiekai]

import tactic
import data.nat.parity
import data.nat.basic

open_locale nat

theorem induction_ineq_nsqlefactn
  (n : ℕ)
  (h₀ : 4 ≤ n) :
  n^2 ≤ n! :=
begin
   have t0 := nat.exists_eq_add_of_le h₀,
   cases t0 with k hk,
   rw hk,
   clear hk h₀ n, -- necessary?
   induction k with d hd,
   { norm_num, },
   have step0 : d.succ = d + 1,
   { refl, },
   rw step0,
   clear step0,

   have step00: 0 < (4 + (d + 1)),
   {
     linarith,
   },

   have step1 : (4 + (d + 1)) * (4 + (d + 1) - 1)! = (4 + (d + 1))!,
   {
     apply nat.mul_factorial_pred,
     exact step00,
   },

   have step2 : (4 + (d + 1)) ^ 2 ≤ (4 + d) ^ 2 * (4 + (d + 1)),
   {
     rw sq,
     apply mul_le_mul,
     {
       rw add_sq,
       rw sq,
       rw sq,
       have t20 : 4 + (d + 1) = 0 + (4 + d + 1),
       {
         ring,
       },
       have t21 : 4 * 4 + 2 * 4 * d + d * d = 11 + 7 * d + d * d + (4 + d + 1),
       {
         ring,
       },
       rw t20,
       rw t21,
       apply add_le_add_right,
       apply zero_le,
     },
     {
       refl,
     },
     {
       apply zero_le,
     },
     {
       apply zero_le,
     },
   },

   have step3 : (4 + d) ^ 2 * (4 + (d + 1)) ≤ (4 + (d + 1))!,
   {
     rw ← step1,
     have t30 : (4 + (d + 1)) * (4 + (d + 1) - 1)! =  (4 + d)! * (4 + (d + 1)),
     {
       ring,
     },
     rw t30,
     apply mul_le_mul,
     {
       apply hd,
     },
     {
       refl,
     },
     {
       apply zero_le,
     },
     {
       apply zero_le,
     },
   },

   have step4 : (4 + (d + 1)) ^ 2 ≤ (4 + (d + 1))!,
   {
     apply le_trans step2 step3,
   },

   exact step4,

end

Save the ugly one

[Kevin Buzzard]

@Jiekai you can write Lean far more compactly than this, for example your last 25 lines or so are just the same as

  have step3 : (4 + d) ^ 2 * (4 + (d + 1)) ≤ (4 + (d + 1))!,
  { rw [← step1, show (4 + (d + 1)) * (4 + (d + 1) - 1)! =  (4 + d)! * (4 + (d + 1)), by ring],
    apply mul_le_mul hd (le_refl _) (zero_le _) (zero_le _), },
  exact step2.trans step3,
end

[Jiekai]

Kevin Buzzard said:

Jiekai I had a really hard time doing the first year undergraduate problem sheets which I was giving to my students when I was learning lean.

I just found M1F from the title image of xena blog. :wink:

This post says

Of all the theorems I proved in M1F, de Moivre’s theorem (Theorem 3.2 of the course) is, I think, the only one which will need some work before it’s possible to verify it, the work in this case being a rigorous definition of the exponential function and its basic properties.

This is fun!

[Kevin Buzzard]

This work was done long ago :-)