Comments on proof

Stream: new members

[Luis O'Shea]

Below is my first proof after the natural number game. I have a few questions:

1. Is it idiomatic? (Especially to a mathematician rather than a computer scientist)
2. How do I determine what theorems were used in the simp in line (1)? (#print nat_sum is a bit long to be helpful)
3. In VS Code, placing the cursor at (2) shows only one goal (omitting 2 > 0). Why?

theorem nat_sum (n : ℕ) : sum(range n) = (n - 1) * n / 2 :=
begin
  induction n with n n_ih,
    refl,
  rw range_concat,
  simp, -- (1)
  -- rest mirrors `triangle_succ`
  rw [n_ih, add_comm, ← add_mul_div_left, ← right_distrib, mul_comm], -- (2)
    cases n; refl,
  apply zero_lt_succ -- 2 > 0
end

What would be a good challenge (in order to learn Lean) after the above?

[Andrew Ashworth]

Most end up reviewing TPIL, in order to be a competent user you will need to have an understanding of the underlying type theory; especially how to read and debug type errors. Knowing how to construct terms by hand is also very useful when trying to construct definitions, and I know Kevin is not very excited about Lean's term mode but I can't imagine not knowing how to use it, at least.

[Bryan Gin-ge Chen]

1) (Speaking generally, I haven't tried to "golf" your proof) there is some basic style advice in this file; in particular we usually use curly brackets to separate the proofs of individual goals. Also, using simp in the middle of a proof (a "non-terminal simp") is generally discouraged since such proofs can break if the simp lemmas change (which can happen depending on what files you have imported).

2) There are a few options that let you see the steps that the simplifier tries, see this doc. It can be quite verbose though.

Somewhat related: you can try replacing simp with squeeze_simp. It will return a message with a roughly equivalent simp only statement that has a (partial) list of used lemmas. It's not perfect though - it might miss some lemmas or have some extra ones.

3) is interesting, I'm not sure why the 2 > 0 goal introduced by the ← add_mul_div_left rewrite disappears outside the square brackets and then reappears later.

[Luis O'Shea]

Below is the new proof with suggestions (1) and (2) applied (thanks for squeeze_simp -- that was very helpful). The problem I now have is that having removed simp the long string of rewrites seems hard to read (to me). Is this really idiomatic?

theorem nat_sum (n : ℕ) : sum(range n) = (n - 1) * n / 2 :=
begin
  induction n with n n_ih,
  { refl },
  { rw [range_concat, sum_append, sum_cons, sum_nil, n_ih,
        ← add_mul_div_left, add_zero, ← right_distrib, mul_comm,
        succ_sub_succ_eq_sub, nat.sub_zero],
    { cases n;refl },
    { apply zero_lt_succ } }
end

[Kevin Buzzard]

I feel a bit bad that I didn't introduce the { } convention in the natural number game. It was because it was always induction on nat, and the base case was usually trivial. There is some talk about this in TPIL, there are several conventions for this sort of thing and I always thought of them as equal but mathlib seems to have chosen one and hence this should probably be the one I'm promoting.

[Kevin Buzzard]

The long string of rewrites is hiding a triviality. To be honest I would have been too scared to approach this sum because integer division is hard to work with (5/2=2 etc). I would have been tempted to either prove 2*sum = ... or to work with rationals.

[Kevin Buzzard]

Here's my effort.

import data.list.basic  tactic.ring
open list nat

theorem nat_sum (n : ℕ) : sum(range n) = (n - 1) * n / 2 :=
begin
  suffices : 2 * sum (range n) = (n - 1) * n, -- terrified of denominators
    rw ←this, simp,
  -- induction
  induction n with n n_ih, refl, -- base case done
  rw [range_concat, sum_append, mul_add, n_ih], -- just enough to use induction hypo
  cases n, refl, -- to deal with awkward n - 1 case when n = 0
  -- ring won't work until the singleton sum and succ and subtraction are gone
  -- and simp will rmove most of these. But I can't use simp in the middle of a proof.
  -- So first I wrote `simp, repeat {rw succ_eq_add_one}`, and now I copy paste the result
  suffices : n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1),
    simpa using this,
  ring,
end

[Kevin Buzzard]

My philosophy is that if what you're doing is clear you can just try and kill the result quickly with tactics and hang readibility, just add comments