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.
Delimit Scope stdpp_scope with stdpp.
Global Open Scope stdpp_scope.
Global Open Scope stdpp_scope.
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}).
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.
(* No Hint Mode set because of Coq bug 14441. Global Hint Mode Equiv ! : typeclass_instances. *)
(* No Hint Mode set because of Coq bug 14441. Global Hint Mode Equiv ! : typeclass_instances. *)
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.
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 := (=).
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.
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.
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 Total {A} (R : relation A) := total x y : R x y ∨ R y x.
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.
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.
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 Total {A} (R : relation A) := total x y : R x y ∨ R y x.
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.
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.
Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
fix go l1 l2 :=
match l1, l2 with x1 :: l1, x2 :: l2 ⇒ f x1 x2 :: go l1 l2 | _ , _ ⇒ [::] end.
Notation zip := (zip_with pair).
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.
Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope.
Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope.
Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
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.
Notation "∅" := empty (format "∅") : stdpp_scope.
Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
fix go l1 l2 :=
match l1, l2 with x1 :: l1, x2 :: l2 ⇒ f x1 x2 :: go l1 l2 | _ , _ ⇒ [::] end.
Notation zip := (zip_with pair).
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.
Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope.
Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope.
Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
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.