src/Preamble.v

   1 (*********************************************************************************************************************************)
   2 (* Preamble: miscellaneous notations                                                                                             *)
   3 (*********************************************************************************************************************************)
   4
   5 Require Import Coq.Unicode.Utf8.
   6 Require Import Coq.Classes.RelationClasses.
   7 Require Import Coq.Classes.Morphisms.
   8 Require Import Coq.Setoids.Setoid.
   9 Require Setoid.
  10 Require Import Coq.Strings.String.
  11 Export Coq.Unicode.Utf8.
  12 Export Coq.Classes.RelationClasses.
  13 Export Coq.Classes.Morphisms.
  14 Export Coq.Setoids.Setoid.
  15
  16 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
  17 Generalizable All Variables.
  18
  19 Reserved Notation "a -~- b"                     (at level 10).
  20 Reserved Notation "a ** b"                      (at level 10).
  21 Reserved Notation "?? x"                        (at level 1).
  22 Reserved Notation "a ,, b"                      (at level 50).
  23 Reserved Notation "!! f"                        (at level 3).
  24 Reserved Notation "!` x"                        (at level 2).
  25 Reserved Notation "`! x"                        (at level 2).
  26 Reserved Notation "a  ~=>  b"                   (at level 70, right associativity).
  27 Reserved Notation "H ===> C"                    (at level 100).
  28 Reserved Notation "f >>=>> g"                   (at level 45).
  29 Reserved Notation "a ~~{ C }~~> b"              (at level 100).
  30 Reserved Notation "f <--> g"                    (at level 20).
  31 Reserved Notation "! f"                         (at level 2).
  32 Reserved Notation "? f"                         (at level 2).
  33 Reserved Notation "# f"                         (at level 2).
  34 Reserved Notation "f '⁻¹'"                      (at level 1).
  35 Reserved Notation "a ≅ b"                       (at level 70, right associativity).
  36 Reserved Notation "C 'ᵒᴾ'"                      (at level 1).
  37 Reserved Notation "F \ a"                       (at level 20).
  38 Reserved Notation "f >>> g"                     (at level 45).
  39 Reserved Notation "a ~~ b"                      (at level 54).
  40 Reserved Notation "a ~> b"                      (at level 70, right associativity).
  41 Reserved Notation "a ≃ b"                       (at level 70, right associativity).
  42 Reserved Notation "a ≃≃ b"                      (at level 70, right associativity).
  43 Reserved Notation "a ~~> b"                     (at level 70, right associativity).
  44 Reserved Notation "F  ~~~> G"                   (at level 70, right associativity).
  45 Reserved Notation "F <~~~> G"                   (at level 70, right associativity).
  46 Reserved Notation "a ⊗ b"                       (at level 40).
  47 Reserved Notation "a ⊗⊗ b"                      (at level 40).
  48 Reserved Notation "a ⊕  b"                      (at level 40).
  49 Reserved Notation "a ⊕⊕ b"                      (at level 40).
  50 Reserved Notation "f ⋉ A"                       (at level 40).
  51 Reserved Notation "A ⋊ f"                       (at level 40).
  52 Reserved Notation "- ⋉ A"                       (at level 40).
  53 Reserved Notation "A ⋊ -"                       (at level 40).
  54 Reserved Notation "a *** b"                     (at level 40).
  55 Reserved Notation "a ;; b"                      (at level 45).
  56 Reserved Notation "[# f #]"                     (at level 2).
  57 Reserved Notation "a ---> b"                    (at level 11, right associativity).
  58 Reserved Notation "a <- b"                      (at level 100, only parsing).
  59 Reserved Notation "G |= S"                      (at level 75).
  60 Reserved Notation "F -| G"                      (at level 75).
  61 Reserved Notation "a :: b"                      (at level 60, right associativity).
  62 Reserved Notation "a ++ b"                      (at level 60, right associativity).
  63 Reserved Notation "<[ t @]>"                    (at level 30).
  64 Reserved Notation "<[ t @ n ]>"                 (at level 30).
  65 Reserved Notation "<[ e ]>"                     (at level 30).
  66 Reserved Notation "'Λ' x : t :-> e"             (at level 9, right associativity, x ident).
  67 Reserved Notation "R ==> R' "                   (at level 55, right associativity).
  68 Reserved Notation "f ○ g"                       (at level 100).
  69 Reserved Notation "a ==[ n ]==> b"              (at level 20).
  70 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
  71 Reserved Notation "H /⋯⋯/ C"                    (at level 70).
  72 Reserved Notation "pf1 === pf2"                 (at level 80).
  73 Reserved Notation "a |== b @@ c"                (at level 100).
  74 Reserved Notation "f >>>> g"                    (at level 45).
  75 Reserved Notation "a >>[ n ]<< b"               (at level 100).
  76 Reserved Notation "f **** g"                    (at level 40).
  77 Reserved Notation "C × D"                       (at level 40).
  78 Reserved Notation "C ×× D"                      (at level 45).
  79 Reserved Notation "C ⁽ºᑭ⁾"                      (at level 1).
  80
  81 Reserved Notation "'<[' a '|-' t ']>'"          (at level 35).
  82
  83 Reserved Notation "Γ '∌'    x"                  (at level 10).
  84 Reserved Notation "Γ '∌∌'   x"                  (at level 10).
  85 Reserved Notation "Γ '∋∋'   x : a ∼ b"          (at level 10, x at level 99).
  86 Reserved Notation "Γ '∋'    x : c"              (at level 10, x at level 99).
  87
  88 Reserved Notation "a ⇛ b"                       (at level 55, right associativity).
  89 Reserved Notation "φ₁ →→ φ₂"                    (at level 11, right associativity).
  90 Reserved Notation "a '⊢ᴛy'  b : c"              (at level 20, b at level 99, c at level 80).
  91 Reserved Notation "a '⊢ᴄᴏ'  b : c ∼ d"          (at level 20, b at level 99).
  92 Reserved Notation "Γ '+'    x : c"              (at level 50, x at level 99).
  93 Reserved Notation "Γ '++'   x : a ∼ b"          (at level 50, x at level 99).
  94 Reserved Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"               (at level 11, φ₂ at level 99, right associativity).
  95
  96 Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
  97    (at level 52, past at level 99, present at level 50, succedent at level 50).
  98
  99 Reserved Notation "'η'".
 100 Reserved Notation "'ε'".
 101 Reserved Notation "'★'".
 102
 103 Close Scope nat_scope.  (* so I can redefine '1' *)
 104
 105 Delimit Scope arrow_scope   with arrow.
 106 Delimit Scope biarrow_scope with biarrow.
 107 Delimit Scope garrow_scope  with garrow.
 108
 109 Notation "f ○ g"    := (fun x => f(g(x))).
 110 Notation "?? T"     := (option T).
 111 Notation "a && b"   := (if a then b else false).
 112 Notation "a || b"   := (if a then true else b).
 113
 114 (* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
 115 Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).
 116 Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
 117 Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
 118     (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100).
 119 Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
 120     (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100).
 121
 122 Notation "∀ x y z u q , P" := (forall x y z u q , P)
 123   (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
 124   : type_scope.
 125 Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
 126   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
 127   : type_scope.
 128 Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
 129   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
 130   : type_scope.
 131 Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
 132   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
 133   : type_scope.
 134 Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
 135   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
 136   : type_scope.
 137 Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
 138   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity)
 139   : type_scope.
 140 Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P)
 141   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident,
 142     right associativity)
 143   : type_scope.