FinMatrix.CoqExt.Complex


Require Export Hierarchy.
Require Export NatExt RExt.
Require Export Lra.

Open Scope R_scope.

Some useful properties


Section general_useful_props.

Basic inequality
ineq1
  Lemma basic_ineq1 : forall a b : R, sqrt (a * a + b * b) <= Rabs a + Rabs b.
  Proof.
    intros.
    rewrite <- sqrt_square.
    - apply sqrt_le_1_alt.
      apply Rle_trans with (Rabs a * Rabs a + Rabs b * Rabs b)%R.
      + rewrite <- !Rabs_mult. apply Rplus_le_compat.
        apply RRle_abs. apply RRle_abs.
      + ring_simplify.
        rewrite !Rplus_assoc. apply Rplus_le_compat_l.
        rewrite <- Rplus_0_l at 1. apply Rplus_le_compat_r.
        assert (0 <= Rabs a) by ra; assert (0 <= Rabs b) by ra. ra.
    - assert (0 <= Rabs a) by ra; assert (0 <= Rabs b) by ra. ra.
  Qed.

ineq2
  Lemma basic_ineq2 : forall a b c d : R, a * c + b * d <= sqrt((a² + b²) * (c² + d²)).
  Proof.
    intros.
    apply Rsqr_incr_0_var; ra. ring_simplify.
    autorewrite with R sqrt; ra.
    ring_simplify.
    rewrite !Rplus_assoc; repeat apply Rplus_le_compat_l.
    rewrite <- !Rplus_assoc; repeat apply Rplus_le_compat_r.
    autorewrite with R.
    replace (2 * a * c * b * d)%R with (2 * (a * d) * (b * c))%R by ring.
    replace (a² * d² + c² * b²)%R with ((a*d)² + (b * c)²)%R; try (cbv; ring).
    apply R_neq1.
  Qed.

End general_useful_props.

period function on Z type, the coq-std-lib only defined it on nat type
Section cos_sin_period.


  Lemma cos_period_Z : forall (x:R) (k:Z), cos (x + 2 * IZR k * PI) = cos x.
  Proof.
    intros x k. induction k.
    -
      replace 0 with (INR 0); auto. apply cos_period.
    -
      replace (Z.pos p) with (Z.of_nat (Pos.to_nat p)).
      + rewrite <- INR_IZR_INZ. apply cos_period.
      + apply positive_nat_Z.
    -
      replace (Z.neg p) with (- (Z.of_nat (Pos.to_nat p)))%Z.
      + rewrite Ropp_Ropp_IZR.
        rewrite <- INR_IZR_INZ.
        rewrite <- Ropp_mult_distr_r.
        rewrite Ropp_mult_distr_l_reverse.
        induction (Pos.to_nat p).
        * replace (x + - (2 * INR 0 * PI)) with x; auto.
          replace (INR 0) with 0; auto; ring.
        * replace (x + - (2 * INR (S n) * PI)) with
            (x - (2 * INR n * PI) - 2 * PI).
          { rewrite cos_minus. rewrite !sin_2PI,!cos_2PI. ring_simplify; auto. }
          { rewrite S_INR. ring. }
      + rewrite positive_nat_Z. auto.
  Qed.

  Lemma sin_period_Z : forall (x:R) (k:Z), sin (x + 2 * IZR k * PI) = sin x.
  Proof.
    intros x k. induction k.
    -
      replace 0 with (INR 0); auto. apply sin_period.
    -
      replace (Z.pos p) with (Z.of_nat (Pos.to_nat p)).
      + rewrite <- INR_IZR_INZ. apply sin_period.
      + apply positive_nat_Z.
    - replace (Z.neg p) with (- (Z.of_nat (Pos.to_nat p)))%Z.
      + rewrite Ropp_Ropp_IZR.
        rewrite <- INR_IZR_INZ.
        rewrite <- Ropp_mult_distr_r.
        rewrite Ropp_mult_distr_l_reverse.
        induction (Pos.to_nat p).
        * replace (x + - (2 * INR 0 * PI)) with x; auto.
          replace (INR 0) with 0; auto; ring.
        * replace (x + - (2 * INR (S n) * PI)) with
            (x - (2 * INR n * PI) - 2 * PI).
          { rewrite sin_minus; rewrite !sin_2PI,!cos_2PI. ring_simplify; auto. }
          { rewrite S_INR. ring. }
      + rewrite positive_nat_Z. auto.
  Qed.

End cos_sin_period.

Definition of C and basic operations

Scope for complex number
Declare Scope C_scope.
Delimit Scope C_scope with C.
Bind Scope C_scope with C.
Open Scope C_scope.

Definition of complex number

Section def.

  Definition C : Set := R * R.

Convert two real numbers to a complex number
  Definition RR2C (a : R) (b : R) : C := (a, b).
  Infix " '+i' " := RR2C (at level 60) : C_scope.

Convert a real number to a complex number
  Definition IRC (a : R) : C := a +i 0.
  Coercion IRC : R >-> C.

Common constant complex numbers
  Definition C0 := 0 +i 0.
  Definition C1 := 1 +i 0.
  Definition Ci := 0 +i 1.
  Notation "0" := C0 : C_scope.
  Notation "1" := C1 : C_scope.

  Definition Cre (z : C) : R :=
    let (a, b) := z in
    a.
  Notation "z .a" := (Cre z) (at level 20, format "z .a") : C_scope.

  Definition Cim (z : C) : R :=
    let (a, b) := z in
    b.
  Notation "z .b" := (Cim z) (at level 20, format "z .b") : C_scope.

  Lemma Cproj_right : forall z : C, z = (z.a, z.b).
  Proof.
    intros (a,b). auto.
  Qed.

  Lemma Cexist_rep_complex : forall a b : R, exists x : C, Cre x = a /\ Cim x = b.
  Proof.
    intros. exists (a +i b). auto.
  Qed.

Equality on C is decidable
  #[export] Instance Complex_eq_Dec : Dec (@eq C).
  Proof.
    constructor. intros (a1,b1) (a2,b2).
    destruct (Aeqdec a1 a2), (Aeqdec b1 b2); subst.
    - left; auto.
    - right; intro; inv H; easy.
    - right; intro; inv H; easy.
    - right; intro; inv H; easy.
  Qed.

  Lemma Ceq_iff : forall z1 z2 : C, z1 = z2 <-> z1.a = z2.a /\ z1.b = z2.b.
  Proof.
    intros (a1,b1) (a2,b2). split; intros H; inv H; auto.
    simpl in *; subst. auto.
  Qed.

