Zulip Chat Archive

Stream: general

Topic: norm_num and nat.fact


view this post on Zulip Reid Barton (Aug 01 2019 at 19:01):

norm_num doesn't seem to know what to do with nat.succ:

example : nat.fact 5 = 120 := begin
  norm_num,
  -- ⊢ nat.succ 4 * (nat.succ 3 * (nat.succ 2 * nat.succ 1)) = 120
end

view this post on Zulip Reid Barton (Aug 01 2019 at 19:01):

But when I try a simpler example like nat.succ 5 = 6, it does work for some reason

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 19:03):

You clearly need to use more powerful automation like rfl

view this post on Zulip Floris van Doorn (Aug 01 2019 at 19:07):

Ah, I'm not the only one doing IMO 2019-4 :)

view this post on Zulip Floris van Doorn (Aug 01 2019 at 19:07):

I used norm_num [finset.range_succ, nat.pow_succ, nat.mul_succ] for the easy direction.

view this post on Zulip Floris van Doorn (Aug 01 2019 at 19:10):

I'm stuck on prime (2 : ℤ) (the definition of prime for rings :) )

view this post on Zulip Johan Commelin (Aug 01 2019 at 19:10):

Didn't Chris prove that primes in nat are primes in int?

view this post on Zulip Floris van Doorn (Aug 01 2019 at 19:14):

Is it in mathlib? I cannot find it.


Last updated: May 10 2021 at 23:11 UTC