Require Export Cdefinitions.

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.

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.

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%R → z = 0.
Proof.
intros. apply <- C0_norm_R0. assumption.
Qed.
Hint Resolve HC0_norm_R0 : complex.

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 = z2 → Cre z1 = Cre z2.
Proof.
intros a b H ; rewrite H ; reflexivity.
Qed.

Lemma Cim_eq_compat : ∀ z1 z2, z1 = z2 → Cim 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.
Hint Resolve Cadd_comm : complex.

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

Lemma Cadd_0_l : ∀ z : C, 0 + z = z.
Proof.
CusingR.
Qed.
Hint Resolve Cadd_0_l : complex.

Lemma Cadd_0_r : ∀ z : C, z + 0 = z.
Proof.
CusingR.
Qed.
Hint Resolve Cadd_0_r : complex.

Lemma Cadd_opp_r : ∀ z : C, z + - z = 0.
Proof.
CusingR.
Qed.
Hint Resolve Cadd_opp_r : complex.

Lemma Cadd_opp_l : ∀ z : C, - z + z = 0.
Proof.
CusingR.
Qed.
Hint Resolve Cadd_opp_l : complex.

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

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

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.

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.

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 ≠ C0 → z × /z = 1.
Proof.
intros ; rewrite Cmult_comm ; apply Cinv_l ; assumption.
Qed.
Hint Resolve Cinv_r : complex.

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

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

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.

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.

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.