proving sum(range 0) = 0

Stream: new members

[Luis O'Shea]

How do I prove example : sum(range 0) = 0 := sorry? (This seems embarrassingly simple, but as soon as I wander off the guided path of the natural number game, basic stuff like this shows up.)

[Kenny Lau]

there should be some lemma starting with range_zero that shows that it's the empty set

[Kenny Lau]

then there should be something about sum_empty or empty_sum or etc

[Mario Carneiro]

simp?

[Mario Carneiro]

rfl?

[Mario Carneiro]

not really sure what sum and range you are talking about so it's hard to be more specific

[Luis O'Shea]

Sorry -- these are the listversions (the example is preceded by import data.list.basic and open nat list). Neither simp nor rfl seem to work.

[Kevin Buzzard]

If you posted complete working code it would make people's lives a bit easier.

[Kevin Buzzard]

import data.list.basic
open list nat
example : sum(range 0) = 0 := rfl

Works for me.

[Luis O'Shea]

Thanks -- it works for me too (I had put rfl between begin ... end).

[Bryan Gin-ge Chen]

In tactic mode you could use exact rfl or refl. They're not exactly equivalent, I think refl works a little harder to close the goal.

[Kevin Buzzard]

Yeah, I was in term mode. The tactic version is refl.

[Kevin Buzzard]

The natural number game hides the following thing: x + 0 is defined to be x, so if you want to prove x + 0 = x although I was encouraging you to write rw add_zero you can just close this goal immediately with refl!

[Floris van Doorn]

In tactic mode you could use exact rfl or refl. They're not exactly equivalent, I think refl works a little harder to close the goal.

The main difference is that rfl is the (term)-proof that equality is reflexive, and the refl tactic works on any relation that is marked with @[refl] (like le, equiv, ...)