]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/CoRN.ma
Simplified version.
[helm.git] / matita / contribs / CoRN-Decl / CoRN.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/CoRN".
18
19 (* From algebra/Basics ****************************************************)
20
21 (* NOTATION
22 Notation Pair := (pair (B:=_)).
23 *)
24
25 (* NOTATION
26 Notation Proj1 := (proj1 (B:=_)).
27 *)
28
29 (* NOTATION
30 Notation Proj2 := (proj2 (B:=_)).
31 *)
32
33 coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *).
34
35 (* From algebra/CAbGroups *************************************************)
36
37 coercion cic:/CoRN/algebra/CAbGroups/cag_crr.con 0 (* compounds *).
38
39 (* From algebra/CAbMonoids ************************************************)
40
41 coercion cic:/CoRN/algebra/CAbMonoids/cam_crr.con 0 (* compounds *).
42
43 (* From algebra/CFields ***************************************************)
44
45 coercion cic:/CoRN/algebra/CFields/cf_crr.con 0 (* compounds *).
46
47 (* NOTATION
48 Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
49 *)
50
51 (* NOTATION
52 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
53 *)
54
55 (* NOTATION
56 Infix "{/}" := Fdiv (at level 41, no associativity).
57 *)
58
59 (* From algebra/CGroups ***************************************************)
60
61 coercion cic:/CoRN/algebra/CGroups/cg_crr.con 0 (* compounds *).
62
63 (* NOTATION
64 Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
65 *)
66
67 (* NOTATION
68 Infix "[-]" := cg_minus (at level 50, left associativity).
69 *)
70
71 (* NOTATION
72 Notation "{--} x" := (Finv x) (at level 2, right associativity).
73 *)
74
75 (* NOTATION
76 Infix "{-}" := Fminus (at level 50, left associativity).
77 *)
78
79 (* From algebra/CLogic ****************************************************)
80
81 (* NOTATION
82 Infix "IFF" := Iff (at level 60, right associativity).
83 *)
84
85 (* NOTATION
86 Infix "or" := COr (at level 85, right associativity).
87 *)
88
89 (* NOTATION
90 Infix "and" := CAnd (at level 80, right associativity).
91 *)
92
93 (* NOTATION
94 Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
95   (at level 0, x at level 99) : type_scope.
96 *)
97
98 (* NOTATION
99 Notation "{ x : A  |  P  |  Q }" :=
100   (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
101   type_scope.
102 *)
103
104 (* NOTATION
105 Notation ProjT1 := (proj1_sigT _ _).
106 *)
107
108 (* NOTATION
109 Notation ProjT2 := (proj2_sigT _ _).
110 *)
111
112 (* From algebra/CMonoids **************************************************)
113
114 coercion cic:/CoRN/algebra/CMonoids/cm_crr.con 0 (* compounds *).
115
116 (* NOTATION
117 Notation Zero := (cm_unit _).
118 *)
119
120 (* From algebra/COrdAbs ***************************************************)
121
122 (* NOTATION
123 Notation ZeroR := (Zero:R).
124 *)
125
126 (* NOTATION
127 Notation AbsBig := (absBig _).
128 *)
129
130 (* From algebra/COrdCauchy ************************************************)
131
132 coercion cic:/CoRN/algebra/COrdCauchy/CS_seq.con 0 (* compounds *).
133
134 (* From algebra/COrdFields ************************************************)
135
136 coercion cic:/CoRN/algebra/COrdFields/cof_crr.con 0 (* compounds *).
137
138 (* NOTATION
139 Infix "[<]" := cof_less (at level 70, no associativity).
140 *)
141
142 (* NOTATION
143 Infix "[>]" := greater (at level 70, no associativity).
144 *)
145
146 (* NOTATION
147 Infix "[<=]" := leEq (at level 70, no associativity).
148 *)
149
150 (* NOTATION
151 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
152 *)
153
154 (* NOTATION
155 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
156 *)
157
158 (* NOTATION
159 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
160 *)
161
162 (* NOTATION
163 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
164 *)
165
166 (* NOTATION
167 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
168 *)
169
170 (* NOTATION
171 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
172 *)
173
174 (* NOTATION
175 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
176 *)
177
178 (* NOTATION
179 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
180 *)
181
182 (* NOTATION
183 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
184 *)
185
186 (* NOTATION
187 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
188 *)
189
190 (* NOTATION
191 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
192 *)
193
194 (* NOTATION
195 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
196 *)
197
198 (* From algebra/COrdFields2 ***********************************************)
199
200 (* NOTATION
201 Notation ZeroR := (Zero:R).
202 *)
203
204 (* NOTATION
205 Notation OneR := (One:R).
206 *)
207
208 (* From algebra/CPoly_ApZero **********************************************)
209
210 (* NOTATION
211 Notation RX := (cpoly_cring R).
212 *)
213
214 (* NOTATION
215 Notation RX := (cpoly_cring R).
216 *)
217
218 (* NOTATION
219 Notation RX := (cpoly_cring R).
220 *)
221
222 (* From algebra/CPoly_Degree **********************************************)
223
224 (* NOTATION
225 Notation RX := (cpoly_cring R).
226 *)
227
228 (* NOTATION
229 Notation RX := (cpoly_cring R).
230 *)
231
232 (* NOTATION
233 Notation FX := (cpoly_cring F).
234 *)
235
236 (* From algebra/CPoly_NthCoeff ********************************************)
237
238 (* NOTATION
239 Notation RX := (cpoly_cring R).
240 *)
241
242 (* NOTATION
243 Notation RX := (cpoly_cring R).
244 *)
245
246 (* From algebra/CPolynomials **********************************************)
247
248 (* NOTATION
249 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
250 *)
251
252 (* NOTATION
253 Notation RX := (cpoly_cring CR).
254 *)
255
256 (* NOTATION
257 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
258 *)
259
260 (* NOTATION
261 Notation RX := (cpoly_cring R).
262 *)
263
264 (* NOTATION
265 Notation Cpoly := (cpoly CR).
266 *)
267
268 (* NOTATION
269 Notation Cpoly_zero := (cpoly_zero CR).
270 *)
271
272 (* NOTATION
273 Notation Cpoly_linear := (cpoly_linear CR).
274 *)
275
276 (* NOTATION
277 Notation Cpoly_cring := (cpoly_cring CR).
278 *)
279
280 (* From algebra/CRings ****************************************************)
281
282 coercion cic:/CoRN/algebra/CRings/cr_crr.con 0 (* compounds *).
283
284 (* NOTATION
285 Notation One := (cr_one _).
286 *)
287
288 (* NOTATION
289 Infix "[*]" := cr_mult (at level 40, left associativity).
290 *)
291
292 (* NOTATION
293 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
294 *)
295
296 (* NOTATION
297 Notation Two := (nring 2).
298 *)
299
300 (* NOTATION
301 Notation Three := (nring 3).
302 *)
303
304 (* NOTATION
305 Notation Four := (nring 4).
306 *)
307
308 (* NOTATION
309 Notation Six := (nring 6).
310 *)
311
312 (* NOTATION
313 Notation Eight := (nring 8).
314 *)
315
316 (* NOTATION
317 Notation Twelve := (nring 12).
318 *)
319
320 (* NOTATION
321 Notation Sixteen := (nring 16).
322 *)
323
324 (* NOTATION
325 Notation Nine := (nring 9).
326 *)
327
328 (* NOTATION
329 Notation Eighteen := (nring 18).
330 *)
331
332 (* NOTATION
333 Notation TwentyFour := (nring 24).
334 *)
335
336 (* NOTATION
337 Notation FortyEight := (nring 48).
338 *)
339
340 (* NOTATION
341 Infix "{*}" := Fmult (at level 40, left associativity).
342 *)
343
344 (* NOTATION
345 Infix "{**}" := Fscalmult (at level 40, left associativity).
346 *)
347
348 (* NOTATION
349 Infix "{^}" := Fnth (at level 30, right associativity).
350 *)
351
352 (* From algebra/CSemiGroups ***********************************************)
353
354 coercion cic:/CoRN/algebra/CSemiGroups/csg_crr.con 0 (* compounds *).
355
356 (* NOTATION
357 Infix "[+]" := csg_op (at level 50, left associativity).
358 *)
359
360 (* NOTATION
361 Infix "{+}" := Fplus (at level 50, left associativity).
362 *)
363
364 (* From algebra/CSetoidFun ************************************************)
365
366 (* NOTATION
367 Notation Conj := (conjP _).
368 *)
369
370 coercion cic:/CoRN/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *).
371
372 (* NOTATION
373 Notation BDom := (bpfdom _ _).
374 *)
375
376 coercion cic:/CoRN/algebra/CSetoidFun/pfpfun.con 0 (* compounds *).
377
378 (* NOTATION
379 Notation Dom := (pfdom _).
380 *)
381
382 (* NOTATION
383 Notation Part := (pfpfun _).
384 *)
385
386 (* NOTATION
387 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
388 *)
389
390 (* NOTATION
391 Notation FId := (Fid _).
392 *)
393
394 (* NOTATION
395 Infix "[o]" := Fcomp (at level 65, no associativity).
396 *)
397
398 (* NOTATION
399 Notation Prj1 := (prj1 _ _ _ _).
400 *)
401
402 (* NOTATION
403 Notation Prj2 := (prj2 _ _ _ _).
404 *)
405
406 (* From algebra/CSetoids **************************************************)
407
408 coercion cic:/CoRN/algebra/CSetoids/cs_crr.con 0 (* compounds *).
409
410 (* NOTATION
411 Infix "[=]" := cs_eq (at level 70, no associativity).
412 *)
413
414 (* NOTATION
415 Infix "[#]" := cs_ap (at level 70, no associativity).
416 *)
417
418 (* NOTATION
419 Infix "[~=]" := cs_neq (at level 70, no associativity).
420 *)
421
422 coercion cic:/CoRN/algebra/CSetoids/csp_pred.con 0 (* compounds *).
423
424 coercion cic:/CoRN/algebra/CSetoids/csp'_pred.con 0 (* compounds *).
425
426 coercion cic:/CoRN/algebra/CSetoids/csr_rel.con 0 (* compounds *).
427
428 coercion cic:/CoRN/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *).
429
430 coercion cic:/CoRN/algebra/CSetoids/csf_fun.con 0 (* compounds *).
431
432 coercion cic:/CoRN/algebra/CSetoids/csbf_fun.con 0 (* compounds *).
433
434 coercion cic:/CoRN/algebra/CSetoids/un_op_fun.con 0 (* compounds *).
435
436 coercion cic:/CoRN/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *).
437
438 coercion cic:/CoRN/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *).
439
440 coercion cic:/CoRN/algebra/CSetoids/scs_elem.con 0 (* compounds *).
441
442 (* From algebra/CVectorSpace **********************************************)
443
444 coercion cic:/CoRN/algebra/CVectorSpace/vs_vs.con 0 (* compounds *).
445
446 (* NOTATION
447 Infix "[']" := vs_op (at level 30, no associativity).
448 *)
449
450 (* From algebra/Expon *****************************************************)
451
452 (* NOTATION
453 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
454 *)
455
456 (* From complex/CComplex **************************************************)
457
458 (* NOTATION
459 Notation CCX := (cpoly_cring CC).
460 *)
461
462 (* NOTATION
463 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
464 *)
465
466 (* From fta/CC_Props ******************************************************)
467
468 coercion cic:/CoRN/fta/CC_Props/CC_seq.con 0 (* compounds *).
469
470 (* From fta/FTAreg ********************************************************)
471
472 coercion cic:/CoRN/fta/FTAreg/z_el.con 0 (* compounds *).
473
474 coercion cic:/CoRN/fta/FTAreg/Kntup.con 0 (* compounds *).
475
476 (* From ftc/FTC ***********************************************************)
477
478 (* NOTATION
479 Notation "[-S-] F" := (Fprim F) (at level 20).
480 *)
481
482 (* From ftc/Integral ******************************************************)
483
484 (* NOTATION
485 Notation Integral := (integral _ _ Hab).
486 *)
487
488 (* From ftc/MoreIntervals *************************************************)
489
490 coercion cic:/CoRN/ftc/MoreIntervals/iprop.con 0 (* compounds *).
491
492 (* From ftc/Partitions ****************************************************)
493
494 coercion cic:/CoRN/ftc/Partitions/Pts.con 0 (* compounds *).
495
496 (* From ftc/RefLemma ******************************************************)
497
498 (* NOTATION
499 Notation g := RL_g.
500 *)
501
502 (* NOTATION
503 Notation h := RL_h.
504 *)
505
506 (* NOTATION
507 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
508 *)
509
510 (* NOTATION
511 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
512 *)
513
514 (* NOTATION
515 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
516 *)
517
518 (* From ftc/RefSeparated **************************************************)
519
520 (* NOTATION
521 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
522 *)
523
524 (* NOTATION
525 Notation just2 :=
526   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
527 *)
528
529 (* From ftc/RefSeparating *************************************************)
530
531 (* NOTATION
532 Notation m := RS'_m.
533 *)
534
535 (* NOTATION
536 Notation h := RS'_h.
537 *)
538
539 (* NOTATION
540 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
541 *)
542
543 (* NOTATION
544 Notation just2 :=
545   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
546 *)
547
548 (* From ftc/Rolle *********************************************************)
549
550 (* NOTATION
551 Notation cp := (compact_part a b Hab' d Hd).
552 *)
553
554 (* From ftc/TaylorLemma ***************************************************)
555
556 (* NOTATION
557 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
558 *)
559
560 (* NOTATION
561 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
562 *)
563
564 (* From ftc/WeakIVT *******************************************************)
565
566 (* NOTATION
567 Infix "**" := prodT (at level 20).
568 *)
569
570 (* From metrics/CMetricSpaces *********************************************)
571
572 coercion cic:/CoRN/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
573
574 (* From metrics/CPseudoMSpaces ********************************************)
575
576 coercion cic:/CoRN/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *).
577
578 (* NOTATION
579 Infix "[-d]" := cms_d (at level 68, left associativity).
580 *)
581
582 (* From model/structures/Nsec *********************************************)
583
584 (* NOTATION
585 Infix "{#N}" := ap_nat (no associativity, at level 90).
586 *)
587
588 (* From model/structures/Qsec *********************************************)
589
590 (* NOTATION
591 Infix "{=Q}" := Qeq (no associativity, at level 90).
592 *)
593
594 (* NOTATION
595 Infix "{#Q}" := Qap (no associativity, at level 90).
596 *)
597
598 (* NOTATION
599 Infix "{<Q}" := Qlt (no associativity, at level 90).
600 *)
601
602 (* NOTATION
603 Infix "{+Q}" := Qplus (no associativity, at level 85).
604 *)
605
606 (* NOTATION
607 Infix "{*Q}" := Qmult (no associativity, at level 80).
608 *)
609
610 (* NOTATION
611 Notation "{-Q}" := Qopp (at level 1, left associativity).
612 *)
613
614 coercion cic:/CoRN/model/structures/Qsec/inject_Z.con 0 (* compounds *).
615
616 (* From model/structures/Zsec *********************************************)
617
618 (* NOTATION
619 Infix "{#Z}" := ap_Z (no associativity, at level 90).
620 *)
621
622 coercion cic:/CoRN/model/structures/Zsec/Zpos.con 0 (* compounds *).
623
624 (* From reals/Bridges_LUB *************************************************)
625
626 (* NOTATION
627 Notation "( p , q )" := (pairT p q).
628 *)
629
630 (* From reals/CMetricFields ***********************************************)
631
632 coercion cic:/CoRN/reals/CMetricFields/cmf_crr.con 0 (* compounds *).
633
634 (* NOTATION
635 Notation MAbs := (cmf_abs _).
636 *)
637
638 coercion cic:/CoRN/reals/CMetricFields/MCS_seq.con 0 (* compounds *).
639
640 (* From reals/CReals ******************************************************)
641
642 coercion cic:/CoRN/reals/CReals/crl_crr.con 0 (* compounds *).
643
644 (* From reals/CauchySeq ***************************************************)
645
646 (* NOTATION
647 Notation PartIR := (PartFunct IR).
648 *)
649
650 (* NOTATION
651 Notation ProjIR1 := (prj1 IR _ _ _).
652 *)
653
654 (* NOTATION
655 Notation ProjIR2 := (prj2 IR _ _ _).
656 *)
657
658 (* NOTATION
659 Notation ZeroR := (Zero:IR).
660 *)
661
662 (* NOTATION
663 Notation OneR := (One:IR).
664 *)
665
666 (* From reals/Cauchy_CReals ***********************************************)
667
668 (* NOTATION
669 Notation "'R_COrdField''" := (R_COrdField F).
670 *)
671
672 (* From reals/Intervals ***************************************************)
673
674 (* NOTATION
675 Notation Compact := (compact _ _).
676 *)
677
678 (* NOTATION
679 Notation FRestr := (Frestr (compact_wd _ _ _)).
680 *)
681
682 (* From reals/Q_dense *****************************************************)
683
684 coercion cic:/CoRN/reals/Q_dense/pair_crr.con 0 (* compounds *).
685
686 (* NOTATION
687 Notation "( A , B )" := (pairT A B).
688 *)
689
690 (* From reals/Q_in_CReals *************************************************)
691
692 coercion cic:/CoRN/reals/Q_in_CReals/nat_of_P.con 0 (* compounds *).
693
694 (* From reals/R_morphism **************************************************)
695
696 coercion cic:/CoRN/reals/R_morphism/map.con 0 (* compounds *).
697
698 (* From tactics/FieldReflection *******************************************)
699
700 (* NOTATION
701 Notation II := (interpF F val unop binop pfun).
702 *)
703
704 (* From tactics/GroupReflection *******************************************)
705
706 (* NOTATION
707 Notation II := (interpG G val unop binop pfun).
708 *)
709
710 (* From tactics/RingReflection ********************************************)
711
712 (* NOTATION
713 Notation II := (interpR R val unop binop pfun).
714 *)
715
716 (* From transc/RealPowers *************************************************)
717
718 (* NOTATION
719 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
720 *)
721
722 (* NOTATION
723 Notation "F {!} G" := (FPower F G) (at level 20).
724 *)
725
726 (* From devel/loeb/per/lst2fun ********************************************)
727
728 coercion cic:/CoRN/devel/loeb/per/lst2fun/F_crr.con 0 (* compounds *).
729
730 coercion cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con 0 (* compounds *).
731