# Library Coqtail.Complex.Cbase

Require Export Cdefinitions.

# Complex to real lemmas.

Lemma Cproj_right : z1 : C, (Cre z1, Cim z1) = z1.
Proof.
intros z1 ; elim z1 ; reflexivity.
Qed.

Lemma Ceq : z1 z2 : C, Cre z1 = Cre z2 Cim z1 = Cim z2 z1 = z2.
Proof.
intros z1 z2 ; split ; intro H.
rewrite <- Cproj_right ; symmetry ; rewrite <- Cproj_right ; destruct H as (H, H0) ;
rewrite H ; rewrite H0 ; reflexivity.
split; rewrite H; reflexivity.
Qed.

Simple tactics using the projections

Ltac CusingR_simpl :=
rewrite <- Ceq ; simpl ; split.

Ltac CusingR_rec := match goal with
| id:C |- _destruct id ; try CusingR_rec
end.

Ltac CusingR := intros; try CusingR_rec ; apply (proj1 (Ceq _ _)) ; split ; simpl ; auto with real.

Ltac CusingR_f := CusingR ; field.

# Field Lemmas.

Lemma C0_neq_R0_neq : z, z 0 (Cre z 0%R Cim z 0%R).
Proof.
intro z ; split ; intro H.
destruct z as (a,b) ; case (Req_or_neq a) ; case (Req_or_neq b) ; intros Ha Hb.
elim H ; rewrite Ha, Hb ; reflexivity.
right ; intuition.
left ; intuition.
left ; intuition.
intro Hf ; destruct H ; apply H ; rewrite Hf ; intuition.
Qed.
Hint Resolve C0_neq_R0_neq : complex.

Lemma HintC0_neq_R0_neq : z, (Cre z 0%R Cim z 0%R) → z 0.
Proof.
intros z. apply <- C0_neq_R0_neq.
Qed.
Hint Resolve HintC0_neq_R0_neq : complex.

Lemma C0_norm_R0 : z, z = 0 Cnorm_sqr z = 0%R.
Proof.
intro z ; unfold Cnorm_sqr ; split ; intro Hrew.
destruct (proj2 (Ceq z 0) Hrew) as (H1, H2) ; destruct z as (r1,r2);
simpl in × ; rewrite H1 ; rewrite H2 ; field.
apply (proj1 (Ceq _ _)) ; split.
apply Rsqr_0_uniq.
apply Rplus_eq_0_l with ((Cim z)%R ; [apply Rle_0_sqr | apply Rle_0_sqr |].
unfold Rsqr.
assumption.
destruct z as (a,b) ; intuition. simpl in ×.
apply Rsqr_0_uniq.
apply Rplus_eq_0_l with ((a)%R ; [apply Rle_0_sqr | apply Rle_0_sqr |].
unfold Rsqr.
rewrite Rplus_comm.
assumption.
Qed.
Hint Resolve C0_norm_R0 : complex.

Lemma HC0_norm_R0 : z, Cnorm_sqr z = 0%Rz = 0.
Proof.
intros. apply <- C0_norm_R0. assumption.
Qed.
Hint Resolve HC0_norm_R0 : complex.

Cre / Cim compatibility with simple operators

Lemma Cre_simpl : (a b : R), Cre (a +i b) = a.
Proof.
intros ; reflexivity.
Qed.

Lemma Cim_simpl : (a b : R), Cim (a +i b) = b.
Proof.
intros ; reflexivity.
Qed.

Lemma Cre_opp_compat : z, (- Cre z = Cre (-z))%R.
Proof.
intro z ; destruct z ; reflexivity.
Qed.

Lemma Cim_opp_compat : z, (- Cim z = Cim (-z))%R.
intro z ; destruct z ; reflexivity.
Qed.

Lemma Cre_add_compat : z1 z2, (Cre z1 + Cre z2 = Cre (z1 + z2))%R.
Proof.
intros z1 z2 ; destruct z1 ; destruct z2 ; reflexivity.
Qed.

Lemma Cim_add_compat : z1 z2, (Cim z1 + Cim z2 = Cim (z1 + z2))%R.
Proof.
intros z1 z2 ; destruct z1 ; destruct z2 ; reflexivity.
Qed.

Lemma Cre_minus_compat : z1 z2, (Cre z1 - Cre z2 = Cre (z1 - z2))%R.
Proof.
intros z1 z2 ; destruct z1 ; destruct z2 ; reflexivity.
Qed.

Lemma Cim_minus_compat : z1 z2, (Cim z1 - Cim z2 = Cim (z1 - z2))%R.
Proof.
intros z1 z2 ; destruct z1 ; destruct z2 ; reflexivity.
Qed.

Lemma Cre_scal_compat : z l, (Cre (l `* z) = l × Cre z)%R.
Proof.
intros z l ; destruct z ; reflexivity.
Qed.

Lemma Cim_scal_compat : z l, (Cim (l `* z) = l × Cim z)%R.
Proof.
intros z l ; destruct z ; reflexivity.
Qed.

Lemma Cre_eq_compat : z1 z2, z1 = z2Cre z1 = Cre z2.
Proof.
intros a b H ; rewrite H ; reflexivity.
Qed.

Lemma Cim_eq_compat : z1 z2, z1 = z2Cim z1 = Cim z2.
Proof.
intros a b H ; rewrite H ; reflexivity.
Qed.

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

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

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

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

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

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

Opposite

Lemma Copp_invol : z, --z = z.
Proof.
CusingR.
Qed.
Hint Resolve Copp_invol : complex.

Minus

Lemma Copp_add_distr : z z', - (z + z') = -z - z'.
Proof.
CusingR_f.
Qed.

Lemma Copp_minus_distr : z z', - (z - z') = - z + z'.
Proof.
CusingR_f.
Qed.
Hint Resolve Copp_minus_distr : complex.