Two complex numbers are neq, iff at least one components are neq
  Lemma Cneq_iff : forall z1 z2 : C, z1 <> z2 <-> (z1.a <> z2.a \/ z1.b <> z2.b).
  Proof.
    intros (a1,b1) (a2,b2); simpl.
    split; intros.
    - destruct (Aeqdec a1 a2), (Aeqdec b1 b2); subst; auto.
    - destruct (Aeqdec a1 a2), (Aeqdec b1 b2); subst; auto.
      + intro H1; inv H1. destruct H; auto.
      + intro H1; inv H1. destruct H; auto.
      + intro H1; inv H1. destruct H; auto.
      + intro H1; inv H1. destruct H; auto.
  Qed.

1 <> 0
  Lemma C1_neq_C0 : 1 <> 0.
  Proof.
    intro H.
    apply (proj1 (Ceq_iff _ _)) in H. simpl in *. destruct H; auto with R.
  Qed.

End def.

Hint Resolve C1_neq_C0 : complex.

Infix " '+i' " := RR2C (at level 60) : C_scope.
Notation "0" := C0 : C_scope.
Notation "1" := C1 : C_scope.
Notation "z .a" := (Cre z) (at level 20, format "z .a") : C_scope.
Notation "z .b" := (Cim z) (at level 20, format "z .b") : C_scope.

Tactics for basic proof on complex number

simplify the environment contain complex numbers
Ltac Csimpl :=
  intros;
  repeat
    match goal with
    | z:C |- _ => destruct z as (?a,?b)
    end;
  simpl.

equality of complex numbers
Ltac Ceq :=
  Csimpl;
  apply (proj2 (Ceq_iff _ _));
  split; simpl; try lra.

Injection from nat or Z to complex numbers

Section INC_IZC.

Injection from N to C
  Definition INC (n : nat) : C := (INR n) +i 0.

Injection from Z to C
  Definition IZC (z : Z) : C := (IZR z) +i 0.

End INC_IZC.

Operations and properties of complex number

Square of norm of complex number

Section Cnorm2.

square of norm
  Definition Cnorm2 (z : C) : R :=
    z.a * z.a + z.b * z.b.

Note that, this notation is too complex, but I havn't found a simple style now
  Notation "C2| z |" := (Cnorm2 z) : C_scope.

z is zero, iff its norm2 is zero
  Lemma C0_norm_R0 : forall z, z = 0 <-> C2|z| = 0%R.
  Proof.
    Csimpl. cbv.
    split; intros H; inv H; try lra.
    assert (a = R0) by nra.
    assert (b = R0) by nra. subst. f_equal; auto.
  Qed.

z <> 0 <-> C2 |z| <> 0
  Lemma Cneq0_iff_norm2_neq0 : forall z : C, z <> 0 <-> C2|z| <> 0%R.
  Proof.
    intros. split; intros; intro.
    - apply C0_norm_R0 in H0. easy.
    - apply C0_norm_R0 in H0. easy.
  Qed.

0 <= Cnorm2 z
  Lemma Cnorm2_ge0 (z : C) : 0 <= C2|z|.
  Proof.
    destruct z. unfold Cnorm2; simpl.
    apply Rplus_le_le_0_compat; apply Rle_0_sqr.
  Qed.

0 < x*x + y*y <-> (x,y) <> 0
  Lemma Cnorm2_pos_iff (x y : R) : (0 < x * x + y * y) <-> (x, y) <> 0.
  Proof.
    split; intros.
    - intro. inversion H0. subst. lra.
    - apply prod_neq_iff in H; simpl in H. ra.
  Qed.

End Cnorm2.

Global Hint Resolve Cnorm2_pos_iff : complex.

Notation "R| r |" := (Rabs r) : R_scope.
Notation "C2| z |" := (Cnorm2 z) : C_scope.

Norm of complex number

Section Cnorm.

  Definition Cnorm (z : C) : R :=
    (sqrt (Cnorm2 z)).
  Notation "C| z |" := (Cnorm z) : C_scope.

Cnorm2 z = (Cnorm z)²
  Lemma Cnorm2_eq (z : C) : C2|z| = (C|z|)².
  Proof. unfold Cnorm. rewrite Rsqr_sqrt; auto. apply Cnorm2_ge0. Qed.

z = 0 <-> |z| = 0
  Lemma Cnorm0_iff_C0 : forall z : C, z = 0 <-> C|z| = R0.
  Proof.
    Csimpl. cbv. split; intros.
    - inv H. ring_simplify. apply Rsqrt_plus_sqr_eq0_iff. auto.
    - apply Rsqrt_plus_sqr_eq0_iff in H. destruct H. subst. auto.
  Qed.

0 <= |z|
  Lemma Cnorm_pos : forall z : C, 0 <= C|z|.
  Proof. Csimpl. unfold Cnorm. ra. Qed.

0 <= |z|
  Lemma Cnorm_ge0 (z : C) : 0 <= C|z|.
  Proof. unfold Cnorm. apply sqrt_pos. Qed.

z <> 0 -> 0 < |z|
  Lemma Cnorm_pos_lt : forall z : C, z <> 0 -> R0 < C|z|.
  Proof.
    intros z Hz; case (Cnorm_pos z); intro H; auto.
    apply eq_sym, Cnorm0_iff_C0 in H. easy.
  Qed.

z <> 0 <-> |z| <> 0
  Lemma Cnorm_neq0_iff_neq0 : forall z : C, z <> 0 <-> C|z| <> R0.
  Proof.
    intros (a,b). cbv. split; intros H.
    - intro. apply Rsqrt_plus_sqr_eq0_iff in H0. inv H0. easy.
    - intro. inv H0. destruct H. apply Rsqrt_plus_sqr_eq0_iff. easy.
  Qed.

|0| = 0
  Lemma Cnorm_C0 : C|C0| = R0.
  Proof.
    cbv.
    replace (R0 * R0 + R0 * R0)%R with 0%R by ring.
    exact sqrt_0.
  Qed.

|(a,0)|=|a|
  Lemma Cnorm_Cre_simpl : forall (a : R), C|(a, R0)| = R|a|.
  Proof.
    intros; unfold Cnorm, Cnorm2; simpl.
    rewrite Rmult_0_r, Rplus_0_r; apply sqrt_Rsqr_abs.
  Qed.

|(0,b)|=|b|
  Lemma Cnorm_Cim_simpl : forall (a : R), C|(R0, a)| = R|a|.
  Proof.
    intros; unfold Cnorm, Cnorm2; simpl.
    rewrite Rmult_0_l, Rplus_0_l; apply sqrt_Rsqr_abs.
  Qed.

