Library probsa.util.stdpp

Note: Due to a notation conflict between libraries stdpp and ssreflect, importing stdpp is not possible. As an alternative, the necessary content of library stdpp has been included in this project by means of copy-and-pasting. Those interested in accessing library stdpp directly may do so by visiting the following link: https://gitlab.mpi-sws.org/iris/stdpp.

From discprob.prob Require Export prob countable stochastic_order.
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool ssrfun seq eqtype fintype bigop choice.

Throughout this development we use stdpp_scope for all general purpose notations that do not belong to a more specific scope.

Declare Scope stdpp_scope.
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.

Equality

Introduce some Haskell style like notations.

Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope.
Notation "(.= x )" := (λ y , eq y x) (only parsing) : stdpp_scope.
Notation "(≠)" := (λ x y , x ≠ y) (only parsing) : stdpp_scope.
Notation "( x ≠.)" := (λ y , x ≠ y) (only parsing) : stdpp_scope.
Notation "(.≠ x )" := (λ y , y ≠ x) (only parsing) : stdpp_scope.
Infix "=@{ A }" := (@eq A)
(at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Notation "(≠@{ A } )" := (λ X Y , ¬X =@{A} Y) (only parsing) : stdpp_scope.
Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
(at level 70, only parsing, no associativity) : stdpp_scope.
Global Hint Extern 0 (_ = _) ⇒ reflexivity : core.
Global Hint Extern 100 (_ ≠ _) ⇒ discriminate : core.
Global Instance: ∀ A , PreOrder (=@{A }).

Setoid equality

We define an operational type class for setoid equality, i.e., the "canonical" equivalence for a type. The typeclass is tied to the \equiv symbol. This is based on (Spitters/van der Weegen, 2011).

Class Equiv A := equiv: relation A.

We instruct setoid rewriting to infer equiv as a relation on type A when needed. This allows setoid_rewrite to solve constraints of shape Proper (eq ==> ?R) f using Proper (eq ==> (equiv (A:=A))) f when an equivalence relation is available on type A. We put this instance at level 150 so it does not take precedence over Coq's stdlib instances, favoring inference of eq (all Coq functions are automatically morphisms for eq). We have eq (at 100) < ≡ (at 150) < ⊑ (at 200).

Global Instance equiv_rewrite_relation `{Equiv A} :
  RewriteRelation (@equiv A _) | 150 := {}.

Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Infix "≡@{ A }" := (@equiv A _)
  (at level 70, only parsing, no associativity) : stdpp_scope.

Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope.
Notation "(.≡ X )" := (λ Y , Y ≡ X) (only parsing) : stdpp_scope.
Notation "(≢)" := (λ X Y , ¬X ≡ Y) (only parsing) : stdpp_scope.
Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope.
Notation "( X ≢.)" := (λ Y , X ≢ Y) (only parsing) : stdpp_scope.
Notation "(.≢ X )" := (λ Y , Y ≢ X) (only parsing) : stdpp_scope.

Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y , ¬X ≡@{A} Y) (only parsing) : stdpp_scope.
Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.

The type class LeibnizEquiv collects setoid equalities that coincide with Leibniz equality. We provide the tactic fold_leibniz to transform such setoid equalities into Leibniz equalities, and unfold_leibniz for the reverse.

Class LeibnizEquiv A `{Equiv A} :=
  leibniz_equiv (x y : A) : x ≡ y → x = y.

Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A })} (x y : A) :
  x ≡ y ↔ x = y.

Ltac fold_leibniz := repeat
  match goal with
  | H : context [ _ ≡@{?A} _ ] |- _ ⇒
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
  | |- context [ _ ≡@{?A} _ ] ⇒
    setoid_rewrite (leibniz_equiv_iff (A:=A))
  end.
Ltac unfold_leibniz := repeat
  match goal with
  | H : context [ _ =@{?A} _ ] |- _ ⇒
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
  | |- context [ _ =@{?A} _ ] ⇒
    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
  end.

Definition equivL {A} : Equiv A := (=).

