FinMatrix.CoqExt.Complex
Require Export Hierarchy ElementType.
Require Export RExt RFunExt.
Open Scope R_scope.
Declare Scope C_scope.
Delimit Scope C_scope with C.
Open Scope C_scope.
Record C := mkC { Cre : R; Cim : R}.
Infix " '+i' " := mkC (at level 60) : 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.
Convert a real number to a complex number
Common constant complex numbers
Definition C0 := 0 +i 0.
Definition C1 := 1 +i 0.
Definition Ci := 0 +i 1.
Lemma Cproj_right : forall z : C, z = z.a +i z.b.
Proof. intros (a,b). auto. Qed.
Lemma Cexist_rep_complex : forall a b : R, exists x : C, x = a +i b.
Proof. intros. exists (a +i b). auto. Qed.
Definition C1 := 1 +i 0.
Definition Ci := 0 +i 1.
Lemma Cproj_right : forall z : C, z = z.a +i z.b.
Proof. intros (a,b). auto. Qed.
Lemma Cexist_rep_complex : forall a b : R, exists x : C, x = a +i b.
Proof. intros. exists (a +i b). auto. Qed.
Equality of complex is decidable
#[export] Instance Ceq_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.
Defined.
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.
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.
Defined.
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. rewrite Ceq_iff. tauto. Qed.
Proof. intros. rewrite Ceq_iff. tauto. Qed.
C1 <> C0
Lemma C1_neq_C0 : C1 <> C0.
Proof.
intro H. apply (proj1 (Ceq_iff _ _)) in H. simpl in *. destruct H; auto with R.
Qed.
#[export] Hint Resolve C1_neq_C0 : C.
Proof.
intro H. apply (proj1 (Ceq_iff _ _)) in H. simpl in *. destruct H; auto with R.
Qed.
#[export] Hint Resolve C1_neq_C0 : C.
equality of complex numbers
Automation for complex arithmetic
Ltac ca :=
ra;
try autorewrite with C;
try auto with C;
Csimpl; ra.
ra;
try autorewrite with C;
try auto with C;
Csimpl; ra.
Definition Cnorm2 (z : C) : R :=
z.a * z.a + z.b * z.b.
Notation "| z |2" := (Cnorm2 z)
(at level 30, z at level 25, format "| z |2") : C_scope.
z.a * z.a + z.b * z.b.
Notation "| z |2" := (Cnorm2 z)
(at level 30, z at level 25, format "| z |2") : C_scope.
Note that, this notation is too complex, but I havn't found a simple style now
z is zero, iff its norm2 is zero
z <> 0 <-> | z |2 <> 0
Lemma Cneq0_iff_norm2_neq0 : forall z : C, z <> C0 <-> | z |2 <> 0.
Proof.
intros. split; intros; intro.
- apply C0_norm_0 in H0. easy.
- apply C0_norm_0 in H0. easy.
Qed.
Proof.
intros. split; intros; intro.
- apply C0_norm_0 in H0. easy.
- apply C0_norm_0 in H0. easy.
Qed.
0 <= | z |2
0 < x*x + y*y <-> x +i y <> C0
Lemma Cnorm2_pos_iff (x y : R) : (0 < x * x + y * y) <-> x +i y <> C0.
Proof.
split; intros.
- intro. inversion H0. subst. lra.
- apply Cneq_iff in H. simpl in H. destruct H; ra.
Qed.
Hint Resolve Cnorm2_pos_iff : C.
Proof.
split; intros.
- intro. inversion H0. subst. lra.
- apply Cneq_iff in H. simpl in H. destruct H; ra.
Qed.
Hint Resolve Cnorm2_pos_iff : C.
Cnorm2 z = (Cnorm z)²
Lemma Cnorm2_eq (z : C) : | z |2 = (| z |%C)².
Proof. unfold Cnorm. rewrite Rsqr_sqrt; auto. apply Cnorm2_ge0. Qed.
Proof. unfold Cnorm. rewrite Rsqr_sqrt; auto. apply Cnorm2_ge0. Qed.
| 0 | = 0
Lemma Cnorm_C0 : |C0| = R0.
Proof. cbv. autorewrite with R. ra. Qed.
#[export] Hint Rewrite Cnorm_C0 : C.
Proof. cbv. autorewrite with R. ra. Qed.
#[export] Hint Rewrite Cnorm_C0 : C.
z = C0 -> | z | = 0
Lemma Cnorm0_if_C0 : forall z : C, z = C0 -> | z | = 0.
Proof. ca. rewrite H. ca. Qed.
#[export] Hint Resolve Cnorm0_if_C0 : C.
Proof. ca. rewrite H. ca. Qed.
#[export] Hint Resolve Cnorm0_if_C0 : C.
| z | = 0 -> z = C0
Lemma Cnorm0_imply_C0 : forall z : C, | z | = 0 -> z = C0.
Proof.
ca. apply Rsqrt_plus_sqr_eq0_iff in H. simpl in H. destruct H. subst. auto.
Qed.
#[export] Hint Resolve Cnorm0_imply_C0 : C.
Proof.
ca. apply Rsqrt_plus_sqr_eq0_iff in H. simpl in H. destruct H. subst. auto.
Qed.
#[export] Hint Resolve Cnorm0_imply_C0 : C.
z = C0 <-> | z | = 0
0 <= | z |
Lemma Cnorm_ge0 : forall z : C, 0 <= | z |%C.
Proof. ca. unfold Cnorm. ca. Qed.
#[export] Hint Resolve Cnorm_ge0 : C.
Proof. ca. unfold Cnorm. ca. Qed.
#[export] Hint Resolve Cnorm_ge0 : C.
z <> C0 -> 0 < | z |
Lemma Cnorm_gt0_if_neq0 : forall z : C, z <> C0 -> 0 < | z |%C.
Proof.
intros. destruct (Aeqdec z C0); subst; try easy.
destruct (Cnorm_ge0 z); auto.
apply eq_sym, Cnorm0_iff_C0 in H0. easy.
Qed.
#[export] Hint Resolve Cnorm_gt0_if_neq0 : C.
Proof.
intros. destruct (Aeqdec z C0); subst; try easy.
destruct (Cnorm_ge0 z); auto.
apply eq_sym, Cnorm0_iff_C0 in H0. easy.
Qed.
#[export] Hint Resolve Cnorm_gt0_if_neq0 : C.
z <> C0 -> | z | <> 0
Lemma Cnorm_neq0_if_neq0 : forall z : C, z <> C0 -> | z | <> 0.
Proof. ca. Qed.
#[export] Hint Resolve Cnorm_neq0_if_neq0 : C.
Proof. ca. Qed.
#[export] Hint Resolve Cnorm_neq0_if_neq0 : C.
| z | <> 0 -> z <> C0
Lemma Cnorm_neq0_imply_neq0 : forall z : C, | z | <> 0 -> z <> C0.
Proof. ca. Qed.
#[export] Hint Resolve Cnorm_neq0_imply_neq0 : C.
Proof. ca. Qed.
#[export] Hint Resolve Cnorm_neq0_imply_neq0 : C.
| a +i 0 | = | a |
Lemma Cnorm_Cre_simpl : forall (a : R), | a +i 0 | = | a |%R.
Proof.
intros; unfold Cnorm, Cnorm2; simpl. ca.
Qed.
#[export] Hint Rewrite Cnorm_Cre_simpl : C.
Proof.
intros; unfold Cnorm, Cnorm2; simpl. ca.
Qed.
#[export] Hint Rewrite Cnorm_Cre_simpl : C.
| 0 +i b | = | b |
Lemma Cnorm_Cim_simpl : forall (b : R), | 0 +i b | = | b |%R.
Proof.
intros; unfold Cnorm, Cnorm2; simpl. ca.
Qed.
#[export] Hint Rewrite Cnorm_Cim_simpl : C.
Proof.
intros; unfold Cnorm, Cnorm2; simpl. ca.
Qed.
#[export] Hint Rewrite Cnorm_Cim_simpl : C.
| a +i b | = | b +i a |
Lemma Cnorm_comm : forall (a b : R), | a +i b | = | b +i a |.
Proof.
intros; unfold Cnorm, Cnorm2. simpl. f_equal; ring.
Qed.
Proof.
intros; unfold Cnorm, Cnorm2. simpl. f_equal; ring.
Qed.
0 < | z | -> z <> C0
Lemma Cnorm_gt0_imply_neq0 : forall z : C, 0 < | z |%C -> z <> C0.
Proof.
intros. destruct (Aeqdec z C0); auto. subst. rewrite Cnorm_C0 in H. lra.
Qed.
#[export] Hint Resolve Cnorm_gt0_imply_neq0 : C.
Proof.
intros. destruct (Aeqdec z C0); auto. subst. rewrite Cnorm_C0 in H. lra.
Qed.
#[export] Hint Resolve Cnorm_gt0_imply_neq0 : C.
| R2C a | = | a |
Lemma Cnorm_R2C_Rabs : forall a : R, |R2C a| = | a |%R.
Proof. intros. unfold R2C. ca. Qed.
#[export] Hint Rewrite Cnorm_R2C_Rabs : C.
Proof. intros. unfold R2C. ca. Qed.
#[export] Hint Rewrite Cnorm_R2C_Rabs : C.
| | z | | = | z |, that is: | R2C (| z |) | = | z |
Lemma Cnorm_norm : forall z : C, | R2C (| z |%C) | = | z |.
Proof.
ca. apply Rabs_right. apply Rle_ge. ca.
Qed.
#[export] Hint Rewrite Cnorm_norm : C.
Proof.
ca. apply Rabs_right. apply Rle_ge. ca.
Qed.
#[export] Hint Rewrite Cnorm_norm : C.
| 1 | = 1
Rabs | z | = | z |
Lemma Rabs_Cnorm : forall z : C, | | z |%C |%R = | z |.
Proof. intro z; apply Rabs_right; apply Rle_ge; apply Cnorm_ge0. Qed.
#[export] Hint Rewrite Rabs_Cnorm : C.
Proof. intro z; apply Rabs_right; apply Rle_ge; apply Cnorm_ge0. Qed.
#[export] Hint Rewrite Rabs_Cnorm : C.
| a | <= | a +i b |
Lemma Cre_le_Cnorm : forall z : C, | z.a | <= | z |%C.
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.
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 +i b |
Lemma Cim_le_Cnorm : forall z : C, | z.b | <= | z |%C.
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.
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 +i b| <= | a | + | b |
Lemma Cnorm_le_Cre_Cim : forall z : C, | z |%C <= | z.a | + | z.b |.
Proof. Csimpl. unfold Cnorm, Cnorm2; simpl. apply R_neq5. Qed.
Proof. Csimpl. unfold Cnorm, Cnorm2; simpl. apply R_neq5. Qed.
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, (z1 + z2).a = (z1.a + z2.a)%R.
Proof. Csimpl. auto. Qed.
Lemma Cim_add : forall z1 z2, (z1 + z2).b = (z1.b + z2.b)%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, C0 + z = z.
Proof. Ceq. Qed.
Lemma Cadd_0_r : forall z : C, z + C0 = z.
Proof. Ceq. Qed.
#[export] Hint Rewrite
Cre_add Cim_add
Cadd_0_l Cadd_0_r
: C.
#[export] Hint Resolve
Cadd_comm
Cadd_assoc
: C.
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, (z1 + z2).a = (z1.a + z2.a)%R.
Proof. Csimpl. auto. Qed.
Lemma Cim_add : forall z1 z2, (z1 + z2).b = (z1.b + z2.b)%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, C0 + z = z.
Proof. Ceq. Qed.
Lemma Cadd_0_r : forall z : C, z + C0 = z.
Proof. Ceq. Qed.
#[export] Hint Rewrite
Cre_add Cim_add
Cadd_0_l Cadd_0_r
: C.
#[export] Hint Resolve
Cadd_comm
Cadd_assoc
: C.
Definition Copp (z : C) :C := (-z.a) +i (-z.b).
Notation "- z" := (Copp z) : C_scope.
Lemma Cre_opp : forall z, (-z).a = (- z.a)%R.
Proof. Csimpl. auto. Qed.
Lemma Cim_opp : forall z, (-z).b = (- z.b)%R.
Proof. Csimpl. auto. Qed.
Lemma Copp_opp : forall z, --z = z.
Proof. Ceq. Qed.
Lemma Cadd_opp_l : forall z : C, - z + z = C0.
Proof. Ceq. Qed.
Lemma Cadd_opp_r : forall z : C, z + - z = C0.
Proof. Ceq. Qed.
|-z| = | z |
Lemma Cnorm_opp : forall z : C, | -z| = | z |.
Proof. Csimpl. unfold Copp; simpl. cbv. f_equal. ring. Qed.
#[export] Hint Rewrite
Cre_opp Cim_opp Copp_opp
Cadd_opp_l Cadd_opp_r
: C.
Proof. Csimpl. unfold Copp; simpl. cbv. f_equal. ring. Qed.
#[export] Hint Rewrite
Cre_opp Cim_opp Copp_opp
Cadd_opp_l Cadd_opp_r
: C.
Definition Csub (c1 c2 : C) : C := c1 + - c2.
Infix "-" := Csub : C_scope.
Lemma Cre_sub : forall z1 z2, (z1 - z2).a = (z1.a - z2.a)%R.
Proof. Csimpl. auto. Qed.
Lemma Cim_sub : forall z1 z2, (z1 - z2).b = (z1.b - z2.b)%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| = |z2 - z1|.
Proof. Csimpl. cbv; f_equal; ring. Qed.
Infix "-" := Csub : C_scope.
#[export] Hint Rewrite
Copp_add_distr
Copp_sub_distr
: C.
Proof. Csimpl. cbv; f_equal; ring. Qed.
Infix "-" := Csub : C_scope.
#[export] Hint Rewrite
Copp_add_distr
Copp_sub_distr
: C.
|z1 + z2| <= |z1| + |z2|
Lemma Cnorm_triang : forall z1 z2 : C, |z1 + z2|%C <= (|z1|%C + |z2|%C)%R.
Proof.
intros (a,b) (c,d). cbv.
apply Rsqr_incr_0_var; ra. rewrite ?Rsqr_sqrt; ra.
unfold Rsqr. ring_simplify.
rewrite !pow2_sqrt; ra.
rewrite (Rmult_assoc 2 (sqrt _)).
rewrite <- sqrt_mult; ra.
pose proof (R_neq6 a b c d). ra.
Qed.
Proof.
intros (a,b) (c,d). cbv.
apply Rsqr_incr_0_var; ra. rewrite ?Rsqr_sqrt; ra.
unfold Rsqr. ring_simplify.
rewrite !pow2_sqrt; ra.
rewrite (Rmult_assoc 2 (sqrt _)).
rewrite <- sqrt_mult; ra.
pose proof (R_neq6 a b c d). ra.
Qed.
Rabs (|z1| - |z2|) <= |z1 - z2|
Lemma Cnorm_triang_rev : forall z1 z2 : C, | |z1|%C - |z2|%C | <= |z1 - z2|%C.
Proof.
intros z1 z2.
assert (H1 : |z1 - z2 + z2|%C <= |z1 - z2|%C + |z2|%C) by (apply Cnorm_triang).
assert (H2 : |z2 - z1 + z1|%C <= |z2 - z1|%C + |z1|%C) by (apply Cnorm_triang).
assert (H3 : forall a b : C, 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. lra.
- rewrite <- H3 in H1; apply Rminus_le; apply Rle_minus in H1. lra.
Qed.
Proof.
intros z1 z2.
assert (H1 : |z1 - z2 + z2|%C <= |z1 - z2|%C + |z2|%C) by (apply Cnorm_triang).
assert (H2 : |z2 - z1 + z1|%C <= |z2 - z1|%C + |z1|%C) by (apply Cnorm_triang).
assert (H3 : forall a b : C, 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. lra.
- rewrite <- H3 in H1; apply Rminus_le; apply Rle_minus in H1. lra.
Qed.
|z1| - |z2| <= |z1 - z2|
Lemma Cnorm_triang_rev_l : forall z1 z2 : C, |z1|%C - |z2|%C <= |z1 - z2|%C.
Proof.
intros z1 z2; apply Rle_trans with (| |z1|%C - |z2|%C |)%R.
apply RRle_abs. apply Cnorm_triang_rev.
Qed.
Proof.
intros z1 z2; apply Rle_trans with (| |z1|%C - |z2|%C |)%R.
apply RRle_abs. apply Cnorm_triang_rev.
Qed.
|z2| - |z1| <= |z1 - z2|
Lemma Cnorm_triang_rev_r : forall z1 z2 : C, |z2|%C - |z1|%C <= |z1 - z2|%C.
Proof.
intros z1 z2; apply Rle_trans with (| |z2|%C - |z1|%C |%R).
apply RRle_abs. rewrite Rabs_minus_sym. apply Cnorm_triang_rev.
Qed.
End triangle_ineq.
Proof.
intros z1 z2; apply Rle_trans with (| |z2|%C - |z1|%C |%R).
apply RRle_abs. rewrite Rabs_minus_sym. apply Cnorm_triang_rev.
Qed.
End triangle_ineq.
Definition Ccmul (k : R) (z : C) : C := (k * z.a) +i (k * z.b).
Infix "c*" := Ccmul: C_scope.
Lemma Cre_cmul : forall z k, (k c* z).a = (k * z.a)%R.
Proof. intros (a,b) k; auto. Qed.
Lemma Cim_cmul : forall z k, (k c* z).b = (k * z.b)%R.
Proof. intros (a,b) k; auto. Qed.
Lemma Ccmul_1 : forall z : C, 1 c* z = z.
Proof. Ceq. Qed.
Lemma Ccmul_add_distr_l : forall k z1 z2, k c* (z1 + z2) = k c* z1 + k c* z2.
Proof. Ceq. Qed.
Lemma Ccmul_add_distr_r : forall k1 k2 z, (k1 + k2)%R c* z = k1 c* z + k2 c* z.
Proof. Ceq. Qed.
Lemma Ccmul_mul_swap_l : forall k1 k2 z, (k1 * k2)%R c* z = k1 c* (k2 c* z).
Proof. Ceq. Qed.
Infix "c*" := Ccmul: C_scope.
Lemma Cre_cmul : forall z k, (k c* z).a = (k * z.a)%R.
Proof. intros (a,b) k; auto. Qed.
Lemma Cim_cmul : forall z k, (k c* z).b = (k * z.b)%R.
Proof. intros (a,b) k; auto. Qed.
Lemma Ccmul_1 : forall z : C, 1 c* z = z.
Proof. Ceq. Qed.
Lemma Ccmul_add_distr_l : forall k z1 z2, k c* (z1 + z2) = k c* z1 + k c* z2.
Proof. Ceq. Qed.
Lemma Ccmul_add_distr_r : forall k1 k2 z, (k1 + k2)%R c* z = k1 c* z + k2 c* z.
Proof. Ceq. Qed.
Lemma Ccmul_mul_swap_l : forall k1 k2 z, (k1 * k2)%R c* z = k1 c* (k2 c* z).
Proof. Ceq. Qed.
|k * z| = |k| * | z |
Lemma Cnorm_cmul : forall k z, |k c* z| = (| k | * | z |%C)%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.
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.
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, C0 * z = C0 .
Proof. Ceq. Qed.
Lemma Cmul_0_r : forall z : C, z * C0 = C0.
Proof. Ceq. Qed.
Lemma Cmul_1_l : forall z : C, C1 * z = z .
Proof. Ceq. Qed.
Lemma Cmul_1_r : forall z : C, z * C1 = 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| = (|z1|%C * |z2|%C)%R.
Proof. intros (a,b) (c,d). cbv. rewrite <- sqrt_mult; ra. f_equal. ra. Qed.
Hint Resolve
Cmul_comm Cmul_assoc
Cmul_1_l Cmul_1_r
Cmul_add_distr_l Cmul_add_distr_r
: C.
Lemma C_ring : ring_theory C0 C1 Cadd Cmul Csub Copp eq.
Proof. constructor; intros; ca. Qed.
Add Ring C_ring_inst : C_ring.
Proof. intros (a,b) (c,d). cbv. rewrite <- sqrt_mult; ra. f_equal. ra. Qed.
Hint Resolve
Cmul_comm Cmul_assoc
Cmul_1_l Cmul_1_r
Cmul_add_distr_l Cmul_add_distr_r
: C.
Lemma C_ring : ring_theory C0 C1 Cadd Cmul Csub Copp eq.
Proof. constructor; intros; ca. Qed.
Add Ring C_ring_inst : C_ring.
Fixpoint Cpow (z : C) (n : nat) {struct n} : C :=
match n with
| 0%nat => C1
| S m => z * (Cpow z m)
end.
Infix "^" := Cpow : C_scope.
Lemma Cpow_0 : forall z : C, z ^ 0 = C1.
Proof. auto. Qed.
Lemma C0_pow : forall n, (0 < n)%nat -> C0 ^ n = C0.
Proof.
induction n; intros; auto. lia.
destruct (Nat.eq_dec n 0).
- 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 C. 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 C.
- rewrite IHn. auto with C.
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 C. rewrite IHn. ring. Qed.
Lemma Cpow_R2C : forall z n, (R2C z) ^ n = R2C (z ^ n).
Proof. intros z n ; induction n; auto. simpl. rewrite IHn. Ceq. Qed.
| z ^ n| = | z | ^ n
Lemma Cnorm_pow : forall (z : C) n, |z ^ n| = ((| z |%C) ^ n)%R.
Proof.
intros z n; induction n. apply Cnorm_C1.
simpl; rewrite Cnorm_Cmult, IHn; reflexivity.
Qed.
Proof.
intros z n; induction n. apply Cnorm_C1.
simpl; rewrite Cnorm_Cmult, IHn; reflexivity.
Qed.
Definition Cinv (z : C) : C := (z.a / | z |2) +i (-z.b / | z |2).
Notation "/ z" := (Cinv z) : C_scope.
Lemma Cinv_rew : forall a b : R,
(a +i b) <> C0 -> /(a +i b) = (/ (a*a + b*b)) c* (a +i - b)%R.
Proof. Ceq. cbv; lra. cbv; lra. Qed.
Lemma Cmul_inv_l : forall z : C, z <> C0 -> / z * z = C1.
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 = C1.
Proof. intros. rewrite Cmul_comm. apply Cmul_inv_l. auto. Qed.
Tips: A Coq-version-issue about inv_sqrt and sqrt_inv
There are two similiar lemmas: inv_sqrt and sqrt_inv
z <> C0 -> |/z| = / | z |
Lemma Cnorm_inv : forall z : C, z <> C0 -> | /z | = (/(| z |%C))%R.
Proof.
intros (a,b) H. cbv. rewrite <- sqrt_inv. f_equal. ra.
apply Cneq_iff in H; simpl in H. ra.
Qed.
Proof.
intros (a,b) H. cbv. rewrite <- sqrt_inv. f_equal. ra.
apply Cneq_iff in H; simpl in H. ra.
Qed.
z <> C0 -> (/z).a = z.a / | z |2
z <> C0 -> (/z).b = -z.b / | z |2
Lemma Cim_inv_neq0 (z : C) : z <> C0 -> (/ z).b = (-z.b / | z |2)%R.
Proof. auto. Qed.
Hint Resolve
Cmul_inv_l Cmul_inv_r
: C.
Proof. auto. Qed.
Hint Resolve
Cmul_inv_l Cmul_inv_r
: C.
z <> C0 -> /z = C1 / z
Lemma Cinv_eq_div (z : C) : z <> C0 -> (/ z) = (C1 / z).
Proof. Ceq. Qed.
Lemma C_field : field_theory C0 C1 Cadd Cmul Csub Copp Cdiv Cinv eq.
Proof. constructor; intros; auto with C. apply C_ring. Qed.
Add Field C_field_inst : C_field.
Proof. Ceq. Qed.
Lemma C_field : field_theory C0 C1 Cadd Cmul Csub Copp Cdiv Cinv eq.
Proof. constructor; intros; auto with C. apply C_ring. Qed.
Add Field C_field_inst : C_field.
Definition Cconj (z : C) : C := (z.a) +i (-z.b).
Notation "z \*" := (Cconj z) (at level 20, format "z \*") : 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 : C, (z1 * z2)\* = z1\* * z2\*.
Proof. Ceq. Qed.
| z\* | = | z |
1.2 Triangle Representation of Complex number (复数的三角表示)
Some inequalities about real part or imaginay part of a complex number
Lemma Cnorm_ge_AbsCre (z : C) : | z.a | <= | z |%C.
Proof. apply Cre_le_Cnorm. Qed.
Lemma Cnorm_ge_AbsCim (z : C) : | z.b | <= | z |%C.
Proof. apply Cim_le_Cnorm. Qed.
Lemma Cnorm_le_AbsCre_plus_AbsCim (z : C) : | z |%C <= (|z.a| + |z.b|)%R.
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.
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 isCArg (z : C) (theta : R) : Prop :=
exists (k : Z), theta = (/_ z + 2 * (IZR k) * PI)%R.
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 -> /_ (x +i y) = atan (y/x)
Lemma Carg_xgt0 (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.
x > 0 -> /_ (x +i y) = atan (y/x).
Proof.
intros. unfold Carg. simpl.
bdestruct (x =? 0); try lra.
bdestruct (x <? 0); try lra.
Qed.
x = 0 -> y > 0 -> /_ (x +i y) = PI / 2
Lemma Carg_xeq0_ygt0 (x y : R) :
x = 0 -> y > 0 -> /_ (x +i y) = (PI / 2)%R.
Proof.
intros. unfold Carg. simpl.
bdestruct (x =? 0); try lra.
bdestruct (y <? 0); try lra.
Qed.
x = 0 -> y > 0 -> /_ (x +i y) = (PI / 2)%R.
Proof.
intros. unfold Carg. simpl.
bdestruct (x =? 0); try lra.
bdestruct (y <? 0); try lra.
Qed.
x = 0 -> y < 0 -> /_ (x +i y) = (- PI / 2)
Lemma Carg_xeq0_ylt0 (x y : R) :
x = 0 -> y < 0 -> /_ (x +i y) = (- PI / 2)%R.
Proof.
intros. unfold Carg. simpl.
bdestruct (x =? 0); try lra.
bdestruct (y <? 0); try lra.
Qed.
x = 0 -> y < 0 -> /_ (x +i y) = (- PI / 2)%R.
Proof.
intros. unfold Carg. simpl.
bdestruct (x =? 0); try lra.
bdestruct (y <? 0); try lra.
Qed.
x < 0 -> y >= 0 -> /_ (x +i y) = (atan (y/x) + PI)
Lemma Carg_xlt0_yge0 (x y : R) :
x < 0 -> 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.
x < 0 -> 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.
x < 0 -> y < 0 -> /_ (x +i y) = (atan (y/x) - PI)
Lemma Carg_xlt0_ylt0 (x y : R) :
x < 0 -> 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.
x < 0 -> 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.
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_b_div_a (a b : R) :
a <> 0 -> (/ (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; [|ra].
rewrite sqrt_div_alt; ra. split; ra.
Qed.
a <> 0 -> (/ (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; [|ra].
rewrite sqrt_div_alt; ra. split; ra.
Qed.
nonzero complex number, the cosine of its main argument equal to
real part divide magnitude (主辐角的余弦等于实部除以模长)
Lemma cos_Carg_neq0 (z : C) : z <> C0 -> cos(/_ z) = (z.a / | z |%C)%R.
Proof.
Csimpl. unfold Cnorm,Cnorm2; simpl.
bdestruct (a >? 0).
- rewrite Carg_xgt0; auto. rewrite cos_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_right; ra.
- bdestruct (a =? 0); subst.
+ bdestruct (b >? 0).
* rewrite Carg_xeq0_ygt0; ra.
* apply Cneq_iff in H; simpl in H. assert (b < 0) by ra.
rewrite Carg_xeq0_ylt0; ra. ra.
+ bdestruct (b >=? 0).
* rewrite Carg_xlt0_yge0; ra. rewrite cos_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
* rewrite Carg_xlt0_ylt0; ra. rewrite cos_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
Qed.
Proof.
Csimpl. unfold Cnorm,Cnorm2; simpl.
bdestruct (a >? 0).
- rewrite Carg_xgt0; auto. rewrite cos_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_right; ra.
- bdestruct (a =? 0); subst.
+ bdestruct (b >? 0).
* rewrite Carg_xeq0_ygt0; ra.
* apply Cneq_iff in H; simpl in H. assert (b < 0) by ra.
rewrite Carg_xeq0_ylt0; ra. ra.
+ bdestruct (b >=? 0).
* rewrite Carg_xlt0_yge0; ra. rewrite cos_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
* rewrite Carg_xlt0_ylt0; ra. rewrite cos_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
Qed.
nonzero complex number, the sine of its main argument equal to
imaginary part divide magnitude (主辐角的正弦等于虚部除以模长)
Lemma sin_Carg_neq0 (z : C) : z <> C0 -> sin(/_ z) = ((Cim z) / | z |%C)%R.
Proof.
Csimpl. unfold Cnorm,Cnorm2; simpl.
bdestruct (a >? 0).
- rewrite Carg_xgt0; auto. rewrite sin_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_right; ra.
- bdestruct (a =? 0); subst.
+ bdestruct (b >? 0).
* rewrite Carg_xeq0_ygt0; ra. symmetry. ra.
* apply Cneq_iff in H; simpl in H. assert (b < 0) by ra.
rewrite Carg_xeq0_ylt0; ra. symmetry. ra.
+ bdestruct (b >=? 0).
* rewrite Carg_xlt0_yge0; ra. rewrite sin_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
* rewrite Carg_xlt0_ylt0; ra. rewrite sin_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
Qed.
Proof.
Csimpl. unfold Cnorm,Cnorm2; simpl.
bdestruct (a >? 0).
- rewrite Carg_xgt0; auto. rewrite sin_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_right; ra.
- bdestruct (a =? 0); subst.
+ bdestruct (b >? 0).
* rewrite Carg_xeq0_ygt0; ra. symmetry. ra.
* apply Cneq_iff in H; simpl in H. assert (b < 0) by ra.
rewrite Carg_xeq0_ylt0; ra. symmetry. ra.
+ bdestruct (b >=? 0).
* rewrite Carg_xlt0_yge0; ra. rewrite sin_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
* rewrite Carg_xlt0_ylt0; ra. rewrite sin_atan.
unfold Rdiv at 1. rewrite Rinv_Rsqrt_1_plus_Rsqr_b_div_a; ra.
rewrite Rabs_left1 by lra. ra.
Qed.
非零复数的主辐角的正切表达式
Lemma tan_Carg_neq0 (z : C) : z.a <> 0%R -> tan(/_ z) = ((Cim z) / Cre z)%R.
Proof.
intros.
assert (z <> C0). apply Cneq_iff; auto.
rewrite tan_eq.
rewrite cos_Carg_neq0, sin_Carg_neq0; auto. field. split; auto.
apply Cnorm_neq0_if_neq0; auto.
Qed.
Proof.
intros.
assert (z <> C0). apply Cneq_iff; auto.
rewrite tan_eq.
rewrite cos_Carg_neq0, sin_Carg_neq0; auto. field. split; auto.
apply Cnorm_neq0_if_neq0; auto.
Qed.
非零复数实部等于模乘以辐角余弦
Lemma Cre_eq_Cnorm_mul_cos_Carg (z : C) : z <> C0 -> z.a = (| z |%C * cos(/_ z))%R.
Proof.
intros. rewrite cos_Carg_neq0; auto. field. apply Cnorm_neq0_if_neq0 in H; auto.
Qed.
Proof.
intros. rewrite cos_Carg_neq0; auto. field. apply Cnorm_neq0_if_neq0 in H; auto.
Qed.
非零复数虚部等于模乘以辐角正弦
Lemma Cim_eq_Cnorm_mul_sin_Carg (z : C) : z <> C0 -> z.b = (| z |%C * sin(/_ z))%R.
Proof.
intros. rewrite sin_Carg_neq0; auto. field. apply Cnorm_neq0_if_neq0; auto.
Qed.
Proof.
intros. rewrite sin_Carg_neq0; auto. field. apply Cnorm_neq0_if_neq0; auto.
Qed.
非零复数，(相等 <-> 模长和辐角相等)
Lemma Cneq0_eq_iff_Cnorm_Carg (z1 z2 : C) (H1 : z1 <> C0) (H2 : z2 <> C0) :
z1 = z2 <-> (|z1| = |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.
z1 = z2 <-> (|z1| = |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.
Lemma CnormCadd_le_CaddCnorm (z1 z2 : C) : |z1 + z2|%C <= |z1|%C + |z2|%C.
Proof. apply Cnorm_triang. Qed.
Lemma CnormCadd_ge_AbsSubCnorm (z1 z2 : C) : | |z1|%C - |z2|%C | <= |z1 + z2|%C.
Proof.
Admitted.
Lemma CnormCsub_le_CaddCnorm (z1 z2 : C) : |z1 - z2|%C <= |z1|%C + |z2|%C.
Proof.
Admitted.
Lemma CnormCsub_ge_AbsSubCnorm (z1 z2 : C) : | |z1|%C - |z2|%C | <= |z1 - z2|%C.
Proof. apply Cnorm_triang_rev. Qed.
Definition Ctrigo (r θ : R) : C := r c* (cos θ +i sin θ).
Infix "^^" := Ctrigo (at level 30) : C_scope.
Infix "^^" := Ctrigo (at level 30) : C_scope.
复数三角表示的重写形式
复数的三角表示有无穷多种选择
Lemma Ctrigo_many : forall (r θ : R) (k : Z),
let θ' : R := (θ + 2 * (IZR k) * PI)%R in
r ^^ θ = r c* (cos θ' +i sin θ').
Proof.
intros. unfold Ctrigo, θ'. rewrite cos_period_Z, sin_period_Z.
auto.
Qed.
let θ' : R := (θ + 2 * (IZR k) * PI)%R in
r ^^ θ = r c* (cos θ' +i sin θ').
Proof.
intros. unfold Ctrigo, θ'. rewrite cos_period_Z, sin_period_Z.
auto.
Qed.
Tips: 例 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 <> C0 -> Cconj z = Ctrigo (| z |%C) (-/_ 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_if_neq0; auto.
Qed.
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_if_neq0; auto.
Qed.
1/z的三角表示
Definition Ctrigo_Cinv (z : C) (k : Z) : C :=
let r := | z | in
let θ := Carg z in
Ctrigo (/r)%R (-θ)%R.
let r := | z | in
let θ := Carg z in
Ctrigo (/r)%R (-θ)%R.
/z 的三角表示公式正确
Lemma Ctrigo_Cinv_ok (z : C) (k : Z) : z <> C0 -> /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.
Proof.
intros. intros; destruct z as (a,b). rewrite Cinv_rew; auto.
remember ((a^2)+(b^2))%R as r.
unfold Ctrigo_Cinv.
Admitted.
复数除法运算的三角表示版本。注意，z2 <> C0
复数乘法三角表示版本与常规乘法定义等价
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 C0), (Aeqdec z2 C0); subst; Ceq;
repeat rewrite Cnorm_C0_eq0; autorewrite with R; auto.
Abort.
z1 * z2 = CmultTrigo z1 z2.
Proof.
unfold CmultTrigo, Ctrigo.
rewrite cos_plus, sin_plus. unfold Ccmul.
destruct (Aeqdec z1 C0), (Aeqdec z2 C0); subst; Ceq;
repeat rewrite Cnorm_C0_eq0; autorewrite with R; auto.
Abort.
除数非零时，复数除法三角表示版本与常规除法定义等价
Lemma CdivTrigo_eq_Cdiv (z1 z2 : C) :
z2 <> C0 -> z1 / z2 = CdivTrigo z1 z2.
Proof.
intros. unfold CdivTrigo, Ctrigo.
rewrite cos_minus, sin_minus. unfold Ccmul. simpl.
destruct (Aeqdec z1 C0), (Aeqdec z2 C0);
subst; rewrite ?Cnorm_C0_eq0; unfold Cdiv.
- destruct H. auto.
Abort.
z2 <> C0 -> z1 / z2 = CdivTrigo z1 z2.
Proof.
intros. unfold CdivTrigo, Ctrigo.
rewrite cos_minus, sin_minus. unfold Ccmul. simpl.
destruct (Aeqdec z1 C0), (Aeqdec z2 C0);
subst; rewrite ?Cnorm_C0_eq0; unfold Cdiv.
- destruct H. auto.
Abort.
复数开方运算的三角表示版本。注意，z2 <> C0，共有 n 个根（n个不同的主辐角）
Definition CnrootTrigo (z : C) (n : nat) (k : nat) : C :=
Ctrigo ( / (| z |%C ^ n))%R ((/_ z + 2 * (INR k) * PI) / (INR n))%R.
Ctrigo ( / (| z |%C ^ n))%R ((/_ z + 2 * (INR k) * PI) / (INR n))%R.
复数乘方三角版本的性质
幂为 0
Lemma CpowTrigo_0 (z : C) : CpowTrigo z 0 = C1.
Proof.
unfold CpowTrigo. simpl. unfold Ctrigo.
rewrite Rmult_0_l. rewrite cos_0, sin_0. compute. f_equal; ring.
Qed.
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.
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.
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.
复数开方运算的三角表示版本 与 复数乘方三角表示版本的互逆性
Hint Resolve eq_equivalence : C.
operations are well-defined. Eg: Proper (eq ==> eq ==> eq) Cadd
Lemma Cadd_wd : Proper (eq ==> eq ==> eq) Cadd.
Proof. repeat (hnf; intros); subst; auto. Qed.
Lemma Copp_wd : Proper (eq ==> eq) Copp.
Proof. repeat (hnf; intros); subst; auto. Qed.
Lemma Csub_wd : Proper (eq ==> eq ==> eq) Csub.
Proof. repeat (hnf; intros); subst; auto. Qed.
Lemma Cmul_wd : Proper (eq ==> eq ==> eq) Cmul.
Proof. repeat (hnf; intros); subst; auto. Qed.
Lemma Cinv_wd : Proper (eq ==> eq) Cinv.
Proof. repeat (hnf; intros); subst; auto. Qed.
Lemma Cdiv_wd : Proper (eq ==> eq ==> eq) Cdiv.
Proof. repeat (hnf; intros); subst; auto. Qed.
Hint Resolve
Cadd_wd Copp_wd Csub_wd
Cmul_wd Cinv_wd Cdiv_wd
: C.
Associative
#[export] Instance Cadd_Assoc : Associative Cadd.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_Assoc : Associative Cmul.
Proof. constructor; intros; field. Qed.
Hint Resolve
Cadd_Assoc
Cmul_Assoc
: C.
Commutative
#[export] Instance Cadd_Comm : Commutative Cadd.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_Comm : Commutative Cmul.
Proof. constructor; intros; field. Qed.
Hint Resolve Cadd_Comm Cmul_Comm : C.
Identity Left/Right
#[export] Instance Cadd_IdL : IdentityLeft Cadd C0.
Proof. constructor. intros. field. Qed.
#[export] Instance Cadd_IdR : IdentityRight Cadd C0.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_IdL : IdentityLeft Cmul C1.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_IdR : IdentityRight Cmul C1.
Proof. constructor; intros; field. Qed.
Hint Resolve
Cadd_IdL
Cadd_IdR
Cmul_IdL
Cmul_IdR
: C.
Proof. constructor. intros. field. Qed.
#[export] Instance Cadd_IdR : IdentityRight Cadd C0.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_IdL : IdentityLeft Cmul C1.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_IdR : IdentityRight Cmul C1.
Proof. constructor; intros; field. Qed.
Hint Resolve
Cadd_IdL
Cadd_IdR
Cmul_IdL
Cmul_IdR
: C.
Inverse Left/Right
#[export] Instance Cadd_InvL : InverseLeft Cadd C0 Copp.
Proof. constructor; intros; ring. Qed.
#[export] Instance Cadd_InvC : InverseRight Cadd C0 Copp.
Proof. constructor; intros; ring. Qed.
Hint Resolve Cadd_InvL Cadd_InvC : C.
Distributive
#[export] Instance Cmul_add_DistrL : DistrLeft Cadd Cmul.
Proof. constructor; intros; field. Qed.
#[export] Instance Cmul_add_DistrR : DistrRight Cadd Cmul.
Proof. constructor; intros; field. Qed.
Hint Resolve
Cmul_add_DistrL
Cmul_add_DistrR
: C.
Semigroup
#[export] Instance Cadd_SGroup : SGroup Cadd.
Proof. constructor; auto with C. Qed.
#[export] Instance Cmul_SGroup : SGroup Cmul.
Proof. constructor; auto with C. Qed.
Hint Resolve
Cadd_SGroup
Cmul_SGroup
: C.
Abelian semigroup
#[export] Instance Cadd_ASGroup : ASGroup Cadd.
Proof. constructor; auto with C. Qed.
#[export] Instance Cmul_ASGroup : ASGroup Cmul.
Proof. constructor; auto with C. Qed.
Hint Resolve
Cadd_ASGroup
Cmul_ASGroup
: C.
Monoid
#[export] Instance Cadd_Monoid : Monoid Cadd C0.
Proof. constructor; auto with C. Qed.
#[export] Instance Cmul_Monoid : Monoid Cmul C1.
Proof. constructor; auto with C. Qed.
Hint Resolve
Cadd_Monoid
Cmul_Monoid
: C.
Abelian monoid
#[export] Instance Cadd_AMonoid : AMonoid Cadd C0.
Proof. constructor; auto with C. Qed.
#[export] Instance Cmul_AMonoid : AMonoid Cmul C1.
Proof. constructor; auto with C. Qed.
Hint Resolve Cadd_AMonoid Cmul_AMonoid : C.
Group
#[export] Instance Cadd_Group : Group Cadd C0 Copp.
Proof. constructor; auto with C. Qed.
Hint Resolve Cadd_Group : C.
AGroup
#[export] Instance Cadd_AGroup : AGroup Cadd C0 Copp.
Proof. constructor; auto with C. Qed.
Hint Resolve Cadd_AGroup : C.
Ring
#[export] Instance C_Ring : Ring Cadd C0 Copp Cmul C1.
Proof. constructor; auto with C. Qed.
Hint Resolve C_Ring : C.
ARing
#[export] Instance C_ARing : ARing Cadd C0 Copp Cmul C1.
Proof. constructor; auto with C. Qed.
Hint Resolve C_ARing : C.
Field
Module ElementTypeC <: ElementType.
Definition A : Type := C.
Definition Azero : A := C0.
Hint Unfold A Azero : A.
Lemma AeqDec : Dec (@eq A).
Proof. apply Ceq_Dec. Defined.
End ElementTypeC.
Module MonoidElementTypeC <: MonoidElementType.
Include ElementTypeC.
Definition Aadd := Cadd.
Note that, this explicit annotation is must,
Hint Unfold Aadd : A.
Infix "+" := Aadd : A_scope.
#[export] Instance Aadd_AMonoid : AMonoid Aadd Azero.
Proof. intros. repeat constructor; intros; autounfold with A; ring. Qed.
End MonoidElementTypeC.
Module RingElementTypeC <: RingElementType.
Include MonoidElementTypeC.
Definition Aone : A := C1.
Definition Aopp := Copp.
Definition Amul := Cmul.
Hint Unfold Aone Aadd Aopp Amul : A.
Notation Asub := (fun x y => Aadd x (Aopp y)).
Infix "*" := Amul : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Infix "-" := Asub : A_scope.
#[export] Instance ARing : ARing Aadd Azero Aopp Amul Aone.
Proof. repeat constructor; autounfold with A; intros; ring. Qed.
Add Ring Ring_inst : (make_ring_theory ARing).
End RingElementTypeC.
Module FieldElementTypeC <: FieldElementType.
Include RingElementTypeC.
Definition Ainv := Cinv.
Hint Unfold Ainv : A.
Notation Adiv := (fun x y => Amul x (Ainv y)).
Lemma Aone_neq_Azero : Aone <> Azero.
Proof. cbv in *. auto with C. Qed.
#[export] Instance Field : Field Aadd Azero Aopp Amul Aone Ainv.
Proof.
constructor. apply ARing. intros.
autounfold with A. field. auto.
apply Aone_neq_Azero.
Qed.
Add Field Field_inst : (make_field_theory Field).
End FieldElementTypeC.
Infix "+" := Aadd : A_scope.
#[export] Instance Aadd_AMonoid : AMonoid Aadd Azero.
Proof. intros. repeat constructor; intros; autounfold with A; ring. Qed.
End MonoidElementTypeC.
Module RingElementTypeC <: RingElementType.
Include MonoidElementTypeC.
Definition Aone : A := C1.
Definition Aopp := Copp.
Definition Amul := Cmul.
Hint Unfold Aone Aadd Aopp Amul : A.
Notation Asub := (fun x y => Aadd x (Aopp y)).
Infix "*" := Amul : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Infix "-" := Asub : A_scope.
#[export] Instance ARing : ARing Aadd Azero Aopp Amul Aone.
Proof. repeat constructor; autounfold with A; intros; ring. Qed.
Add Ring Ring_inst : (make_ring_theory ARing).
End RingElementTypeC.
Module FieldElementTypeC <: FieldElementType.
Include RingElementTypeC.
Definition Ainv := Cinv.
Hint Unfold Ainv : A.
Notation Adiv := (fun x y => Amul x (Ainv y)).
Lemma Aone_neq_Azero : Aone <> Azero.
Proof. cbv in *. auto with C. Qed.
#[export] Instance Field : Field Aadd Azero Aopp Amul Aone Ainv.
Proof.
constructor. apply ARing. intros.
autounfold with A. field. auto.
apply Aone_neq_Azero.
Qed.
Add Field Field_inst : (make_field_theory Field).
End FieldElementTypeC.