|(a,b)|=|(b,a)|
  Lemma Cnorm_comm : forall (a b : R), C|(a, b)| = C|(b, a)|.
  Proof.
    intros; unfold Cnorm, Cnorm2.
    simpl; rewrite Rplus_comm; reflexivity.
  Qed.

|z| > 0 -> z <> 0
  Lemma Cnorm_gt_not_eq : forall z, C|z| > R0 -> z <> 0.
  Proof.
    intros. destruct (Aeqdec z 0); auto.
    subst. rewrite Cnorm_C0 in H. lra.
  Qed.

|IRC x| = |x|
  Lemma Cnorm_IRC_Rabs : forall a, C|IRC a| = R|a|.
  Proof.
    intros. cbv. rewrite Rmult_0_r, Rplus_0_r; apply sqrt_Rsqr_abs.
  Qed.

| |z| | = |z|, that is: | IRC (|z|) | = |z|
  Lemma Cnorm_norm : forall z : C, C|C|z| | = C|z|.
  Proof.
    intro z. rewrite Cnorm_IRC_Rabs.
    apply Rabs_right.
    apply Rle_ge; apply Cnorm_pos.
  Qed.

|1| = 1
  Lemma Cnorm_C1 : C|C1| = R1.
  Proof.
    replace C1 with (IRC R1) by trivial;
      rewrite Cnorm_IRC_Rabs; exact Rabs_R1.
  Qed.

Rabs |z| = |z|
  Lemma Rabs_Cnorm : forall z : C, R| C|z| | = C|z|.
  Proof. intro z; apply Rabs_right; apply Rle_ge; apply Cnorm_pos. Qed.

|a| <= |(a,b)|
  Lemma Cre_le_Cnorm : forall z : C, R|z.a| <= C|z|.
  Proof.
    Csimpl. unfold Cnorm,Cnorm2; simpl.
    destruct (Aeqdec b R0).
    - subst. autorewrite with R. lra.
    - apply Rle_trans with (sqrt (a * a)).
      autorewrite with R. lra.
      apply sqrt_le_1_alt. ra.
  Qed.

|b| <= |(a,b)|
  Lemma Cim_le_Cnorm : forall z : C, R|z.b| <= C|z|.
  Proof.
    Csimpl. unfold Cnorm,Cnorm2; simpl.
    destruct (Aeqdec a R0).
    - subst. autorewrite with R. lra.
    - apply Rle_trans with (sqrt (b * b)).
      autorewrite with R. lra.
      apply sqrt_le_1_alt. ra.
  Qed.

|(a,b)| <= |a| + |b|
  Lemma Cnorm_le_Cre_Cim : forall z : C, C|z| <= R|z.a| + R|z.b|.
  Proof. Csimpl. unfold Cnorm, Cnorm2; simpl. apply basic_ineq1. Qed.

End Cnorm.

Notation "C| z |" := (Cnorm z) : C_scope.

Hint Resolve C0_norm_R0 : complex.

Addition of complex numbers

Section Cadd.
  Definition Cadd (z1 : C) (z2 : C) : C := (z1.a + z2.a) +i (z1.b + z2.b).
  Infix "+" := Cadd : C_scope.

  Lemma Cadd_spec : forall z1 z2 : C, (z1+z2).a = (z1.a+z2.a)%R /\ (z1+z2).b = (z1.b+z2.b)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Cre_add : forall z1 z2, Cre (z1 + z2) = (Cre z1 + Cre z2)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Cim_add : forall z1 z2, Cim (z1 + z2) = (Cim z1 + Cim z2)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Cadd_comm : forall z1 z2 : C, z1 + z2 = z2 + z1.
  Proof. Ceq. Qed.

  Lemma Cadd_assoc : forall a b c : C, a + b + c = a + (b + c).
  Proof. Ceq. Qed.

  Lemma Cadd_0_l : forall z : C, 0 + z = z.
  Proof. Ceq. Qed.

  Lemma Cadd_0_r : forall z : C, z + 0 = z.
  Proof. Ceq. Qed.

End Cadd.

Infix "+" := Cadd : C_scope.

Hint Resolve Cadd_comm : complex.
Hint Resolve Cadd_assoc : complex.
Hint Resolve Cadd_0_l : complex.
Hint Resolve Cadd_0_r : complex.

Opposition of complex numbers

Section Copp.

  Definition Copp (z : C) :C := (-z.a) +i (-z.b).
  Notation "- z" := (Copp z) : C_scope.

  Lemma Cre_opp : forall z, Cre (-z) = (- Cre z)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Cim_opp : forall z, Cim (-z) = (- Cim z)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Copp_opp : forall z, --z = z.
  Proof. Ceq. Qed.

  Lemma Cadd_opp_l : forall z : C, - z + z = 0.
  Proof. Ceq. Qed.

  Lemma Cadd_opp_r : forall z : C, z + - z = 0.
  Proof. Ceq. Qed.

|-z| = |z|
  Lemma Cnorm_opp : forall z : C, C| -z| = C|z|.
  Proof.
    intros z; unfold Cnorm, Cnorm2; destruct z as (a,b).
    simpl; replace (a * a + b * b)%R with (- a * - a + - b * - b)%R by field;
      reflexivity.
  Qed.

End Copp.

Notation "- z" := (Copp z) : C_scope.

Hint Resolve Copp_opp : complex.
Hint Resolve Cadd_opp_l : complex.
Hint Resolve Cadd_opp_r : complex.

Subtraction of complex numbers

Section Csub.

  Definition Csub (c1 c2 : C) : C := c1 + - c2.
  Infix "-" := Csub : C_scope.

  Lemma Cre_sub : forall z1 z2, Cre (z1 - z2) = (Cre z1 - Cre z2)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Cim_sub : forall z1 z2, Cim (z1 - z2) = (Cim z1 - Cim z2)%R.
  Proof. Csimpl. auto. Qed.

  Lemma Copp_add_distr : forall z1 z2, - (z1 + z2) = -z1 - z2.
  Proof. Ceq. Qed.

  Lemma Copp_sub_distr : forall z1 z2, - (z1 - z2) = - z1 + z2.
  Proof. Ceq. Qed.

  Lemma Csub_antisym : forall z1 z2, z1 - z2 = - (z2 - z1).
  Proof. Ceq. Qed.

|z1-z2| = |z2-z1|
  Lemma Cnorm_sub_sym : forall z1 z2, C|z1 - z2| = C|z2 - z1|.
  Proof.
    intros; rewrite Csub_antisym; rewrite Cnorm_opp; reflexivity.
  Qed.

End Csub.

Infix "-" := Csub : C_scope.

Hint Resolve Copp_add_distr : complex.
Hint Resolve Copp_sub_distr : complex.
Hint Resolve Csub_antisym : complex.

