Simple tactic for sum of natural numbers

Stream: new members

[Elvorfirilmathredia]

A while ago there was a discussion about how to prove sum(range(n+1)) = n*(n+1)/2, and the solution was along the lines of

lemma nat_sum (n : ℕ) : 2 * sum(range(n+1)) = n*(n+1) :=
begin
  induction n with n ih,
    refl,
  rw [range_concat, sum_append, mul_add, ih],

  suffices : n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1),
    simp,
    assumption,

  ring,
end

After reading the tactics chapter in "Programming in Lean" I wanted to write a tactic for the nat_sum lemma above as an exercise.
Unfortunately this turned out to be way trickier than I expected ...

I started with the induction part and wrote the following (incomplete) tactic:

meta def sum_range : tactic unit :=
do ctx <- local_context,
   induction ctx.head [`n_, `ih_], -- Just using ctx.head as the first parameter is probably not ideal ...
     reflexivity,
-- but essentially everything works till here :)
-- next I would like to do the rewrite stuff.
-- I expected/hoped that (something like) the following works, but it doesn't
   t <- target,
   e <- to_expr ```(list.range_concat n_),
   rewrite t e,
   skip

To be precise, when executing the tactic lean tells me that rewrite tactic failed, lemma is not an equality nor a iff :shrug: .

Any help would be greatly appreciated

[Patrick Massot]

Hi. First let me give you a couple of practical Zulip advices. What really really help people helping other people is to get code they can copy-paste in a scratch file and run. Both your code snippets fail that criterion. You need to include the imports and name spaces opening. More tricky: it helps a lot if you describe the expected behavior of your tactic. I'll assume for now that you simply want the tactic to write exactly the same proof as what you did by hand, although this will give a very very specialized tactic (but that's fine as an exercise).

[Patrick Massot]

import tactic
import data.list

open list

lemma nat_sum (n : ℕ) : 2 * sum(range(n+1)) = n*(n+1) :=
begin
  induction n with n ih,
    refl,
  rw [range_concat, sum_append, mul_add, ih],
  suffices : n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1), by simpa,
  ring,
end

namespace tactic.interactive
open tactic
meta def sum_range : tactic unit :=
do ctx ← local_context,
   ih_name ← get_unused_name `ih,
   tactic.induction ctx.head [`n, ih_name],
     reflexivity,
   ih_expr ← get_local ih_name,
   e ← to_expr ```(list.range_concat),
   e' ← to_expr ```(list.sum_append),
   e'' ← to_expr ```(mul_add),
   e''' ← to_expr ```(nat.add_one),
   rewrite_target e,
   rewrite_target e',
   rewrite_target e'',
   rewrite_target ih_expr,
   `[simp only [add_zero, sum_cons, sum_nil]],
   rewrite_target e''' {symm:=tt}
end tactic.interactive

example (n : ℕ) : 2 * sum(range(n+1)) = n*(n+1) :=
begin
  sum_range,
  ring,
end

[Patrick Massot]

The above code works. Did you read https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md by the way?

[Elvorfirilmathredia]

What really really help people helping other people is to get code they can copy-paste in a scratch file and run. Both your code snippets fail that criterion. You need to include the imports and name spaces opening.

Good point, I'll pay more attention to this in the future.

The above code works. Did you read https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md by the way?

I read most of it, but didn't see anything that seemed helpful since rewrite is not used anywhere.

Anyway, thanks a lot for your help! :thank_you:
Shockingly my main mistake was apparently the usage of rewrite, since rewrite_target e is not exactly the same as rewrite e t. How could I miss that? :confused: