# Zulip Chat Archive

## Stream: general

### Topic: a wild `nat.add` appears

#### Scott Morrison (Feb 28 2019 at 10:12):

Can anyone explain why the `nat.add`

s are appearing here? I'd really prefer to stay in the hygenic world of `(+)`

.

example (p : ℕ) (h : p ∈ range 2) : true := begin cases h, trivial, cases h, trivial, cases h, end

#### Scott Morrison (Feb 28 2019 at 10:12):

How insane is `@[simp] lemma nat.add_plus (a b : ℕ) : nat.add a b = a + b := rfl`

as a simp lemma?

#### Kevin Buzzard (Feb 28 2019 at 10:35):

When I was doing cases on < yesterday on your challenge problem this phenomenon occurred to me too.

#### Kevin Buzzard (Feb 28 2019 at 11:00):

I was getting `nat.less_than_or_equals_to (nat.succ ...)`

. In my case it was because `cases`

was literally using the names of the constructors rather than using our nicer variants

#### Kevin Buzzard (Feb 28 2019 at 11:04):

I realise I don't understand the `cases`

tactic. It comes out nicer if you do this:

open list example (p : ℕ) (h : p ∈ range 2) : false := begin unfold has_mem.mem at h, unfold range at h, unfold range_core at h, unfold list.mem at h, cases h, sorry, cases h, sorry, cases h, end

#### Gabriel Ebner (Feb 28 2019 at 11:10):

This is a result of how Lean unfolds definitions. For example `2`

is syntax for `bit0 1`

, which reduces to `nat.add 1 1`

, which reduces to `nat.succ (nat.add 1 0)`

, and so on. Here the unfolding happens due to unification, since `range`

is defined by a pattern-match on `succ n`

. So we have to find some n such that `succ n = 2`

. And now Lean starts unfolding `2`

until it sees a `succ`

.

#### Scott Morrison (Feb 28 2019 at 20:42):

Thanks, @Gabriel Ebner .

Last updated: Aug 03 2023 at 10:10 UTC