Scalar multiplication of complex numbers

Section Ccmul.

scalar multiplication
  Definition Ccmul (k : R) (z : C) : C := (k * z.a) +i (k * z.b).
  Infix "\.*" := Ccmul: C_scope.

  Lemma Cre_cmul : forall z k, (Cre (k \.* z) = k * Cre z)%R.
  Proof. intros (a,b) k; auto. Qed.

  Lemma Cim_cmul : forall z k, (Cim (k \.* z) = k * Cim z)%R.
  Proof. intros (a,b) k; auto. Qed.

  Lemma Ccmul_1 : forall z : C, 1 \.* z = z.
  Proof. Ceq. Qed.

  Lemma Ccmul_add_distr_l : forall k z1 z2, k \.* (z1 + z2) = k \.* z1 + k \.* z2.
  Proof. Ceq. Qed.

  Lemma Ccmul_add_distr_r : forall k1 k2 z, (k1 + k2)%R \.* z = k1 \.* z + k2 \.* z.
  Proof. Ceq. Qed.

  Lemma Ccmul_mul_swap_l : forall k1 k2 z, (k1 * k2)%R \.* z = k1 \.* (k2 \.* z).
  Proof. Ceq. Qed.

|k * z| = |k| * |z|
  Lemma Cnorm_cmul : forall k z, C|k \.* z| = (R|k| * (C|z|))%R.
  Proof.
    intros k (a,b). unfold Cnorm; unfold Cnorm2; simpl.
    rewrite <- sqrt_Rsqr_abs. rewrite <- sqrt_mult; ra.
    apply Rsqr_inj; ra. autorewrite with R. rewrite ?Rsqr_sqrt; ra.
  Qed.

End Ccmul.
Infix "\.*" := Ccmul: C_scope.

Multiplication of complex numbers

Section Cmul.

  Definition Cmul (z1 : C) (z2 : C) : C :=
    (z1.a * z2.a - z1.b * z2.b) +i (z1.a * z2.b + z2.a * z1.b).
  Infix "*" := Cmul : C_scope.

  Lemma Cmul_comm : forall z1 z2 : C, z1 * z2 = z2 * z1.
  Proof. Ceq. Qed.

  Lemma Cmul_assoc : forall z1 z2 z3 : C, (z1 * z2) * z3 = z1 * (z2 * z3).
  Proof. Ceq. Qed.

  Lemma Cmul_0_l : forall z : C, 0 * z = 0 .
  Proof. Ceq. Qed.

  Lemma Cmul_0_r : forall z : C, z * 0 = 0 .
  Proof. Ceq. Qed.

  Lemma Cmul_1_l : forall z : C, 1 * z = z .
  Proof. Ceq. Qed.

  Lemma Cmul_1_r : forall z : C, z * 1 = z .
  Proof. Ceq. Qed.

  Lemma Cmul_add_distr_l : forall z1 z2 z3 : C, z1 * (z2 + z3) = z1 * z2 + z1 * z3.
  Proof. Ceq. Qed.

  Lemma Cmul_add_distr_r : forall z1 z2 z3 : C, (z1 + z2) * z3= z1 * z3 + z2 * z3.
  Proof. Ceq. Qed.

|z1 * z2| = |z1| * |z2|
  Lemma Cnorm_Cmult : forall z1 z2, C|z1 * z2| = (C|z1| * C|z2|)%R.
  Proof.
    intros (a,b) (c,d). cbv.
    rewrite <- sqrt_mult; ra.
    apply Rsqr_inj; ra. autorewrite with R. rewrite ?Rsqr_sqrt; ra.
  Qed.

End Cmul.

Infix "*" := Cmul : C_scope.

Hint Resolve Cmul_comm : complex.
Hint Resolve Cmul_assoc : complex.
Hint Resolve Cmul_1_l : complex.
Hint Resolve Cmul_1_r : complex.
Hint Resolve Cmul_add_distr_l : complex.
Hint Resolve Cmul_add_distr_r : complex.

Lemma Complex_ring : ring_theory C0 C1 Cadd Cmul Csub Copp eq.
Proof.
  constructor; intros; auto.
  apply Cadd_0_l. apply Cadd_comm. rewrite Cadd_assoc; auto.
  apply Cmul_1_l. apply Cmul_comm. rewrite Cmul_assoc; auto.
  apply Cmul_add_distr_r. apply Cadd_opp_r.
Qed.

Add Ring Complex_ring_inst : Complex_ring.

Power on C

Section Cpow.

  Fixpoint Cpow (z : C) (n : nat) {struct n} : C :=
    match n with
    | 0%nat => 1
    | S m => z * (Cpow z m)
    end.

  Infix "^" := Cpow : C_scope.

  Lemma Cpow_0 : forall z, z ^ 0 = 1.
  Proof. auto. Qed.

  Lemma C0_pow : forall n, (0 < n)%nat -> 0 ^ n = 0.
  Proof.
    induction n; intros; auto. lia.
    destruct (Aeqdec n 0%nat).
    - rewrite e. Ceq.
    - simpl. rewrite IHn. Ceq. lia.
  Qed.

  Lemma Cpow_S : forall (z : C) (n : nat), z ^ (S n) = z ^ n * z.
  Proof. intros. simpl. auto with complex. Qed.

  Lemma Cpow_add : forall (z : C) (n m : nat), z ^ (n + m) = z ^ n * z ^ m.
  Proof.
    intros z n. induction n; intros; cbn.
    - auto with complex.
    - rewrite IHn. auto with complex.
  Qed.

  Lemma Cpow_mul : forall z n m, z ^ (n * m) = (z ^ n) ^ m.
  Proof.
    intros z n m. revert n. induction m; intros; cbn.
    - rewrite Nat.mul_0_r. easy.
    - rewrite <- IHm. rewrite <- Cpow_add. f_equal. lia.
  Qed.

  Lemma Cpow_mul_distr_l : forall z1 z2 n, (z1 * z2) ^ n = z1 ^ n * z2 ^ n.
  Proof.
    intros z1 z2 n. induction n; cbn; auto with complex.
    rewrite IHn.
    rewrite ?Cmul_assoc. f_equal.
    rewrite <- ?Cmul_assoc. f_equal.
    auto with complex.
  Qed.

  Lemma Cpow_IRC : forall z n, IRC z ^ n = IRC (z ^ n).
  Proof. intros z n ; induction n; auto. simpl. rewrite IHn. Ceq. Qed.

