matita/contribs/CoRN-Decl/complex/CComplex.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/complex/CComplex".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CComplex.v,v 1.8 2004/04/23 10:00:55 lcf Exp $ *)
  22
  23 (*#* printing Re %\ensuremath{\Re}% #&real;# *)
  24
  25 (*#* printing Im %\ensuremath{\Im}% #&image;# *)
  26
  27 (*#* printing CC %\ensuremath{\mathbb C}% #<b>C</b># *)
  28
  29 (*#* printing II %\ensuremath{\imath}% #i# *)
  30
  31 (*#* printing [+I*] %\ensuremath{+\imath}% *)
  32
  33 (*#* printing AbsCC %\ensuremath{|\cdot|_{\mathbb C}}% *)
  34
  35 (*#* printing CCX %\ensuremath{\mathbb C[X]}% #<b>C</b>[X]# *)
  36
  37 include "reals/NRootIR.ma".
  38
  39 (*#* * Complex Numbers
  40 ** Algebraic structure
  41 *)
  42
  43 (* UNEXPORTED
  44 Section Complex_Numbers
  45 *)
  46
  47 inline "cic:/CoRN/complex/CComplex/CC_set.ind".
  48
  49 inline "cic:/CoRN/complex/CComplex/cc_ap.con".
  50
  51 inline "cic:/CoRN/complex/CComplex/cc_eq.con".
  52
  53 inline "cic:/CoRN/complex/CComplex/cc_is_CSetoid.con".
  54
  55 inline "cic:/CoRN/complex/CComplex/cc_csetoid.con".
  56
  57 inline "cic:/CoRN/complex/CComplex/cc_plus.con".
  58
  59 inline "cic:/CoRN/complex/CComplex/cc_mult.con".
  60
  61 inline "cic:/CoRN/complex/CComplex/cc_zero.con".
  62
  63 inline "cic:/CoRN/complex/CComplex/cc_one.con".
  64
  65 inline "cic:/CoRN/complex/CComplex/cc_i.con".
  66
  67 inline "cic:/CoRN/complex/CComplex/cc_inv.con".
  68
  69 (* not needed anymore
  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.
  75 Split; Algebra.
  76 Qed.
  77
  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.
  83 Split; Algebra.
  84 Qed.
  85
  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.
  91 Split; Algebra.
  92 Qed.
  93 *)
  94
  95 inline "cic:/CoRN/complex/CComplex/cc_inv_strext.con".
  96
  97 inline "cic:/CoRN/complex/CComplex/cc_plus_strext.con".
  98
  99 inline "cic:/CoRN/complex/CComplex/cc_mult_strext.con".
 100
 101 inline "cic:/CoRN/complex/CComplex/cc_inv_op.con".
 102
 103 inline "cic:/CoRN/complex/CComplex/cc_plus_op.con".
 104
 105 inline "cic:/CoRN/complex/CComplex/cc_mult_op.con".
 106
 107 inline "cic:/CoRN/complex/CComplex/cc_csg_associative.con".
 108
 109 inline "cic:/CoRN/complex/CComplex/cc_cr_mult_associative.con".
 110
 111 inline "cic:/CoRN/complex/CComplex/cc_csemi_grp.con".
 112
 113 inline "cic:/CoRN/complex/CComplex/cc_cm_proof.con".
 114
 115 inline "cic:/CoRN/complex/CComplex/cc_cmonoid.con".
 116
 117 inline "cic:/CoRN/complex/CComplex/cc_cg_proof.con".
 118
 119 inline "cic:/CoRN/complex/CComplex/cc_cr_dist.con".
 120
 121 inline "cic:/CoRN/complex/CComplex/cc_cr_non_triv.con".
 122
 123 inline "cic:/CoRN/complex/CComplex/cc_cgroup.con".
 124
 125 inline "cic:/CoRN/complex/CComplex/cc_cabgroup.con".
 126
 127 inline "cic:/CoRN/complex/CComplex/cc_cr_mult_mon.con".
 128
 129 inline "cic:/CoRN/complex/CComplex/cc_mult_commutes.con".
 130
 131 inline "cic:/CoRN/complex/CComplex/cc_isCRing.con".
 132
 133 inline "cic:/CoRN/complex/CComplex/cc_cring.con".
 134
 135 inline "cic:/CoRN/complex/CComplex/cc_ap_zero.con".
 136
 137 inline "cic:/CoRN/complex/CComplex/cc_inv_aid.con".
 138
 139 (*#*
 140 If [x [~=] Zero] or [y [~=] Zero], then  [x [/] x[^]2 [+] y[^]2 [~=] Zero] or
 141 [[--]y[/]x[^]2[+]y[^]2 [~=] Zero].
 142 *)
 143
 144 inline "cic:/CoRN/complex/CComplex/cc_inv_aid2.con".
 145
 146 (*
 147 REMARK KEPT FOR SENTIMENTAL REASONS...
 148
 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
 152 actual function.
 153 *)
 154
 155 inline "cic:/CoRN/complex/CComplex/cc_recip.con".
 156
 157 inline "cic:/CoRN/complex/CComplex/cc_cfield_proof.con".
 158
 159 inline "cic:/CoRN/complex/CComplex/cc_Recip_proof.con".
 160
 161 (* UNEXPORTED
 162 Opaque cc_recip.
 163 *)
 164
 165 (* UNEXPORTED
 166 Opaque cc_inv.
 167 *)
 168
 169 inline "cic:/CoRN/complex/CComplex/cc_cfield.con".
 170
 171 inline "cic:/CoRN/complex/CComplex/CC.con".
 172
 173 (*#*
 174 Maps from reals to complex and vice-versa are defined, as well as conjugate,
 175 absolute value and the imaginary unit [I] *)
 176
 177 inline "cic:/CoRN/complex/CComplex/cc_set_CC.con".
 178
 179 inline "cic:/CoRN/complex/CComplex/cc_IR.con".
 180
 181 inline "cic:/CoRN/complex/CComplex/CC_conj.con".
 182
 183 (* old def
 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).
 185 *)
 186
 187 inline "cic:/CoRN/complex/CComplex/AbsCC.con".
 188
 189 inline "cic:/CoRN/complex/CComplex/TwoCC_ap_zero.con".
 190
 191 (* UNEXPORTED
 192 End Complex_Numbers
 193 *)
 194
 195 (* begin hide *)
 196
 197 (* NOTATION
 198 Notation CCX := (cpoly_cring CC).
 199 *)
 200
 201 (* end hide *)
 202
 203 inline "cic:/CoRN/complex/CComplex/II.con".
 204
 205 (* NOTATION
 206 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
 207 *)
 208
 209 (*#* ** Properties of [II] *)
 210
 211 (* UNEXPORTED
 212 Section I_properties
 213 *)
 214
 215 inline "cic:/CoRN/complex/CComplex/I_square.con".
 216
 217 (* UNEXPORTED
 218 Hint Resolve I_square: algebra.
 219 *)
 220
 221 inline "cic:/CoRN/complex/CComplex/I_square'.con".
 222
 223 inline "cic:/CoRN/complex/CComplex/I_recip_lft.con".
 224
 225 inline "cic:/CoRN/complex/CComplex/I_recip_rht.con".
 226
 227 inline "cic:/CoRN/complex/CComplex/mult_I.con".
 228
 229 inline "cic:/CoRN/complex/CComplex/I_wd.con".
 230
 231 (*#* ** Properties of [Re] and [Im] *)
 232
 233 inline "cic:/CoRN/complex/CComplex/calculate_norm.con".
 234
 235 inline "cic:/CoRN/complex/CComplex/calculate_Re.con".
 236
 237 inline "cic:/CoRN/complex/CComplex/calculate_Im.con".
 238
 239 inline "cic:/CoRN/complex/CComplex/Re_wd.con".
 240
 241 inline "cic:/CoRN/complex/CComplex/Im_wd.con".
 242
 243 inline "cic:/CoRN/complex/CComplex/Re_resp_plus.con".
 244
 245 inline "cic:/CoRN/complex/CComplex/Re_resp_inv.con".
 246
 247 inline "cic:/CoRN/complex/CComplex/Im_resp_plus.con".
 248
 249 inline "cic:/CoRN/complex/CComplex/Im_resp_inv.con".
 250
 251 inline "cic:/CoRN/complex/CComplex/cc_calculate_square.con".
 252
 253 (* UNEXPORTED
 254 End I_properties
 255 *)
 256
 257 (* UNEXPORTED
 258 Hint Resolve I_square I_square' I_recip_lft I_recip_rht mult_I calculate_norm
 259   cc_calculate_square: algebra.
 260 *)
 261
 262 (* UNEXPORTED
 263 Hint Resolve I_wd Re_wd Im_wd: algebra_c.
 264 *)
 265
 266 (*#* ** Properties of conjugation *)
 267
 268 (* UNEXPORTED
 269 Section Conj_properties
 270 *)
 271
 272 inline "cic:/CoRN/complex/CComplex/CC_conj_plus.con".
 273
 274 inline "cic:/CoRN/complex/CComplex/CC_conj_mult.con".
 275
 276 (* UNEXPORTED
 277 Hint Resolve CC_conj_mult: algebra.
 278 *)
 279
 280 inline "cic:/CoRN/complex/CComplex/CC_conj_strext.con".
 281
 282 inline "cic:/CoRN/complex/CComplex/CC_conj_conj.con".
 283
 284 inline "cic:/CoRN/complex/CComplex/CC_conj_zero.con".
 285
 286 inline "cic:/CoRN/complex/CComplex/CC_conj_one.con".
 287
 288 (* UNEXPORTED
 289 Hint Resolve CC_conj_one: algebra.
 290 *)
 291
 292 inline "cic:/CoRN/complex/CComplex/CC_conj_nexp.con".
 293
 294 (* UNEXPORTED
 295 End Conj_properties
 296 *)
 297
 298 (* UNEXPORTED
 299 Hint Resolve CC_conj_plus CC_conj_mult CC_conj_nexp CC_conj_conj
 300   CC_conj_zero: algebra.
 301 *)
 302
 303 (*#* ** Properties of the real axis *)
 304
 305 (* UNEXPORTED
 306 Section cc_IR_properties
 307 *)
 308
 309 inline "cic:/CoRN/complex/CComplex/Re_cc_IR.con".
 310
 311 inline "cic:/CoRN/complex/CComplex/Im_cc_IR.con".
 312
 313 inline "cic:/CoRN/complex/CComplex/cc_IR_wd.con".
 314
 315 (* UNEXPORTED
 316 Hint Resolve cc_IR_wd: algebra_c.
 317 *)
 318
 319 inline "cic:/CoRN/complex/CComplex/cc_IR_resp_ap.con".
 320
 321 inline "cic:/CoRN/complex/CComplex/cc_IR_mult.con".
 322
 323 (* UNEXPORTED
 324 Hint Resolve cc_IR_mult: algebra.
 325 *)
 326
 327 inline "cic:/CoRN/complex/CComplex/cc_IR_mult_lft.con".
 328
 329 inline "cic:/CoRN/complex/CComplex/cc_IR_mult_rht.con".
 330
 331 inline "cic:/CoRN/complex/CComplex/cc_IR_plus.con".
 332
 333 (* UNEXPORTED
 334 Hint Resolve cc_IR_plus: algebra.
 335 *)
 336
 337 inline "cic:/CoRN/complex/CComplex/cc_IR_minus.con".
 338
 339 inline "cic:/CoRN/complex/CComplex/cc_IR_zero.con".
 340
 341 (* UNEXPORTED
 342 Hint Resolve cc_IR_zero: algebra.
 343 *)
 344
 345 inline "cic:/CoRN/complex/CComplex/cc_IR_one.con".
 346
 347 (* UNEXPORTED
 348 Hint Resolve cc_IR_one: algebra.
 349 *)
 350
 351 inline "cic:/CoRN/complex/CComplex/cc_IR_nring.con".
 352
 353 inline "cic:/CoRN/complex/CComplex/cc_IR_nexp.con".
 354
 355 (* UNEXPORTED
 356 End cc_IR_properties
 357 *)
 358
 359 (* UNEXPORTED
 360 Hint Resolve Re_cc_IR Im_cc_IR: algebra.
 361 *)
 362
 363 (* UNEXPORTED
 364 Hint Resolve cc_IR_wd: algebra_c.
 365 *)
 366
 367 (* UNEXPORTED
 368 Hint Resolve cc_IR_mult cc_IR_nexp cc_IR_mult_lft cc_IR_mult_rht cc_IR_plus
 369   cc_IR_minus: algebra.
 370 *)
 371
 372 (* UNEXPORTED
 373 Hint Resolve cc_IR_nring cc_IR_zero: algebra.
 374 *)
 375
 376 (*#* ** [CC] has characteristic zero *)
 377
 378 include "tactics/Transparent_algebra.ma".
 379
 380 inline "cic:/CoRN/complex/CComplex/char0_CC.con".
 381
 382 include "tactics/Opaque_algebra.ma".
 383
 384 inline "cic:/CoRN/complex/CComplex/poly_apzero_CC.con".
 385
 386 inline "cic:/CoRN/complex/CComplex/poly_CC_extensional.con".
 387