1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CComplex.v,v 1.8 2004/04/23 10:00:55 lcf Exp $ *)
21 (*#* printing Re %\ensuremath{\Re}% #ℜ# *)
23 (*#* printing Im %\ensuremath{\Im}% #ℑ# *)
25 (*#* printing CC %\ensuremath{\mathbb C}% #<b>C</b># *)
27 (*#* printing II %\ensuremath{\imath}% #i# *)
29 (*#* printing [+I*] %\ensuremath{+\imath}% *)
31 (*#* printing AbsCC %\ensuremath{|\cdot|_{\mathbb C}}% *)
33 (*#* printing CCX %\ensuremath{\mathbb C[X]}% #<b>C</b>[X]# *)
35 include "reals/NRootIR.ma".
37 (*#* * Complex Numbers
38 ** Algebraic structure
42 Section Complex_Numbers
45 inline procedural "cic:/CoRN/complex/CComplex/CC_set.ind".
47 inline procedural "cic:/CoRN/complex/CComplex/cc_ap.con".
49 inline procedural "cic:/CoRN/complex/CComplex/cc_eq.con".
51 inline procedural "cic:/CoRN/complex/CComplex/cc_is_CSetoid.con".
53 inline procedural "cic:/CoRN/complex/CComplex/cc_csetoid.con".
55 inline procedural "cic:/CoRN/complex/CComplex/cc_plus.con".
57 inline procedural "cic:/CoRN/complex/CComplex/cc_mult.con".
59 inline procedural "cic:/CoRN/complex/CComplex/cc_zero.con".
61 inline procedural "cic:/CoRN/complex/CComplex/cc_one.con".
63 inline procedural "cic:/CoRN/complex/CComplex/cc_i.con".
65 inline procedural "cic:/CoRN/complex/CComplex/cc_inv.con".
68 Lemma cc_plus_op_proof : (bin_op_wd cc_csetoid cc_plus).
69 Unfold bin_op_wd. Unfold bin_fun_wd.
70 Intros x1 x2 y1 y2. Elim x1. Elim x2. Elim y1. Elim y2.
71 Simpl. Unfold cc_eq. Simpl. Intros.
72 Elim H. Clear H. Intros. Elim H0. Clear H0. Intros.
76 Lemma cc_mult_op_proof : (bin_op_wd cc_csetoid cc_mult).
77 Unfold bin_op_wd. Unfold bin_fun_wd.
78 Intros x1 x2 y1 y2. Elim x1. Elim x2. Elim y1. Elim y2.
79 Simpl. Unfold cc_eq. Simpl. Intros.
80 Elim H. Clear H. Intros. Elim H0. Clear H0. Intros.
84 Lemma cc_inv_op_proof : (un_op_wd cc_csetoid cc_inv).
85 Unfold un_op_wd. Unfold fun_wd.
86 Intros x y. Elim x. Elim y.
87 Simpl. Unfold cc_eq. Simpl. Intros.
88 Elim H. Clear H. Intros.
93 inline procedural "cic:/CoRN/complex/CComplex/cc_inv_strext.con".
95 inline procedural "cic:/CoRN/complex/CComplex/cc_plus_strext.con".
97 inline procedural "cic:/CoRN/complex/CComplex/cc_mult_strext.con".
99 inline procedural "cic:/CoRN/complex/CComplex/cc_inv_op.con".
101 inline procedural "cic:/CoRN/complex/CComplex/cc_plus_op.con".
103 inline procedural "cic:/CoRN/complex/CComplex/cc_mult_op.con".
105 inline procedural "cic:/CoRN/complex/CComplex/cc_csg_associative.con".
107 inline procedural "cic:/CoRN/complex/CComplex/cc_cr_mult_associative.con".
109 inline procedural "cic:/CoRN/complex/CComplex/cc_csemi_grp.con".
111 inline procedural "cic:/CoRN/complex/CComplex/cc_cm_proof.con".
113 inline procedural "cic:/CoRN/complex/CComplex/cc_cmonoid.con".
115 inline procedural "cic:/CoRN/complex/CComplex/cc_cg_proof.con".
117 inline procedural "cic:/CoRN/complex/CComplex/cc_cr_dist.con".
119 inline procedural "cic:/CoRN/complex/CComplex/cc_cr_non_triv.con".
121 inline procedural "cic:/CoRN/complex/CComplex/cc_cgroup.con".
123 inline procedural "cic:/CoRN/complex/CComplex/cc_cabgroup.con".
125 inline procedural "cic:/CoRN/complex/CComplex/cc_cr_mult_mon.con".
127 inline procedural "cic:/CoRN/complex/CComplex/cc_mult_commutes.con".
129 inline procedural "cic:/CoRN/complex/CComplex/cc_isCRing.con".
131 inline procedural "cic:/CoRN/complex/CComplex/cc_cring.con".
133 inline procedural "cic:/CoRN/complex/CComplex/cc_ap_zero.con".
135 inline procedural "cic:/CoRN/complex/CComplex/cc_inv_aid.con".
138 If [x [~=] Zero] or [y [~=] Zero], then [x [/] x[^]2 [+] y[^]2 [~=] Zero] or
139 [[--]y[/]x[^]2[+]y[^]2 [~=] Zero].
142 inline procedural "cic:/CoRN/complex/CComplex/cc_inv_aid2.con".
145 REMARK KEPT FOR SENTIMENTAL REASONS...
147 This definition seems clever. Even though we *cannot* construct an
148 element of (NonZeros cc_cring) (a Set) by deciding which part of the
149 input (Re or Im) is NonZero (a Prop), we manage to construct the
153 inline procedural "cic:/CoRN/complex/CComplex/cc_recip.con".
155 inline procedural "cic:/CoRN/complex/CComplex/cc_cfield_proof.con".
157 inline procedural "cic:/CoRN/complex/CComplex/cc_Recip_proof.con".
167 inline procedural "cic:/CoRN/complex/CComplex/cc_cfield.con".
169 inline procedural "cic:/CoRN/complex/CComplex/CC.con".
172 Maps from reals to complex and vice-versa are defined, as well as conjugate,
173 absolute value and the imaginary unit [I] *)
175 inline procedural "cic:/CoRN/complex/CComplex/cc_set_CC.con".
177 inline procedural "cic:/CoRN/complex/CComplex/cc_IR.con".
179 inline procedural "cic:/CoRN/complex/CComplex/CC_conj.con".
182 Definition CC_conj' : CC->CC := [z:CC_set] (CC_set_rec [_:CC_set]CC_set [Re0,Im0:IR] (Build_CC_set Re0 [--]Im0) z).
185 inline procedural "cic:/CoRN/complex/CComplex/AbsCC.con".
187 inline procedural "cic:/CoRN/complex/CComplex/TwoCC_ap_zero.con".
196 Notation CCX := (cpoly_cring CC).
201 inline procedural "cic:/CoRN/complex/CComplex/II.con".
204 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
207 (*#* ** Properties of [II] *)
213 inline procedural "cic:/CoRN/complex/CComplex/I_square.con".
216 Hint Resolve I_square: algebra.
219 inline procedural "cic:/CoRN/complex/CComplex/I_square'.con".
221 inline procedural "cic:/CoRN/complex/CComplex/I_recip_lft.con".
223 inline procedural "cic:/CoRN/complex/CComplex/I_recip_rht.con".
225 inline procedural "cic:/CoRN/complex/CComplex/mult_I.con".
227 inline procedural "cic:/CoRN/complex/CComplex/I_wd.con".
229 (*#* ** Properties of [Re] and [Im] *)
231 inline procedural "cic:/CoRN/complex/CComplex/calculate_norm.con".
233 inline procedural "cic:/CoRN/complex/CComplex/calculate_Re.con".
235 inline procedural "cic:/CoRN/complex/CComplex/calculate_Im.con".
237 inline procedural "cic:/CoRN/complex/CComplex/Re_wd.con".
239 inline procedural "cic:/CoRN/complex/CComplex/Im_wd.con".
241 inline procedural "cic:/CoRN/complex/CComplex/Re_resp_plus.con".
243 inline procedural "cic:/CoRN/complex/CComplex/Re_resp_inv.con".
245 inline procedural "cic:/CoRN/complex/CComplex/Im_resp_plus.con".
247 inline procedural "cic:/CoRN/complex/CComplex/Im_resp_inv.con".
249 inline procedural "cic:/CoRN/complex/CComplex/cc_calculate_square.con".
256 Hint Resolve I_square I_square' I_recip_lft I_recip_rht mult_I calculate_norm
257 cc_calculate_square: algebra.
261 Hint Resolve I_wd Re_wd Im_wd: algebra_c.
264 (*#* ** Properties of conjugation *)
267 Section Conj_properties
270 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_plus.con".
272 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_mult.con".
275 Hint Resolve CC_conj_mult: algebra.
278 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_strext.con".
280 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_conj.con".
282 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_zero.con".
284 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_one.con".
287 Hint Resolve CC_conj_one: algebra.
290 inline procedural "cic:/CoRN/complex/CComplex/CC_conj_nexp.con".
297 Hint Resolve CC_conj_plus CC_conj_mult CC_conj_nexp CC_conj_conj
298 CC_conj_zero: algebra.
301 (*#* ** Properties of the real axis *)
304 Section cc_IR_properties
307 inline procedural "cic:/CoRN/complex/CComplex/Re_cc_IR.con".
309 inline procedural "cic:/CoRN/complex/CComplex/Im_cc_IR.con".
311 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_wd.con".
314 Hint Resolve cc_IR_wd: algebra_c.
317 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_resp_ap.con".
319 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_mult.con".
322 Hint Resolve cc_IR_mult: algebra.
325 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_mult_lft.con".
327 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_mult_rht.con".
329 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_plus.con".
332 Hint Resolve cc_IR_plus: algebra.
335 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_minus.con".
337 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_zero.con".
340 Hint Resolve cc_IR_zero: algebra.
343 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_one.con".
346 Hint Resolve cc_IR_one: algebra.
349 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_nring.con".
351 inline procedural "cic:/CoRN/complex/CComplex/cc_IR_nexp.con".
358 Hint Resolve Re_cc_IR Im_cc_IR: algebra.
362 Hint Resolve cc_IR_wd: algebra_c.
366 Hint Resolve cc_IR_mult cc_IR_nexp cc_IR_mult_lft cc_IR_mult_rht cc_IR_plus
367 cc_IR_minus: algebra.
371 Hint Resolve cc_IR_nring cc_IR_zero: algebra.
374 (*#* ** [CC] has characteristic zero *)
376 include "tactics/Transparent_algebra.ma".
378 inline procedural "cic:/CoRN/complex/CComplex/char0_CC.con".
380 include "tactics/Opaque_algebra.ma".
382 inline procedural "cic:/CoRN/complex/CComplex/poly_apzero_CC.con".
384 inline procedural "cic:/CoRN/complex/CComplex/poly_CC_extensional.con".