Zulip Chat Archive

Stream: new members

Topic: proving sum(range 0) = 0


Luis O'Shea (Nov 19 2019 at 07:04):

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 (Nov 19 2019 at 07:07):

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

Kenny Lau (Nov 19 2019 at 07:07):

then there should be something about sum_empty or empty_sum or etc

Mario Carneiro (Nov 19 2019 at 07:13):

simp?

Mario Carneiro (Nov 19 2019 at 07:13):

rfl?

Mario Carneiro (Nov 19 2019 at 07:14):

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

Luis O'Shea (Nov 19 2019 at 15:46):

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 (Nov 19 2019 at 15:48):

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

Kevin Buzzard (Nov 19 2019 at 15:48):

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

Works for me.

Luis O'Shea (Nov 19 2019 at 18:06):

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

Bryan Gin-ge Chen (Nov 19 2019 at 18:14):

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 (Nov 19 2019 at 18:16):

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

Kevin Buzzard (Nov 19 2019 at 18:17):

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 (Nov 20 2019 at 00:19):

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, ...)


Last updated: Dec 20 2023 at 11:08 UTC