Library Obs.notations

Require Export Eqdep Setoid Morphisms.
Set Implicit Arguments.

Notation " $ o " := (proj1_sig o) (at level 0).
Infix " ∘ " := Basics.compose (at level 40).
Infix " ⊕ " := Nat.max (at level 40).

Create HintDb simpl_typeclasses.
Ltac rsimpl := repeat autorewrite with simpl_typeclasses||simpl.
Tactic Notation "rsimpl" "in" hyp(h) :=
(repeat autorewrite with simpl_typeclasses in h||simpl in h).
Tactic Notation "rsimpl" "in" "*" :=
(repeat autorewrite with simpl_typeclasses in × ||simpl in × ).

Typeclass and notation for size functions.

Class Size (A : Type) := size : A → nat.
Notation " ⎢ x ⎥ " := (size x).

A partial order is a subrelation of its equivalence relation.

Global Instance PartialOrder_subrelation {X e o} `{PartialOrder X e o} :
subrelation e o.

Typeclass and notation for satisfaction relations.

Class Satisfaction (A B : Type) := satisfies : A → B → Prop.
Infix " ⊨ " := satisfies (at level 10).

Section SemEquiv.
Context {A B : Type}.
Context {sat : Satisfaction B A}.

Semantic equivalence derived from satisfaction relation.

  Definition sequiv: relation A :=
    (fun a b : A ⇒ ∀ c : B, c ⊨ a ↔ c ⊨ b).
  Notation " e ≃ f " := (sequiv e f) (at level 80).

  Global Instance sequiv_Equiv : Equivalence sequiv.

Semantic order relation derived from satisfaction relation.

  Definition ssmaller : relation A :=
    (fun a b ⇒ ∀ c, c ⊨ a → c ⊨ b).
  Notation " e ≲ f " := (ssmaller e f) (at level 80).

  Global Instance ssmaller_PreOrder : PreOrder ssmaller.

  Global Instance ssmaller_PartialOrder : PartialOrder sequiv ssmaller.

  Global Instance satisfies_proper b :
    Proper (sequiv ==> iff) (satisfies b).

  Global Instance satisfies_inf b :
    Proper (ssmaller ==> Basics.impl) (satisfies b).
End SemEquiv.
Notation " e ≲ f " := (ssmaller e f) (at level 80).

Notation " e ≃ f " := (sequiv e f) (at level 80).