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 40).
  20 Reserved Notation "a ;; b"                      (at level 45).
  21
  22 Reserved Notation "a -~- b"                     (at level 10).
  23 Reserved Notation "pf1 === pf2"                 (at level 80).
  24 Reserved Notation "?? x"                        (at level 1).
  25 Reserved Notation "a ,, b"                      (at level 50).
  26 Reserved Notation "!! f"                        (at level 3).
  27 Reserved Notation "!` x"                        (at level 2).
  28 Reserved Notation "`! x"                        (at level 2).
  29 Reserved Notation "a  ~=>  b"                   (at level 70, right associativity).
  30 Reserved Notation "H ===> C"                    (at level 100).
  31 Reserved Notation "f >>=>> g"                   (at level 45).
  32 Reserved Notation "a ~~{ C }~~> b"              (at level 100).
  33 Reserved Notation "f <--> g"                    (at level 20).
  34 Reserved Notation "! f"                         (at level 2).
  35 Reserved Notation "? f"                         (at level 2).
  36 Reserved Notation "# f"                         (at level 2).
  37 Reserved Notation "f '⁻¹'"                      (at level 1).
  38 Reserved Notation "a ≅ b"                       (at level 70, right associativity).
  39 Reserved Notation "C 'ᵒᴾ'"                      (at level 1).
  40 Reserved Notation "F \ a"                       (at level 20).
  41 Reserved Notation "f >>> g"                     (at level 45).
  42 Reserved Notation "a ~~ b"                      (at level 54).
  43 Reserved Notation "a ~> b"                      (at level 70, right associativity).
  44 Reserved Notation "a ≃ b"                       (at level 70, right associativity).
  45 Reserved Notation "a ≃≃ b"                      (at level 70, right associativity).
  46 Reserved Notation "a ~~> b"                     (at level 70, right associativity).
  47 Reserved Notation "F  ~~~> G"                   (at level 70, right associativity).
  48 Reserved Notation "F <~~~> G"                   (at level 70, right associativity).
  49 Reserved Notation "a ⊗ b"                       (at level 40).
  50 Reserved Notation "a ⊗⊗ b"                      (at level 40).
  51 Reserved Notation "a ⊕  b"                      (at level 40).
  52 Reserved Notation "a ⊕⊕ b"                      (at level 40).
  53 Reserved Notation "f ⋉ A"                       (at level 40).
  54 Reserved Notation "A ⋊ f"                       (at level 40).
  55 Reserved Notation "- ⋉ A"                       (at level 40).
  56 Reserved Notation "A ⋊ -"                       (at level 40).
  57 Reserved Notation "a *** b"                     (at level 40).
  58 Reserved Notation "[# f #]"                     (at level 2).
  59 Reserved Notation "a ---> b"                    (at level 11, right associativity).
  60 Reserved Notation "a <- b"                      (at level 100, only parsing).
  61 Reserved Notation "G |= S"                      (at level 75).
  62 Reserved Notation "F -| G"                      (at level 75).
  63 Reserved Notation "a :: b"                      (at level 60, right associativity).
  64 Reserved Notation "a ++ b"                      (at level 60, right associativity).
  65 Reserved Notation "<[ t @]>"                    (at level 30).
  66 Reserved Notation "<[ t @ n ]>"                 (at level 30).
  67 Reserved Notation "<[ e ]>"                     (at level 30).
  68 Reserved Notation "'Λ' x : t :-> e"             (at level 9, right associativity, x ident).
  69 Reserved Notation "R ==> R' "                   (at level 55, right associativity).
  70 Reserved Notation "f ○ g"                       (at level 100).
  71 Reserved Notation "a ==[ n ]==> b"              (at level 20).
  72 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
  73 Reserved Notation "H /⋯⋯/ C"                    (at level 70).
  74 Reserved Notation "a |== b @@ c"                (at level 100).
  75 Reserved Notation "f >>>> g"                    (at level 45).
  76 Reserved Notation "a >>[ n ]<< b"               (at level 100).
  77 Reserved Notation "f **** g"                    (at level 40).
  78 Reserved Notation "C × D"                       (at level 40).
  79 Reserved Notation "C ×× D"                      (at level 45).
  80 Reserved Notation "C ⁽ºᑭ⁾"                      (at level 1).
  81
  82 Reserved Notation "'<[' a '|-' t ']>'"          (at level 35).
  83
  84 Reserved Notation "Γ '∌'    x"                  (at level 10).
  85 Reserved Notation "Γ '∌∌'   x"                  (at level 10).
  86 Reserved Notation "Γ '∋∋'   x : a ∼ b"          (at level 10, x at level 99).
  87 Reserved Notation "Γ '∋'    x : c"              (at level 10, x at level 99).
  88
  89 Reserved Notation "a ⇛ b"                       (at level 55, right associativity).
  90 Reserved Notation "φ₁ →→ φ₂"                    (at level 11, right associativity).
  91 Reserved Notation "a '⊢ᴛy'  b : c"              (at level 20, b at level 99, c at level 80).
  92 Reserved Notation "a '⊢ᴄᴏ'  b : c ∼ d"          (at level 20, b at level 99).
  93 Reserved Notation "Γ '+'    x : c"              (at level 50, x at level 99).
  94 Reserved Notation "Γ '++'   x : a ∼ b"          (at level 50, x at level 99).
  95 Reserved Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"               (at level 11, φ₂ at level 99, right associativity).
  96
  97 Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
  98    (at level 52, past at level 99, present at level 50, succedent at level 50).
  99
 100 Reserved Notation "'η'".
 101 Reserved Notation "'ε'".
 102 Reserved Notation "'★'".
 103
 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 Notation "a && b"   := (if a then b else false).
 113 Notation "a || b"   := (if a then true else b).
 114
 115 (* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
 116 Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).
 117 Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
 118 Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
 119     (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).
 120 Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
 121     (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).
 122
 123 Notation "∀ x y z u q , P" := (forall x y z u q , P)
 124   (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
 125   : type_scope.
 126 Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
 127   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
 128   : type_scope.
 129 Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
 130   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
 131   : type_scope.
 132 Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
 133   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
 134   : type_scope.
 135 Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
 136   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
 137   : type_scope.
 138 Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
 139   (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)
 140   : type_scope.
 141 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)
 142   (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,
 143     right associativity)
 144   : type_scope.