Library UniMath.Foundations.Init

Initial setup unrelated to Univalent Foundations

Require Export Coq.Init.Logic.

Require Export Coq.Init.Notations.

Notations

Notation "'∏' x .. y , P" := ( x, .. ( y, P) ..)
  (at level 200, x binder, y binder, right associativity) : type_scope.

Notation "'λ' x .. y , t" := (fun x ⇒ .. (fun yt) ..)
  (at level 200, x binder, y binder, right associativity).

Notation "A -> B" := ( (_ : A), B) : type_scope.

Notation "X <- Y" := (Y X) (at level 90, only parsing, left associativity) : type_scope.

Notation "x → y" := (x y)
  (at level 99, y at level 200, right associativity): type_scope.

Reserved notations

Reserved Notation "x :: y" (at level 60, right associativity).
Reserved Notation "x ++ y" (at level 60, right associativity).
Reserved Notation "p # x" (right associativity, at level 65, only parsing).

Reserved Notation "a ╝ b" (at level 70, no associativity).

Reserved Notation "X ≃ Y" (at level 80, no associativity).

Reserved Notation "p #' x" (right associativity, at level 65, only parsing).

Reserved Notation "f ~ g" (at level 70, no associativity).

Reserved Notation "p @ q" (at level 60, right associativity).

Reserved Notation "'¬¬' X" (at level 35, right associativity).

Reserved Notation "x != y" (at level 70).

Reserved Notation "'¬' X" (at level 35, right associativity).

Reserved Notation "A × B" (at level 75, right associativity).

Reserved Notation "C ⟦ a , b ⟧" (at level 49, right associativity).

Reserved Notation "⟦ a ⟧" (at level 48, left associativity).

Reserved Notation "f ;; g" (at level 50, left associativity, only parsing).
Reserved Notation "g ∘ f" (at level 40, left associativity).

Reserved Notation "f · g" (at level 40, left associativity).

Reserved Notation "a --> b" (at level 55).

Reserved Notation "! p " (at level 50, left associativity).


Reserved Notation "p #' x" (right associativity, at level 65, only parsing).

Reserved Notation "C '^op'" (at level 3, format "C ^op").

Reserved Notation "q '^-1'" (at level 10).

Reserved Notation "a <-- b" (at level 55).

Reserved Notation "[ C , D ]" .

Reserved Notation "C [ a , b ]" (at level 50, left associativity).

Reserved Notation "X ⟶ Y" (at level 39).

Reserved Notation "X ⟹ Y" (at level 39).

Reserved Notation "F ∙ G" (at level 35).


Reserved Notation "X ⊗ Y" (at level 40, left associativity).

Reserved Notation "F ◾ b" (at level 36, left associativity).

Reserved Notation "F ▭ f" (at level 36, left associativity).

Reserved Notation "A ⇒ B" (at level 95, right associativity).

Reserved Notation "X ⇐ c" (at level 94, left associativity).

Reserved Notation "x ⟲ f" (at level 50, left associativity).

Reserved Notation "q ⟳ x" (at level 50, left associativity).

Reserved Notation "p ◽ b" (at level 36).

Reserved Notation "xe ⟲⟲ p" (at level 50, left associativity).

Reserved Notation "r \\ x" (at level 50, left associativity).

Reserved Notation "x // r" (at level 50, left associativity).

Reserved Notation "X ⨿ Y" (at level 50, left associativity).

Reserved Notation "x ,, y" (at level 60, right associativity).

Reserved Notation "A ⊕ B" (at level 50, left associativity).

Reserved Notation "A ↣ B" (at level 50).

Reserved Notation "B ↠ C" (at level 50).

Tactics

Ltac contradicts a b := solve [ induction (a b) | induction (b a) ].

A few more tactics, thanks go to Jason Gross

Ltac simple_rapply p :=
  simple refine p ||
  simple refine (p _) ||
  simple refine (p _ _) ||
  simple refine (p _ _ _) ||
  simple refine (p _ _ _ _) ||
  simple refine (p _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).

Tactic Notation "use" uconstr(p) := simple_rapply p.

Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
  simple refine (let name := (_ : type) in _).

Ltac exact_op x :=
  let T := type of x in
  let G := match goal with |- ?Gconstr:(G) end in
  exact (((λ g:G, g) : T G) x).

Create HintDb rewrite discriminated.
Hint Variables Opaque : rewrite.
Create HintDb typeclass_instances discriminated.