Zulip Chat Archive

Stream: maths

Topic: int.coe_nat_max


view this post on Zulip Kevin Buzzard (Sep 06 2018 at 17:13):

I don't think int.coe_nat_max : {m n : ℕ} : (↑(max m n) : ℤ) = max m n is in mathlib, and I needed it today. Kenny produced this proof:

theorem int.coe_nat_max {m n : } : ((max m n) : ) = max m n :=
begin
  unfold max,simp [int.coe_nat_le],
  split_ifs;refl,
end

but I was thinking that the result probably lived near the beginning of data.int.basic and I'm not sure that the devs will want split_ifs to be used in such a low-level file. Should it go later on or should we think of a more low-level proof? (or is it there already?)

view this post on Zulip Mario Carneiro (Sep 06 2018 at 17:28):

I agree this belongs in data.int.basic, and there is no problem using split_ifs. The mathlib tactics are all very low in the dependency order so that mathlib can use them


Last updated: May 10 2021 at 06:13 UTC