|z^n| = |z|^n
  Lemma Cnorm_pow : forall z n, C|z ^ n| = ((C|z|) ^ n)%R.
  Proof.
    intros z n; induction n.
    simpl; apply Cnorm_C1.
    simpl; rewrite Cnorm_Cmult, IHn; reflexivity.
  Qed.

End Cpow.

Inversion of complex numbers

Section Cinv.

  Definition Cinv (z : C) : C :=
    (z.a / C2|z|) +i (-z.b / C2|z|).
  Notation "/ z" := (Cinv z) : C_scope.

  Lemma Cinv_rew : forall a b : R,
      (a +i b) <> 0 -> /(a +i b) = (/ (a*a + b*b)) \.* (a +i - b)%R.
  Proof. Ceq. cbv; lra. cbv; lra. Qed.

  Lemma Cmul_inv_l : forall z : C, z <> 0 -> / z * z = 1.
  Proof.
    Ceq. cbv. field. apply Rplus2_sqr_neq0. apply Cneq_iff in H. auto.
  Qed.

  Lemma Cmul_inv_r : forall z:C, z <> C0 -> z * /z = 1.
  Proof. intros. rewrite Cmul_comm. apply Cmul_inv_l. auto. Qed.

A Coq-version-issue about inv_sqrt and sqrt_inv
  Section coq_version_issue.

There are two similiar lemmas: inv_sqrt and sqrt_inv


    Axiom sqrt_inv : forall x : R, sqrt (/ x) = (/ sqrt x)%R.

  End coq_version_issue.

z <> 0 -> |/z| = / |z|
  Lemma Cnorm_inv : forall z : C, z <> 0 -> C| /z | = (/(C|z|))%R.
  Proof.
    intros (a,b) H. cbv.
    assert (0 < a * a + b * b).
    { apply Cneq_iff in H; simpl in H. destruct H; ra. }
    rewrite <- sqrt_inv; ra.
    apply Rsqr_inj; ra. autorewrite with R. rewrite !Rsqr_sqrt; ra.
    field. lra.
  Qed.

z <> 0 -> (/z).a = z.a / C2|z|
  Lemma Cre_inv (z : C) : z <> 0 -> (/ z).a = ((z.a) / C2|z |)%R.
  Proof. auto. Qed.

z <> 0 -> (/z).b = -z.b / C2|z|
  Lemma Cim_inv_neq0 (z : C) : z <> 0 -> (/ z).b = (-z.b / C2|z|)%R.
  Proof. auto. Qed.

End Cinv.

Notation "/ z" := (Cinv z) : C_scope.

Hint Resolve Cmul_inv_l : complex.
Hint Resolve Cmul_inv_r : complex.

Division of complex numbers

Section Cdiv.

  Definition Cdiv (c1 c2 : C) : C := c1 * / c2.
  Infix "/" := Cdiv : C_scope.

z <> 0 -> /z = 1/z
  Lemma Cinv_eq_div (z : C) : z <> 0 -> (/z) = (1/z).
  Proof. Ceq. Qed.

End Cdiv.
Infix "/" := Cdiv : C_scope.

Lemma Complex_field : field_theory C0 C1 Cadd Cmul Csub Copp Cdiv Cinv eq.
Proof.
  constructor; intros; auto with complex.
  apply Complex_ring.
Qed.

Add Field Complex_field_inst : Complex_field.

Instance of classes which defined in HierarchySetoid






Global Instance ARing_C : ARing Cadd 0 Copp Cmul 1.
Proof. split_intro; intros; subst; try ring. Qed.

Global Instance Field_C : Field Cadd 0 Copp Cmul 1 Cinv.
Proof.
  constructor. apply ARing_C.
  intros. field. auto. apply C1_neq_C0.
Qed.

Conjugate of complex numbers

Section Cconj.

  Definition Cconj (z : C) : C := (z.a) +i (-z.b).
  Notation "z '" := (Cconj z) (at level 20) : C_scope.

  Lemma Cconj_add : forall z1 z2 : C, (z1 + z2) ' = z1 ' + z2 '.
  Proof. Ceq. Qed.

  Lemma Cadd_conj : forall z : C, z + z ' = (2 * z.a) +i 0.
  Proof. Ceq. Qed.

  Lemma Cconj_sub : forall z1 z2 : C, (z1 - z2)' = z1 ' - z2 '.
  Proof. Ceq. Qed.

  Lemma Csub_conj : forall z : C, z - z ' = 0 +i (2 * z.b).
  Proof. Ceq. Qed.

  Lemma Cconj_mul : forall z1 z2, (z1 * z2)' = z1 ' * z2 '.
  Proof. Ceq. Qed.

|z'| = |z|
  Lemma Cnorm_conj_compat : forall z, C|z '| = C|z|.
  Proof.
    intros z; unfold Cconj, Cnorm, Cnorm2; simpl; destruct z;
      rewrite Rmult_opp_opp; reflexivity.
  Qed.

End Cconj.

Notation "z '" := (Cconj z) (at level 20) : C_scope.

Triangle Inequalities

Section triangle_ineq.

|z1 + z2| <= |z1| + |z2|
  Lemma Cnorm_triang : forall z1 z2 : C, C|z1 + z2| <= (C|z1| + C|z2|)%R.
  Proof.
    intros (a,b) (c,d). cbv.
    apply Rsqr_incr_0_var; ra. ring_simplify.
    autorewrite with R. rewrite ?Rsqr_sqrt; ra.
    ring_simplify.
    replace (a ^ 2 + 2 * a * c + c ^ 2 + b ^ 2 + 2 * b * d + d ^ 2)%R
      with (a ^ 2 + c ^ 2 + b ^ 2 + d ^ 2 + 2 * a * c + 2 * b * d)%R by ring.
    rewrite ?Rplus_assoc. repeat apply Rplus_le_compat_l.
    replace (2 * a * c + 2 * b * d)%R with (2 * (a * c + b * d))%R by ring.
    rewrite ?Rmult_assoc. apply Rmult_le_compat_l; try lra.
    rewrite <- sqrt_mult; ra.
    apply basic_ineq2.
  Qed.

Rabs (|z1| - |z2|) <= |z1 - z2|
  Lemma Cnorm_triang_rev : forall z1 z2 : C, R| C|z1| - C|z2| | <= C|z1 - z2|.
  Proof.
    intros z1 z2.
    assert (H1 : C|z1 - z2 + z2| <= C|z1 - z2| + C|z2|) by (apply Cnorm_triang).
    assert (H2 : C|z2 - z1 + z1| <= C|z2 - z1| + C|z1|) by (apply Cnorm_triang).
    assert (H3 : forall a b, a = a - b + b). Ceq.
    unfold Rabs; case Rcase_abs; intro H; ring_simplify.
    rewrite <- H3 in H2. apply Rminus_le; apply Rle_minus in H2.
    ring_simplify in H2. rewrite Cnorm_sub_sym.
    replace ( -Cnorm z1 + Cnorm z2 - Cnorm (z2 - z1)%C)%R with
      (Cnorm z2 - Cnorm (z2 - z1)%C - Cnorm z1)%R by field; apply H2.
    rewrite <- H3 in H1; apply Rminus_le; apply Rle_minus in H1.
    replace (Cnorm z1 - Cnorm z2 - Cnorm (z1 - z2)%C)%R with
      (Cnorm z1 - (Cnorm(z1 - z2)%C + Cnorm z2))%R by field; apply H1.
  Qed.

