# Zulip Chat Archive

## Stream: new members

### Topic: Simple tactic for sum of natural numbers

#### Elvorfirilmathredia (Dec 12 2019 at 11:56):

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 (Dec 12 2019 at 13:51):

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 (Dec 12 2019 at 13:54):

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 (Dec 12 2019 at 13:55):

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

#### Elvorfirilmathredia (Dec 12 2019 at 17:47):

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:

Last updated: May 16 2021 at 05:21 UTC