helm/software/matita/contribs/procedural/CoRN/complex/CComplex.mma

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