## Stream: general

### Topic: a wild nat.add appears

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

Can anyone explain why the nat.adds 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: May 10 2021 at 18:22 UTC