Zulip Chat Archive

Stream: general

Topic: a wild `nat.add` appears


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 28 2019 at 20:42):

Thanks, @Gabriel Ebner .


Last updated: May 10 2021 at 18:22 UTC