|z1| - |z2| <= |z1 - z2|
  Lemma Cnorm_triang_rev_l : forall z1 z2 : C, C|z1| - C|z2| <= C|z1 - z2|.
  Proof.
    intros z1 z2; apply Rle_trans with (Rabs (Cnorm z1 - Cnorm z2));
      [apply RRle_abs |
        apply Cnorm_triang_rev].
  Qed.

|z2| - |z1| <= |z1 - z2|
  Lemma Cnorm_triang_rev_r : forall z1 z2 : C, C|z2| - C|z1| <= C|z1 - z2|.
  Proof.
    intros z1 z2; apply Rle_trans with (Rabs (Cnorm z2 - Cnorm z1));
      [apply RRle_abs |
        rewrite Rabs_minus_sym; apply Cnorm_triang_rev].
  Qed.

End triangle_ineq.

1.2 Triangle Representation of Complex number (复数的三角表示)

1.2.1 Magnitude, Main argument and argument of complex number

(复数的模、主辐角和辐角)

Magnitude of complex number


Some inequalities about real part or imaginay part of a complex number

Lemma Cnorm_ge_AbsCre (z : C) : R|z.a| <= C|z|.
Proof. apply Cre_le_Cnorm. Qed.

Lemma Cnorm_ge_AbsCim (z : C) : R|z.b| <= C|z|.
Proof. apply Cim_le_Cnorm. Qed.

Lemma Cnorm_le_AbsCre_plus_AbsCim (z : C) :
  C|z| <= R|z.a| + R|z.b|.
Proof. apply Cnorm_le_Cre_Cim. Qed.

Main argument
Definition Carg (z : C) : R :=
  let x : R := Cre z in
  let y : R := Cim z in
  let r : R := atan (y / x) in
  let r1_pos : R := (PI / 2)%R in
  let r1_neg : R := (- r1_pos)%R in
  if (x =? 0)
  then (if y <? 0 then r1_neg else r1_pos)
  else (if x <? 0
        then (if y <? 0 then (r - PI)%R else (r + PI)%R)
        else r).

Notation "∠ z" := (Carg z) (at level 10) : C_scope.


Argument of a complex number
Definition is_CArg (z : C) (theta : R) : Prop := exists (k : Z),
    theta = (∠z + 2 * (IZR k) * PI)%R.

Because, every different arguments of a complex number must have same sine and cosine value, thus we should abtain same complex number. Therefore, we won't distinguish main argument and argument now.
Verify the definition of Carg (x > 0)
Lemma Carg_verify_xlt0 (x y : R) :
  x > 0 -> ∠(x +i y) = atan (y/x).
Proof.
  intros. unfold Carg. simpl.
  bdestruct (x =? 0); try lra.
  bdestruct (x <? 0); try lra.
Qed.

Verify the definition of Carg (x = 0, y > 0)
Lemma Carg_verify_xeq0_ygt0 (x y : R) :
  x = 0%R -> y > 0 -> ∠(x +i y) = (PI / 2)%R.
Proof.
  intros. unfold Carg. simpl.
  bdestruct (x =? 0); try lra.
  bdestruct (y <? 0); try lra.
Qed.

Verify the definition of Carg (x < 0, y >= 0)
Lemma Carg_verify_xlt0_yge0 (x y : R) :
  x < 0%R -> y >= 0 -> ∠(x +i y) = (atan (y/x) + PI)%R.
Proof.
  intros. unfold Carg. simpl.
  bdestruct (x =? 0); try lra.
  bdestruct (x <? 0); try lra.
  bdestruct (y <? 0); try lra.
Qed.

Verify the definition of Carg (x < 0, y < 0)
Lemma Carg_verify_xlt0_ylt0 (x y : R) :
  x < 0%R -> y < 0 -> ∠(x +i y) = (atan (y/x) - PI)%R.
Proof.
  intros. unfold Carg. simpl.
  bdestruct (x =? 0); try lra.
  bdestruct (x <? 0); try lra.
  bdestruct (y <? 0); try lra.
Qed.

Verify the definition of Carg (x = 0, y < 0)
Lemma Carg_verify_xeq0_ylt0 (x y : R) :
  x = 0%R -> y < 0 -> ∠(x +i y) = (- PI / 2)%R.
Proof.
  intros. unfold Carg. simpl.
  bdestruct (x =? 0); try lra.
  bdestruct (y <? 0); try lra.
Qed.

Note, this equation will be used in the proof about cos(∠ z) and sin(∠ z)
/(sqrt (1+(b/a)²)) = abs(a) / sqrt(a*a + b*b)
Lemma Rinv_Rsqrt_1_plus_Rsqr_a_div_b (a b : R) :
  a <> 0%R -> (/ (sqrt (1+(b/a)²)) = (Rabs a) / sqrt(a*a + b*b))%R.
Proof.
  intros.
  replace (1 + (b/a)²)%R with ((a*a + b*b) / (a*a))%R.
  - rewrite sqrt_div_alt; ra.
    replace (sqrt (a * a)%R) with R|a|.
    + field. split; ra.
      autorewrite with R. auto with R.
    + autorewrite with R. auto.
  - cbv. field. auto.
Qed.

solve "0 < a * a" on real number
Ltac tac_Rsqr_gt0 :=
  match goal with
  
  | H1 : ?a < 0%R |- 0 < ?a * ?a =>
      apply Rsqr_pos_lt
      ; apply Rlt_not_eq
      ; assumption
  
  | H1 : ?a <> 0%R |- 0 < ?a * ?a =>
      apply Rsqr_pos_lt
      ; assumption
  | |- _ => idtac "no match"
  end.

