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