Stream: general

Topic: norm_num and nat.fact

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


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

Kevin Buzzard (Aug 01 2019 at 19:03):

You clearly need to use more powerful automation like rfl

Floris van Doorn (Aug 01 2019 at 19:07):

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

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.

Floris van Doorn (Aug 01 2019 at 19:10):

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

Johan Commelin (Aug 01 2019 at 19:10):

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

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