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 include "preamble.ma".
19 (* From Arith/Compare *****************************************************)
22 Notation not_eq_sym := sym_not_eq.
25 (* From Bool/Bool *********************************************************)
28 Infix "||" := orb (at level 50, left associativity) : bool_scope.
32 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
35 (* From Init/Datatypes ****************************************************)
42 Notation "x + y" := (sum x y) : type_scope.
46 Add Printing Let prod.
50 Notation "x * y" := (prod x y) : type_scope.
54 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
57 (* From Init/Logic ********************************************************)
60 Notation "~ x" := (not x) : type_scope.
64 Notation "A <-> B" := (iff A B) : type_scope.
68 Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
69 (at level 200) : type_scope.
73 Notation "'exists' x , p" := (ex (fun x => p))
74 (at level 200, x ident) : type_scope.
78 Notation "'exists' x : t , p" := (ex (fun x:t => p))
79 (at level 200, x ident, format "'exists' '/ ' x : t , '/ ' p")
84 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
85 (at level 200, x ident, p at level 200) : type_scope.
89 Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
90 (at level 200, x ident, t at level 200, p at level 200,
91 format "'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']'")
96 Notation "x = y" := (x = y :>_) : type_scope.
100 Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
104 Notation "x <> y" := (x <> y :>_) : type_scope.
107 (* From Init/Notations ****************************************************)
110 Reserved Notation "x <-> y" (at level 95, no associativity).
114 Reserved Notation "x /\ y" (at level 80, right associativity).
118 Reserved Notation "x \/ y" (at level 85, right associativity).
122 Reserved Notation "~ x" (at level 75, right associativity).
126 Reserved Notation "x = y :> T"
127 (at level 70, y at next level, no associativity).
131 Reserved Notation "x = y" (at level 70, no associativity).
135 Reserved Notation "x = y = z"
136 (at level 70, no associativity, y at next level).
140 Reserved Notation "x <> y :> T"
141 (at level 70, y at next level, no associativity).
145 Reserved Notation "x <> y" (at level 70, no associativity).
149 Reserved Notation "x <= y" (at level 70, no associativity).
153 Reserved Notation "x < y" (at level 70, no associativity).
157 Reserved Notation "x >= y" (at level 70, no associativity).
161 Reserved Notation "x > y" (at level 70, no associativity).
165 Reserved Notation "x <= y <= z" (at level 70, y at next level).
169 Reserved Notation "x <= y < z" (at level 70, y at next level).
173 Reserved Notation "x < y < z" (at level 70, y at next level).
177 Reserved Notation "x < y <= z" (at level 70, y at next level).
181 Reserved Notation "x + y" (at level 50, left associativity).
185 Reserved Notation "x - y" (at level 50, left associativity).
189 Reserved Notation "x * y" (at level 40, left associativity).
193 Reserved Notation "x / y" (at level 40, left associativity).
197 Reserved Notation "- x" (at level 35, right associativity).
201 Reserved Notation "/ x" (at level 35, right associativity).
205 Reserved Notation "x ^ y" (at level 30, right associativity).
209 Reserved Notation "( x , y , .. , z )" (at level 0).
213 Reserved Notation "{ x }" (at level 0, x at level 99).
217 Reserved Notation "{ A } + { B }" (at level 50, left associativity).
221 Reserved Notation "A + { B }" (at level 50, left associativity).
225 Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
229 Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
233 Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
237 Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
240 (* From Init/Peano ********************************************************)
243 Infix "+" := plus : nat_scope.
247 Infix "*" := mult : nat_scope.
251 Infix "-" := minus : nat_scope.
255 Infix "<=" := le : nat_scope.
259 Infix "<" := lt : nat_scope.
263 Infix ">=" := ge : nat_scope.
267 Infix ">" := gt : nat_scope.
271 Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
275 Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
279 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
283 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
286 (* From Init/Specif *******************************************************)
289 Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope.
293 Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
298 Notation "{ x : A & P }" := (sigS (fun x:A => P)) : type_scope.
302 Notation "{ x : A & P & Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
307 Add Printing Let sig.
311 Add Printing Let sig2.
315 Add Printing Let sigS.
319 Add Printing Let sigS2.
323 Add Printing If sumbool.
327 Add Printing If sumor.
330 (* From Lists/List ********************************************************)
333 Infix "::" := cons (at level 60, right associativity) : list_scope.
337 Infix "++" := app (right associativity, at level 60) : list_scope.
341 Infix "::" := cons (at level 60, right associativity) : list_scope.
345 Infix "++" := app (right associativity, at level 60) : list_scope.
348 (* From Num/Leibniz/EqAxioms **********************************************)
351 Grammar constr constr1 :=
352 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
358 equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ].
361 (* From Num/Leibniz/NSyntax ***********************************************)
380 Grammar constr lassoc_constr4 :=
382 [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
386 (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
387 | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
389 | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
396 equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
400 sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
404 (* From Num/Nat/NSyntax ***************************************************)
423 Grammar constr lassoc_constr4 :=
425 [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
429 (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
430 | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
432 | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
439 sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
443 (* From Num/EqParams ******************************************************)
446 Grammar constr constr1 :=
447 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
453 equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
457 (* From Num/NSyntax *******************************************************)
460 Infix 6 "<" lt V8only 70.
464 Infix 6 "<=" le V8only 70.
468 Infix 6 ">" gt V8only 70.
472 Infix 6 ">=" ge V8only 70.
476 Grammar constr lassoc_constr4 :=
478 [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
482 (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
483 | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
485 | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
492 sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
496 (* From Num/NeqDef ********************************************************)
499 Infix 6 "<>" neq V8only 70.
502 (* From Num/NeqParams *****************************************************)
505 Infix 6 "<>" neq V8only 70.
508 (* From Reals/RIneq *******************************************************)
511 Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
512 with minus := Rminus div := Rdiv.
515 (* From Reals/Ranalysis1 **************************************************)
518 Infix "+" := plus_fct : Rfun_scope.
522 Notation "- x" := (opp_fct x) : Rfun_scope.
526 Infix "*" := mult_fct : Rfun_scope.
530 Infix "-" := minus_fct : Rfun_scope.
534 Infix "/" := div_fct : Rfun_scope.
538 Notation Local "f1 'o' f2" := (comp f1 f2)
539 (at level 20, right associativity) : Rfun_scope.
543 Notation "/ x" := (inv_fct x) : Rfun_scope.
546 (* From Reals/Rdefinitions ************************************************)
549 Infix "+" := Rplus : R_scope.
553 Infix "*" := Rmult : R_scope.
557 Notation "- x" := (Ropp x) : R_scope.
561 Notation "/ x" := (Rinv x) : R_scope.
565 Infix "<" := Rlt : R_scope.
569 Infix "-" := Rminus : R_scope.
573 Infix "/" := Rdiv : R_scope.
577 Infix "<=" := Rle : R_scope.
581 Infix ">=" := Rge : R_scope.
585 Infix ">" := Rgt : R_scope.
589 Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
593 Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
597 Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
601 Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.
604 (* From Reals/Rfunctions **************************************************)
607 Infix "^" := pow : R_scope.
611 Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
614 (* From Reals/Rpower ******************************************************)
617 Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
620 (* From Reals/Rtopology ***************************************************)
623 Infix "=_D" := eq_Dom (at level 70, no associativity).
626 (* From Setoids/Setoid ****************************************************)
629 Add Setoid Prop iff Prop_S.
632 (* From Wellfounded/Disjoint_Union ****************************************)
635 Notation Le_AsB := (le_AsB A B leA leB).
638 (* From Wellfounded/Lexicographic_Product *********************************)
641 Notation LexProd := (lexprod A B leA leB).
645 Notation Symprod := (symprod A B leA leB).
649 Notation SwapProd := (swapprod A R).
652 (* From Wellfounded/Union *************************************************)
655 Notation Union := (union A R1 R2).
658 (* From Wellfounded/Lexicographic_Exponentiation **************************)
661 Notation Power := (Pow A leA).
665 Notation Lex_Exp := (lex_exp A leA).
669 Notation ltl := (Ltl A leA).
673 Notation Descl := (Desc A leA).
677 Notation List := (list A).
681 Notation Nil := (nil (A:=A)).
685 Notation Cons := (cons (A:=A)).
689 Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
692 (* From Wellfounded/Transitive_Closure ************************************)
695 Notation trans_clos := (clos_trans A R).
698 (* From ZArith/Zdiv *******************************************************)
701 Infix "/" := Zdiv : Z_scope.
705 Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
708 (* From ZArith/Zpower *****************************************************)
711 Infix "^" := Zpower : Z_scope.
715 Infix "^" := Zpower : Z_scope.
718 (* From ZArith/BinInt *****************************************************)
721 Infix "+" := Zplus : Z_scope.
725 Notation "- x" := (Zopp x) : Z_scope.
729 Infix "-" := Zminus : Z_scope.
733 Infix "*" := Zmult : Z_scope.
737 Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
741 Infix "<=" := Zle : Z_scope.
745 Infix "<" := Zlt : Z_scope.
749 Infix ">=" := Zge : Z_scope.
753 Infix ">" := Zgt : Z_scope.
757 Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
761 Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
765 Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
769 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
772 (* From ZArith/Znumtheory *************************************************)
775 Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
778 (* From NArith/BinNat *****************************************************)
781 Infix "+" := Nplus : N_scope.
785 Infix "*" := Nmult : N_scope.
789 Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
792 (* From NArith/BinPos *****************************************************)
795 Infix "+" := Pplus : positive_scope.
799 Infix "-" := Pminus : positive_scope.
803 Infix "*" := Pmult : positive_scope.
807 Infix "/" := Pdiv2 : positive_scope.
811 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.