A Params f n instance forces the setoid rewriting mechanism not to rewrite in the first n arguments of the function f. We will declare such instances for all operational type classes in this development.

Global Instance: Params (@equiv) 2 := {}.

The following instance forces setoid_replace to use setoid equality (for types that have an Equiv instance) rather than the standard Leibniz equality.

Global Instance equiv_default_relation `{Equiv A} :
DefaultRelation (≡@{A }) | 3 := {}.
Global Hint Extern 0 (_ ≡ _) ⇒ reflexivity : core.
Global Hint Extern 0 (_ ≡ _) ⇒ symmetry; assumption : core.

Common properties

These operational type classes allow us to refer to common mathematical properties in a generic way. For example, for injectivity of (k ++.) it allows us to write inj (k ++.) instead of app_inv_head k.

Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
  inj x y : S (f x) (f y) → R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
    (S : relation C) (f : A → B → C) : Prop :=
  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop :=
  cancel : ∀ x , S (f (g x)) x.
Class Surj {A B} (R : relation B) (f : A → B) :=
  surj y : ∃ x , R (f x) y.
Class IdemP {A} (R : relation A) (f : A → A → A) : Prop :=
  idemp x : R (f x x) x.
Class Comm {A B} (R : relation A) (f : B → B → A) : Prop :=
  comm x y : R (f x y) (f y x).
Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
  left_id x : R (f i x) x.
Class RightId {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
  right_id x : R (f x i) x.
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
  assoc x y z : R (f x (f y z)) (f (f x y) z).
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
  left_absorb x : R (f i x) i.
Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
  right_absorb x : R (f x i) i.
Class AntiSymm {A} (R S : relation A) : Prop :=
  anti_symm x y : S x y → S y x → R x y.
Class Trichotomy {A} (R : relation A) :=
  trichotomy x y : R x y ∨ x = y ∨ R y x.
Class TrichotomyT {A} (R : relation A) :=
  trichotomyT x y : {R x y } + {x = y } + {R y x }.

Notation Involutive R f := (Cancel R f f).
Lemma involutive {A} {R : relation A} (f : A → A) `{Involutive R f} x :
  R (f (f x)) x.

Global Arguments irreflexivity {_} _ {_} _ _ : assert.
Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
Global Arguments cancel {_ _ _} _ _ {_} _ : assert.
Global Arguments surj {_ _ _} _ {_} _ : assert.
Global Arguments idemp {_ _} _ {_} _ : assert.
Global Arguments comm {_ _ _} _ {_} _ _ : assert.
Global Arguments left_id {_ _} _ _ {_} _ : assert.
Global Arguments right_id {_ _} _ _ {_} _ : assert.
Global Arguments assoc {_ _} _ {_} _ _ _ : assert.
Global Arguments left_absorb {_ _} _ _ {_} _ : assert.
Global Arguments right_absorb {_ _} _ _ {_} _ : assert.
Global Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
Global Arguments trichotomy {_} _ {_} _ _ : assert.
Global Arguments trichotomyT {_} _ {_} _ _ : assert.

Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x.

Operations on sets

We define operational type classes for the traditional operations and relations on sets: the empty set ∅, the union (∪), intersection (∩), and difference (∖), the singleton {[_]}, the subset (⊆) and element of (∈) relation, and disjointess (##).

Class Empty A := empty: A.
Notation "∅" := empty (format "∅") : stdpp_scope.

Class Union A := union: A → A → A.
Global Instance: Params (@union) 2 := {}.
Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
Notation "(∪)" := union (only parsing) : stdpp_scope.
Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
Notation "(.∪ x )" := (λ y , union y x) (only parsing) : stdpp_scope.

Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
Global Arguments union_list _ _ _ !_ / : assert.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope.

Class Intersection A := intersection: A → A → A.
Global Instance: Params (@intersection) 2 := {}.
Infix "∩" := intersection (at level 40) : stdpp_scope.
Notation "(∩)" := intersection (only parsing) : stdpp_scope.
Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
Notation "(.∩ x )" := (λ y , intersection y x) (only parsing) : stdpp_scope.