solve "0 < a*a + b*b" on real number
Ltac tac_Rplus_Rsqr_Rsqr_gt0 :=
  match goal with
  
  | H1:?a<0 , H2:?b<0 |- 0 < ?a*?a + ?b*?b =>
      apply Rplus_lt_0_compat
      ;tac_Rsqr_gt0
  
  | H1:?a<0 , H2:?b>=0 |- 0 < ?a*?a + ?b*?b =>
      apply Rplus_lt_le_0_compat
      ;[tac_Rsqr_gt0 |
         apply Rle_0_sqr]
  
  | H1:?a>=0 |- 0 < ?a*?a + ?b*?b =>
      apply Rplus_lt_le_0_compat
      ;[tac_Rsqr_gt0 |
         apply Rle_0_sqr]
  | |- _ => idtac "no matching"
  end.

nonzero complex number, the cosine of its main argument equal to real part divide magnitude (主辐角的余弦等于实部除以模长)
Lemma cos_Carg_neq0 (z : C) : z <> 0 -> cos(∠z) = ((Cre z) / C|z|)%R.
Proof.
  intros. unfold Carg. destruct z as (a,b); simpl.
  bdestruct (a =? 0).
  - destruct (b <? 0).
    + subst. rewrite cos_neg. rewrite cos_PI2.
      unfold Rdiv; rewrite Rmult_0_l; auto.
    + rewrite cos_PI2. subst. unfold Rdiv; rewrite Rmult_0_l; auto.
  - bdestruct (a <? 0).
    + bdestruct (b <? 0).
      * rewrite cos_minus,?cos_PI,?sin_PI; ring_simplify. rewrite cos_atan.
        unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_a_div_b; auto.
        replace (Rabs a) with (-a)%R.
        unfold Cnorm, Cnorm2. simpl. field.
        apply not_eq_sym. apply Rlt_not_eq. apply sqrt_lt_R0. ra.
        rewrite Rabs_left; auto.
      * rewrite cos_plus,?sin_PI,?cos_PI; ring_simplify. rewrite cos_atan.
        unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_a_div_b; auto.
        replace (Rabs a) with (-a)%R.
        unfold Cnorm, Cnorm2. simpl. field.
        apply not_eq_sym. apply Rlt_not_eq. apply sqrt_lt_R0. ra.
        rewrite Rabs_left; auto.
    + rewrite cos_atan.
      unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_a_div_b; auto.
      replace (Rabs a) with a.
      unfold Cnorm, Cnorm2. simpl. field.
      apply not_eq_sym. apply Rlt_not_eq. apply sqrt_lt_R0. ra.
      rewrite Rabs_right; auto. ra.
Qed.

nonzero complex number, the sine of its main argument equal to imaginary part divide magnitude (主辐角的正弦等于虚部除以模长)
Lemma sin_Carg_neq0 (z : C) : z <> 0 -> sin(∠z) = ((Cim z) / C|z|)%R.
Proof.
  intros. unfold Carg. destruct z as (a,b); simpl.
  bdestruct (a =? 0).
  - bdestruct (b <? 0).
    + subst. rewrite sin_neg. rewrite sin_PI2.
      unfold Cnorm. unfold Cnorm2. simpl. ring_simplify (0*0+b*b)%R.
      rewrite <- Rsqr_pow2. rewrite sqrt_Rsqr_abs. rewrite Rabs_left; auto.
      field. lra.
    + rewrite sin_PI2.
      unfold Cnorm. unfold Cnorm2. simpl. subst. ring_simplify (0*0+b*b)%R.
      rewrite <- Rsqr_pow2. rewrite sqrt_Rsqr_abs. rewrite Rabs_right; auto.
      field. intro. subst. destruct H. auto. ra.
  - bdestruct (a <? 0).
    + destruct (b <? 0).
      * rewrite sin_minus,?sin_PI,?cos_PI. ring_simplify.
        rewrite sin_atan.
        unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_a_div_b; auto.
        replace (Rabs a) with (-a)%R.
        unfold Cnorm, Cnorm2. simpl. field. split; auto.
        apply not_eq_sym. apply Rlt_not_eq. apply sqrt_lt_R0. ra.
        rewrite Rabs_left; auto.
      * rewrite sin_plus,?sin_PI,?cos_PI. ring_simplify.
        rewrite sin_atan.
        unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_a_div_b; auto.
        replace (Rabs a) with (-a)%R.
        unfold Cnorm, Cnorm2. simpl. field. split; auto.
        apply not_eq_sym. apply Rlt_not_eq. apply sqrt_lt_R0. ra.
        rewrite Rabs_left; auto.
    + rewrite sin_atan.
      unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_a_div_b; auto.
      replace (Rabs a) with a.
      unfold Cnorm, Cnorm2. simpl. field. split; auto.
      apply not_eq_sym. apply Rlt_not_eq. apply sqrt_lt_R0. ra.
      rewrite Rabs_right; auto. ra.
Qed.

非零复数的主辐角的正切表达式

Axiom tan_sin_cos : forall (r : R), tan r = (sin r / cos r)%R.

Lemma tan_Carg_neq0 (z : C) : z <> 0 -> tan(∠z) = ((Cim z) / Cre z)%R.
Proof.
  intros.
  rewrite tan_sin_cos.
  rewrite cos_Carg_neq0, sin_Carg_neq0; auto. field. split.
Abort.
非零复数实部等于模乘以辐角余弦
Lemma Cre_eq_Cnorm_mul_cos_Carg (z : C) : z <> 0 ->
                                          Cre z = (C|z| * cos(∠z))%R.
Proof.
  intros. rewrite cos_Carg_neq0; auto. field. apply Cnorm_neq0_iff_neq0 in H; auto.
Qed.

非零复数虚部等于模乘以辐角正弦
Lemma Cim_eq_Cnorm_mul_sin_Carg (z : C) : z <> 0 ->
                                          Cim z = (C|z| * sin(∠z))%R.
Proof.
  intros. rewrite sin_Carg_neq0; auto. field. apply Cnorm_neq0_iff_neq0; auto.
Qed.

非零复数，(相等 <-> 模长和辐角相等)
Lemma Cneq0_eq_iff_Cnorm_Carg (z1 z2 : C) (H1 : z1 <> 0) (H2 : z2 <> 0) :
  z1 = z2 <-> (C|z1| = C|z2|) /\ (∠ z1 = ∠ z2).
Proof.
  split; intros. subst; auto.
  destruct H. apply Ceq_iff.
  repeat rewrite Cre_eq_Cnorm_mul_cos_Carg, Cim_eq_Cnorm_mul_sin_Carg; auto.
  rewrite H,H0. auto.
Qed.

1.2.2 复数模的三角不等式


Lemma CnormCadd_le_CaddCnorm (z1 z2 : C) : C|z1+z2| <= C|z1| + C|z2|.
Proof. apply Cnorm_triang. Qed.

Lemma CnormCadd_ge_AbsSubCnorm (z1 z2 : C) : R| C|z1| - C|z2| | <= C|z1+z2|.
Proof.
Admitted.

