Library Coqtail.Complex.Ctacfield

Require Import Nnat.
Require Import Arith.
Require Export Ring Field.
Require Import Cbase.
Require Import Cpow.

Open Scope C_scope.

Tactics ring and field in the Complex field

Lemma Cring : @ring_theory C 0 1 Cadd Cmult Cminus Copp (eq(A:=C)).
Proof.
  constructor.
  exact Cadd_0_l.
  exact Cadd_comm.
  intros ; rewrite <- Cadd_assoc ; reflexivity.
  exact Cmult_1_l.
  exact Cmult_comm.
  symmetry; apply Cmult_assoc.
  intros; apply Cmult_add_distr_r.
  reflexivity.
  exact Cadd_opp_r.
Qed.

Lemma Cfield :
  @field_theory C 0 1 Cadd Cmult Cminus Copp Cdiv Cinv (eq(A:=C)).
Proof.
  constructor.
  exact Cring.
  exact C1_neq_C0.
  reflexivity.
  exact Cinv_l.
Qed.

Lemma C_power_theory : power_theory 1 Cmult (eq (A:=C)) nat_of_N Cpow.
Proof.
constructor.
intros z n ; elim n ; clear n.
reflexivity.
induction p ; simpl in ×.
   rewrite ZL6 ; rewrite Cpow_add ; rewrite IHp ; reflexivity.
  unfold nat_of_P ; rewrite <- IHp ; rewrite <- Cpow_add ; rewrite <- ZL6 ; reflexivity.
apply Cmult_1_r.
Qed.

Ltac Cpow_tac t :=
  match isnatcst t with
  | false ⇒ constr:(InitialRing.NotConstant)
  | _ ⇒ constr:(N_of_nat t)
  end.

Add Ring CRing : Cring( abstract).

Add Field CField : Cfield(power_tac C_power_theory [Cpow_tac]).