Zulip Chat Archive

Stream: maths

Topic: norm_num and fact


view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:57):

import data.nat.basic
import tactic.norm_num

open nat

example : fact 7  3 ^ 7 :=
begin
--  unfold fact, norm_num, -- fails, perhaps because of succ's
  show 7 * (6 * (5 * (4 * (3 * (2 * (1 * 1))))))  3 ^ 7,
  norm_num,
end

@Mario Carneiro Can you get norm_num to know enough about fact to make this work? After unfolding fact I get a goal with a lot of nat.succ's in. Or is this harder than it looks?

view this post on Zulip Mario Carneiro (Nov 18 2018 at 16:02):

I think you can rewrite nat.succ to +1 and then apply norm_num

view this post on Zulip Mario Carneiro (Nov 18 2018 at 16:31):

example : fact 7  3 ^ 7 :=
by dsimp only [fact, succ_eq_add_one]; norm_num

Last updated: May 09 2021 at 10:11 UTC