Lemma CnormCsub_le_CaddCnorm (z1 z2 : C) : C|z1-z2| <= C|z1| + C|z2|.
Proof.
Admitted.

Lemma CnormCsub_ge_AbsSubCnorm (z1 z2 : C) : R| C|z1| - C|z2| | <= C|z1-z2|.
Proof. apply Cnorm_triang_rev. Qed.

1.2.3 复数的三角表示

复数三角表示的定义
Definition Ctrigo (r θ : R) : C := Ccmul r (cos θ +i sin θ).

复数三角表示的重写形式
Definition Ctrigo_rew (z : C) : C := Ctrigo C|z| (∠ z).

任意正整数r和实数θ，则存在一个复数z的三角表示如下
Lemma Ctrigo_r_theta_existsC (r θ : R) (k : Z) : r > 0 ->
                                                  {z : C | z = Ccmul r (cos θ +i sin θ)}.
Proof.
  intros. exists (Ctrigo r θ). auto.
Qed.

复数的三角表示有无穷多种选择
Lemma Ctrigo_many : forall (r θ : R) (k : Z),
    let θ' : R := (θ + 2 * (IZR k) * PI)%R in
    Ctrigo r θ = Ccmul r (cos θ' +i sin θ').
Proof.
  intros. unfold Ctrigo, θ'. rewrite cos_period_Z, sin_period_Z.
  auto.
Qed.

例 1.2。这类题目证明还是很繁琐，因实数构造问题 这个例子也看出了大量的自动化的需求，比如带有 sqrt, cos, sin 等的运算， 比如 Rsqr 2 与 sqr 2 的问题（它们混在一起）。 能将这个证明简化到几步完成，而且还比较通用，也是个不错的课题。

Fact ex_1_2_ans1_aux1 (x : R) (k : Z) : (7/8 <= x <= 7/4)%R ->
                                        (x = IZR k * PI + PI / 2)%R -> k = Z0.
Proof.
  intros. subst.
  destruct H as [H1 H2].
  assert (0 <= k)%Z.
  { apply le_IZR.
    Fail lra.     assert (PI <= 3.15).

Admitted.

Example ex_1_2_ans1 : 1 +i 1 = Ctrigo (sqrt 2) (PI/4)%R.
Proof.
Abort.

Example ex_1_2_ans2 : 1 +i 1 = Ctrigo (sqrt 2) (PI/4)%R.
Abort.

非零复数的共轭的三角表示
Lemma Ctrigo_Cconj (z : C) : z <> 0 -> Cconj z = Ctrigo C|z| (-∠z)%R.
Proof.
  intros; unfold Cconj, Ctrigo.
  rewrite cos_neg, sin_neg, ?cos_Carg_neq0, ?sin_Carg_neq0; auto.
  unfold Ccmul. simpl. f_equal; field; apply Cnorm_neq0_iff_neq0; auto.
Qed.

1/z的三角表示
Definition Ctrigo_Cinv (z : C) (k : Z) : C :=
  let r := C|z| in
  let θ := Carg z in
  Ctrigo (/r)%R (-θ)%R.

/z 的三角表示公式正确
Lemma Ctrigo_Cinv_ok (z : C) (k : Z) : z <> 0 ->
                                       /z = Ctrigo_Cinv z k.
Proof.
  intros.   intros; destruct z as (a,b). rewrite Cinv_rew; auto.
  remember ((a^2)+(b^2))%R as r.
  unfold Ctrigo_Cinv.
Admitted.

1.2.4 用复数的三角表示作乘除法

复数乘法运算的三角表示版本
Definition CmultTrigo (z1 z2 : C) : C :=
  Ctrigo (C|z1| * C|z2|)%R (∠ z1 + ∠ z2)%R.

复数除法运算的三角表示版本。注意，z2 <> 0
Definition CdivTrigo (z1 z2 : C) : C :=
  Ctrigo (C|z1| / C|z2|)%R (∠ z1 - ∠ z2)%R.

复数乘法三角表示版本与常规乘法定义等价
Lemma CmultTrigo_eq_Cmult (z1 z2 : C) :
  z1 * z2 = CmultTrigo z1 z2.
Proof.
  unfold CmultTrigo, Ctrigo.
  rewrite cos_plus, sin_plus. unfold Ccmul.
  destruct (Aeqdec z1 0), (Aeqdec z2 0); subst; Ceq;
    repeat rewrite Cnorm_C0_eq0; autorewrite with R; auto.




Abort.

除数非零时，复数除法三角表示版本与常规除法定义等价
Lemma CdivTrigo_eq_Cdiv (z1 z2 : C) : z2 <> 0 ->
                                      z1 / z2 = CdivTrigo z1 z2.
Proof.
  intros. unfold CdivTrigo, Ctrigo.
  rewrite cos_minus, sin_minus. unfold Ccmul. simpl.
  destruct (Aeqdec z1 0), (Aeqdec z2 0);
    subst; rewrite ?Cnorm_C0_eq0; unfold Cdiv.
  - destruct H. auto.
Abort.

1.2.5 复数的乘方与开方

复数乘方运算的三角表示版本
Definition CpowTrigo (z : C) (n : nat) : C :=
  Ctrigo (C|z| ^ n)%R ((INR n) * (∠ z))%R.

复数开方运算的三角表示版本。注意，z2 <> 0，共有 n 个根（n个不同的主辐角）
Definition CnrootTrigo (z : C) (n : nat) (k : nat) : C :=
  Ctrigo ( / (C|z| ^ n))%R ((∠ z + 2 * (INR k) * PI) / (INR n))%R.

复数乘方三角版本的性质
幂为 0
Lemma CpowTrigo_0 (z : C) : CpowTrigo z 0 = 1.
Proof.
  unfold CpowTrigo. simpl. unfold Ctrigo.
  rewrite Rmult_0_l. rewrite cos_0, sin_0. compute. f_equal; ring.
Qed.

幂为 S n
Lemma CpowTrigo_S (z : C) (n : nat) : CpowTrigo z (S n) = z * (CpowTrigo z n).
Proof.
  unfold CpowTrigo.
Admitted.

复数乘方三角表示版本与常规乘方定义等价
Lemma CpowTrigo_eq_Cmult (z : C) (n : nat) :
  Cpow z n = CpowTrigo z n.
Proof.
  generalize dependent z. induction n; intros; simpl.
  - rewrite CpowTrigo_0; auto.
  - rewrite CpowTrigo_S. f_equal. auto.
Qed.

复数开方运算的三角表示版本 与 复数乘方三角表示版本的互逆性