Zulip Chat Archive

Stream: maths

Topic: dirty nom_cast


view this post on Zulip Patrick Massot (Sep 21 2019 at 20:02):

@Paul-Nicolas Madelaine and @Rob Lewis do you know how I could clean the following two lemmas:

@[simp, move_cast] theorem cast_fpow {α : Type*} [discrete_field α] [char_zero α] (q) (k : ) :
  ((q ^ k : ) : α) = q ^ k :=
begin
  cases k,
  { erw fpow_of_nat,
    rw rat.cast_pow,
    erw fpow_of_nat },
  { rw fpow_neg_succ_of_nat,
    rw fpow_neg_succ_of_nat,
    norm_cast }
end

lemma num_aux (p : ) (n : ) :  (coe :   ) ((p : ) ^ n) = (p : ) ^ n :=
begin
  rw cast_fpow,
  congr' 1,
  norm_cast
end

view this post on Zulip Rob Lewis (Sep 23 2019 at 08:08):

@[simp, elim_cast] theorem cast_fpow {α : Type*} [discrete_field α] [char_zero α] (q : ) (k : ) :
  ((q ^ k : ) : α) = q ^ k :=
begin
  cases k,
  { erw [fpow_of_nat, rat.cast_pow, fpow_of_nat] },
  { simp only [fpow_neg_succ_of_nat], norm_cast }
end

lemma num_aux (p : ) (n : ) :  (coe :   ) ((p : ) ^ n) = (p : ) ^ n :=
begin
  norm_cast
end

Not sure right now why the erw is needed there, but whatever makes rw and simp fail is probably also making norm_cast fail.

view this post on Zulip Floris van Doorn (Sep 23 2019 at 15:45):

The problem is that fpow_of_nat is stated using (coe : ℕ → ℤ), while in the goal we have int.of_nat which are not syntactically equal. This works:

@[simp] lemma fpow_of_nat' {α} [division_ring α] (a : α) (n : ) : a ^ int.of_nat n = a ^ n := rfl

@[simp, elim_cast] theorem cast_fpow {α : Type*} [discrete_field α] [char_zero α] (q : ) (k : ) :
  ((q ^ k : ) : α) = q ^ k :=
by cases k; simp [fpow_neg_succ_of_nat]

view this post on Zulip Floris van Doorn (Sep 23 2019 at 15:47):

Although the actual missing simp lemma is that int.of_nat should be turned into a coercion:

@[simp] lemma of_nat_eq_coe (n : ) : int.of_nat n = n := rfl

Last updated: May 09 2021 at 09:11 UTC