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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/complex/CComplex".
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]# *)
39 (*#* * Complex Numbers
40 ** Algebraic structure
44 Section Complex_Numbers.
47 inline cic:/CoRN/complex/CComplex/CC_set.ind.
49 inline cic:/CoRN/complex/CComplex/cc_ap.con.
51 inline cic:/CoRN/complex/CComplex/cc_eq.con.
53 inline cic:/CoRN/complex/CComplex/cc_is_CSetoid.con.
55 inline cic:/CoRN/complex/CComplex/cc_csetoid.con.
57 inline cic:/CoRN/complex/CComplex/cc_plus.con.
59 inline cic:/CoRN/complex/CComplex/cc_mult.con.
61 inline cic:/CoRN/complex/CComplex/cc_zero.con.
63 inline cic:/CoRN/complex/CComplex/cc_one.con.
65 inline cic:/CoRN/complex/CComplex/cc_i.con.
67 inline cic:/CoRN/complex/CComplex/cc_inv.con.
70 Lemma cc_plus_op_proof : (bin_op_wd cc_csetoid cc_plus).
71 Unfold bin_op_wd. Unfold bin_fun_wd.
72 Intros x1 x2 y1 y2. Elim x1. Elim x2. Elim y1. Elim y2.
73 Simpl. Unfold cc_eq. Simpl. Intros.
74 Elim H. Clear H. Intros. Elim H0. Clear H0. Intros.
78 Lemma cc_mult_op_proof : (bin_op_wd cc_csetoid cc_mult).
79 Unfold bin_op_wd. Unfold bin_fun_wd.
80 Intros x1 x2 y1 y2. Elim x1. Elim x2. Elim y1. Elim y2.
81 Simpl. Unfold cc_eq. Simpl. Intros.
82 Elim H. Clear H. Intros. Elim H0. Clear H0. Intros.
86 Lemma cc_inv_op_proof : (un_op_wd cc_csetoid cc_inv).
87 Unfold un_op_wd. Unfold fun_wd.
88 Intros x y. Elim x. Elim y.
89 Simpl. Unfold cc_eq. Simpl. Intros.
90 Elim H. Clear H. Intros.
95 inline cic:/CoRN/complex/CComplex/cc_inv_strext.con.
97 inline cic:/CoRN/complex/CComplex/cc_plus_strext.con.
99 inline cic:/CoRN/complex/CComplex/cc_mult_strext.con.
101 inline cic:/CoRN/complex/CComplex/cc_inv_op.con.
103 inline cic:/CoRN/complex/CComplex/cc_plus_op.con.
105 inline cic:/CoRN/complex/CComplex/cc_mult_op.con.
107 inline cic:/CoRN/complex/CComplex/cc_csg_associative.con.
109 inline cic:/CoRN/complex/CComplex/cc_cr_mult_associative.con.
111 inline cic:/CoRN/complex/CComplex/cc_csemi_grp.con.
113 inline cic:/CoRN/complex/CComplex/cc_cm_proof.con.
115 inline cic:/CoRN/complex/CComplex/cc_cmonoid.con.
117 inline cic:/CoRN/complex/CComplex/cc_cg_proof.con.
119 inline cic:/CoRN/complex/CComplex/cc_cr_dist.con.
121 inline cic:/CoRN/complex/CComplex/cc_cr_non_triv.con.
123 inline cic:/CoRN/complex/CComplex/cc_cgroup.con.
125 inline cic:/CoRN/complex/CComplex/cc_cabgroup.con.
127 inline cic:/CoRN/complex/CComplex/cc_cr_mult_mon.con.
129 inline cic:/CoRN/complex/CComplex/cc_mult_commutes.con.
131 inline cic:/CoRN/complex/CComplex/cc_isCRing.con.
133 inline cic:/CoRN/complex/CComplex/cc_cring.con.
135 inline cic:/CoRN/complex/CComplex/cc_ap_zero.con.
137 inline cic:/CoRN/complex/CComplex/cc_inv_aid.con.
140 If [x [~=] Zero] or [y [~=] Zero], then [x [/] x[^]2 [+] y[^]2 [~=] Zero] or
141 [[--]y[/]x[^]2[+]y[^]2 [~=] Zero].
144 inline cic:/CoRN/complex/CComplex/cc_inv_aid2.con.
147 REMARK KEPT FOR SENTIMENTAL REASONS...
149 This definition seems clever. Even though we *cannot* construct an
150 element of (NonZeros cc_cring) (a Set) by deciding which part of the
151 input (Re or Im) is NonZero (a Prop), we manage to construct the
155 inline cic:/CoRN/complex/CComplex/cc_recip.con.
157 inline cic:/CoRN/complex/CComplex/cc_cfield_proof.con.
159 inline cic:/CoRN/complex/CComplex/cc_Recip_proof.con.
169 inline cic:/CoRN/complex/CComplex/cc_cfield.con.
171 inline cic:/CoRN/complex/CComplex/CC.con.
174 Maps from reals to complex and vice-versa are defined, as well as conjugate,
175 absolute value and the imaginary unit [I] *)
177 inline cic:/CoRN/complex/CComplex/cc_set_CC.con.
179 inline cic:/CoRN/complex/CComplex/cc_IR.con.
181 inline cic:/CoRN/complex/CComplex/CC_conj.con.
184 Definition CC_conj' : CC->CC := [z:CC_set] (CC_set_rec [_:CC_set]CC_set [Re0,Im0:IR] (Build_CC_set Re0 [--]Im0) z).
187 inline cic:/CoRN/complex/CComplex/AbsCC.con.
189 inline cic:/CoRN/complex/CComplex/TwoCC_ap_zero.con.
199 inline cic:/CoRN/complex/CComplex/II.con.
201 (*#* ** Properties of [II] *)
204 Section I_properties.
207 inline cic:/CoRN/complex/CComplex/I_square.con.
210 Hint Resolve I_square: algebra.
213 inline cic:/CoRN/complex/CComplex/I_square'.con.
215 inline cic:/CoRN/complex/CComplex/I_recip_lft.con.
217 inline cic:/CoRN/complex/CComplex/I_recip_rht.con.
219 inline cic:/CoRN/complex/CComplex/mult_I.con.
221 inline cic:/CoRN/complex/CComplex/I_wd.con.
223 (*#* ** Properties of [Re] and [Im] *)
225 inline cic:/CoRN/complex/CComplex/calculate_norm.con.
227 inline cic:/CoRN/complex/CComplex/calculate_Re.con.
229 inline cic:/CoRN/complex/CComplex/calculate_Im.con.
231 inline cic:/CoRN/complex/CComplex/Re_wd.con.
233 inline cic:/CoRN/complex/CComplex/Im_wd.con.
235 inline cic:/CoRN/complex/CComplex/Re_resp_plus.con.
237 inline cic:/CoRN/complex/CComplex/Re_resp_inv.con.
239 inline cic:/CoRN/complex/CComplex/Im_resp_plus.con.
241 inline cic:/CoRN/complex/CComplex/Im_resp_inv.con.
243 inline cic:/CoRN/complex/CComplex/cc_calculate_square.con.
250 Hint Resolve I_square I_square' I_recip_lft I_recip_rht mult_I calculate_norm
251 cc_calculate_square: algebra.
255 Hint Resolve I_wd Re_wd Im_wd: algebra_c.
258 (*#* ** Properties of conjugation *)
261 Section Conj_properties.
264 inline cic:/CoRN/complex/CComplex/CC_conj_plus.con.
266 inline cic:/CoRN/complex/CComplex/CC_conj_mult.con.
269 Hint Resolve CC_conj_mult: algebra.
272 inline cic:/CoRN/complex/CComplex/CC_conj_strext.con.
274 inline cic:/CoRN/complex/CComplex/CC_conj_conj.con.
276 inline cic:/CoRN/complex/CComplex/CC_conj_zero.con.
278 inline cic:/CoRN/complex/CComplex/CC_conj_one.con.
281 Hint Resolve CC_conj_one: algebra.
284 inline cic:/CoRN/complex/CComplex/CC_conj_nexp.con.
291 Hint Resolve CC_conj_plus CC_conj_mult CC_conj_nexp CC_conj_conj
292 CC_conj_zero: algebra.
295 (*#* ** Properties of the real axis *)
298 Section cc_IR_properties.
301 inline cic:/CoRN/complex/CComplex/Re_cc_IR.con.
303 inline cic:/CoRN/complex/CComplex/Im_cc_IR.con.
305 inline cic:/CoRN/complex/CComplex/cc_IR_wd.con.
308 Hint Resolve cc_IR_wd: algebra_c.
311 inline cic:/CoRN/complex/CComplex/cc_IR_resp_ap.con.
313 inline cic:/CoRN/complex/CComplex/cc_IR_mult.con.
316 Hint Resolve cc_IR_mult: algebra.
319 inline cic:/CoRN/complex/CComplex/cc_IR_mult_lft.con.
321 inline cic:/CoRN/complex/CComplex/cc_IR_mult_rht.con.
323 inline cic:/CoRN/complex/CComplex/cc_IR_plus.con.
326 Hint Resolve cc_IR_plus: algebra.
329 inline cic:/CoRN/complex/CComplex/cc_IR_minus.con.
331 inline cic:/CoRN/complex/CComplex/cc_IR_zero.con.
334 Hint Resolve cc_IR_zero: algebra.
337 inline cic:/CoRN/complex/CComplex/cc_IR_one.con.
340 Hint Resolve cc_IR_one: algebra.
343 inline cic:/CoRN/complex/CComplex/cc_IR_nring.con.
345 inline cic:/CoRN/complex/CComplex/cc_IR_nexp.con.
348 End cc_IR_properties.
352 Hint Resolve Re_cc_IR Im_cc_IR: algebra.
356 Hint Resolve cc_IR_wd: algebra_c.
360 Hint Resolve cc_IR_mult cc_IR_nexp cc_IR_mult_lft cc_IR_mult_rht cc_IR_plus
361 cc_IR_minus: algebra.
365 Hint Resolve cc_IR_nring cc_IR_zero: algebra.
368 (*#* ** [CC] has characteristic zero *)
374 inline cic:/CoRN/complex/CComplex/char0_CC.con.
380 inline cic:/CoRN/complex/CComplex/poly_apzero_CC.con.
382 inline cic:/CoRN/complex/CComplex/poly_CC_extensional.con.