a wild `nat.add` appears

Stream: general

[Scott Morrison]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

Thanks, @Gabriel Ebner .