trigs.lean

import tactic
import data.real.basic 
import data.complex.exponential
import analysis.special_functions.trigonometric

open real

-- Better name?
lemma cos_npi_pos (n : ℤ) : cos ((2*n + 1)/2 * pi) = 0 :=
by rw [show (2 * ↑n + 1) / 2 * pi = n * pi + pi / 2, by { field_simp, ring },
       cos_add_pi_div_two,
       sin_int_mul_pi,
       neg_zero]

lemma cos_nat_mul_pi (n : ℕ) : cos (n * pi) = (-1)^n :=
begin
  induction n with k IH,
  { simp },
  { push_cast,
    rw [add_mul, one_mul, cos_add_pi, pow_succ, neg_one_mul, IH] }
end

-- auxiallary lemma for the next proof.
lemma neg_one_pow_neg (n : ℤ) : (-1 : ℝ)^(-n) = (-1)^n :=
begin
  rw [fpow_neg, inv_eq_one_div, div_eq_iff, ←fpow_add, ←two_mul, fpow_mul,
      show (-1 : ℝ)^(2:ℤ) = 1,
      begin
        rw show (2 : ℤ) = int.of_nat 2, by refl,
        rw fpow_of_nat,
        norm_num,
      end,
      one_fpow],
  norm_num,
  apply fpow_ne_zero,
  norm_num,
end

lemma cos_int_mul_pi (n : ℤ) : cos (n * pi) = (-1)^n :=
begin
  cases n,
  { simp only [int.cast_coe_nat, int.of_nat_eq_coe, fpow_coe_nat],
    exact cos_nat_mul_pi n },
  { rw [int.neg_succ_of_nat_eq],
    simp only [int.cast_coe_nat, int.cast_add, int.cast_one, neg_add_rev, int.cast_neg],
    rw [←neg_add, ←neg_add, ←neg_mul_eq_neg_mul, cos_neg, neg_one_pow_neg],
    have h : (1 : ℝ) + ↑n = ↑(1 + n), by simp only [nat.cast_add, nat.cast_one],
    have h2 : (1 : ℤ) + ↑n = int.of_nat (1 + n), by norm_num,
    rw [h, h2, fpow_of_nat],
    exact cos_nat_mul_pi _ }
end .

lemma sin_npi_pos (n : ℤ) : sin ((2*n + 1)/2 * pi) = (-1)^n :=
by rw [show (2 * ↑n + 1) / 2 * pi = n * pi + pi / 2, by { field_simp, ring }, 
       sin_add_pi_div_two,
       cos_int_mul_pi]