dirty nom_cast

Stream: maths

[Patrick Massot]

@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

[Rob Lewis]

@[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.

[Floris van Doorn]

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]

[Floris van Doorn]

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