Lemma Cminus_antisym : z z', (z - z') = - (z' - z).
Proof.
CusingR_f.
Qed.
Hint Resolve Cminus_antisym : complex.

Multiplication.
Lemma Cmult_comm : z1 z2 : C, z1 × z2 = z2 × z1.
Proof.
CusingR_f.
Qed.
Hint Resolve Cmult_comm : complex.

Lemma Cmult_assoc : z1 z2 z3 : C, z1 × z2 × z3 = z1 × (z2 × z3).
Proof.
CusingR_f.
Qed.
Hint Resolve Cmult_assoc : complex.

Lemma Cmult_1_l : z : C, 1 × z = z .
Proof.
CusingR_f.
Qed.
Hint Resolve Cmult_1_l : complex.

Lemma Cmult_1_r : z : C, z × 1= z .
Proof.
CusingR_f.
Qed.
Hint Resolve Cmult_1_r : complex.

Lemma Cinv_rew : a b : R, (a +i b) 0 → /(a +i b) = (/ (a^2 + b^2)) `* (a +i - b)%R.
Proof.
intros a b ; simpl.
destruct (C0_norm_R0 (a, b)).
CusingR_f ; intuition.
Qed.

Division/Inverse

Lemma Cinv_l : z : C, z C0/ z × z = 1.
Proof.
intros z z_neq ; destruct z as (r, r0) ; apply (proj1 (Ceq _ _)) ; split ;
compute.
replace (r × / (r × r + r0 × r0) × r + - (- r0 × / (r × r + r0 × r0) × r0))%R with
(((r × r) + - (- r0 × r0)) / (r × r + r0 × r0))%R.
unfold Rdiv ; replace (- (- r0 × r0))%R with (r0 × r0)%R by field.
apply Rinv_r. intro Hyp ; apply z_neq.
apply (proj2 (C0_norm_R0 _)) ; unfold Cnorm_sqr ; intuition.
field.
replace (r × r + r0 × r0)%R with (Cnorm_sqr (r +i r0)).
intro H ; apply z_neq ; apply (proj2 (C0_norm_R0 _) H).
unfold Cnorm_sqr ; intuition.
field.
replace (r × r + r0 × r0)%R with (Cnorm_sqr (r +i r0)).
intro H ; apply z_neq ; apply (proj2 (C0_norm_R0 _) H).
unfold Cnorm_sqr ; intuition.
Qed.
Hint Resolve Cinv_l : complex.

Lemma Cinv_r : z:C, z C0z × /z = 1.
Proof.
intros ; rewrite Cmult_comm ; apply Cinv_l ; assumption.
Qed.
Hint Resolve Cinv_r : complex.

Distributivity

Lemma Cmult_add_distr_l : z1 z2 z3 : C, z1 × (z2 + z3) = z1 × z2 + z1 × z3.
Proof.
CusingR_f.
Qed.

Lemma Cmult_add_distr_r : z1 z2 z3 : C, (z2 + z3) × z1= z2 × z1 + z3 × z1.
Proof.
CusingR_f.
Qed.

1 <> 0
Lemma C1_neq_C0 : 1 0.
Proof.
intro H ; apply (proj2 (Ceq _ _)) in H ; destruct H as (H, H0); compute in H ;
apply R1_neq_R0 ; assumption.
Qed.
Hint Resolve C1_neq_C0 : complex.

# R Vector Space Lemmas

Lemma Cscal_1 : z : C, 1%R `* z = z.
Proof.
intro ; CusingR.
Qed.

Lemma Cscal_distr_C_l : x, u v, x `* (u + v) = x `* u + x `* v.
Proof.
CusingR.
Qed.

Lemma Cscal_distr_R_r : x y : R, z : C, (x + y)%R `* z = x `* z + y `* z.
Proof.
CusingR_f.
Qed.

Lemma Cscal_assoc : x y : R, z : C, (x × y)%R `* z = x `* (y `* z).
Proof.
CusingR_f.
Qed.

Lemma Crev_distr : x : R, u v : C, x `* (u + v) = x `* u + x `* v.
Proof.
CusingR.
Qed.

# Other properties (Cconj)

Lemma Cadd_conj : z : C, z + Cconj z = (C1 + C1) × (Cre z +i 0%R).
Proof.
CusingR_f.
Qed.

Lemma Cminus_conj : z : C, z - Cconj z = (C1 + C1) × (0%R +i Cim z).
Proof.
CusingR_f.
Qed.

Lemma Cmul_conj : z1 z2, (Cconj z1) × z2 = Cconj (z1 × (Cconj z2)).
Proof.
CusingR_f.
Qed.

Lemma Cexist_rep_complex : a b : R, x : C, Cre x = a Cim x = b.
Proof.
intros a b.
(a +i b).
intuition.
Qed.