src/Preamble.v-

   1 Require Import Coq.Unicode.Utf8.
   2 Require Import Coq.Classes.RelationClasses.
   3 Require Import Coq.Classes.Morphisms.
   4 Require Import Coq.Setoids.Setoid.
   5 Require Setoid.
   6 Require Import Coq.Strings.String.
   7 Export Coq.Unicode.Utf8.
   8 Export Coq.Classes.RelationClasses.
   9 Export Coq.Classes.Morphisms.
  10 Export Coq.Setoids.Setoid.
  11
  12 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
  13 Generalizable All Variables.
  14
  15 (******************************************************************************)
  16 (* Preamble                                                                   *)
  17 (******************************************************************************)
  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 40).
  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 Notation "a +++ b" := (append a b) (at level 100).
 104 Close Scope nat_scope.  (* so I can redefine '1' *)
 105
 106 Delimit Scope arrow_scope   with arrow.
 107 Delimit Scope biarrow_scope with biarrow.
 108 Delimit Scope garrow_scope  with garrow.
 109
 110 Notation "f ○ g"    := (fun x => f(g(x))).
 111 Notation "?? T"     := (option T).
 112
 113 (* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
 114 Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).
 115 Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
 116 Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
 117     (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).
 118 Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
 119     (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).
 120
 121 Notation "∀ x y z u q , P" := (forall x y z u q , P)
 122   (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
 123   : type_scope.
 124 Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
 125   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
 126   : type_scope.
 127 Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
 128   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
 129   : type_scope.
 130 Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
 131   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
 132   : type_scope.
 133 Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
 134   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
 135   : type_scope.
 136 Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
 137   (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)
 138   : type_scope.
 139 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)
 140   (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,
 141     right associativity)
 142   : type_scope.