phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/base.v *)
Notation "(##*)"
:= (Forall2 (##)) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Class Filter A B
:= filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
(* stdpp/base.v *)
Class UpClose A B
:= up_close : A → B.
(* stdpp/base.v *)
Notation "↑ x"
:= (up_close x) (at level 20, format "↑ x").
(* stdpp/base.v *)
(* We define operational type classes for the monadic operations bind, join
and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
Class MRet (M : Type → Type)
:= mret: ∀ {A}, A → M A.
(* stdpp/base.v *)
Instance : Params (@mret) 3
:= {}.
(* stdpp/base.v *)
Class MBind (M : Type → Type)
:= mbind : ∀ {A B}, (A → M B) → M A → M B.
(* stdpp/base.v *)
Instance : Params (@mbind) 4
:= {}.
(* stdpp/base.v *)
Class MJoin (M : Type → Type)
:= mjoin: ∀ {A}, M (M A) → M A.
(* stdpp/base.v *)
Instance : Params (@mjoin) 3
:= {}.
(* stdpp/base.v *)
Class FMap (M : Type → Type)
:= fmap : ∀ {A B}, (A → B) → M A → M B.
(* stdpp/base.v *)
Instance : Params (@fmap) 4
:= {}.
(* stdpp/base.v *)
Class OMap (M : Type → Type)
:= omap: ∀ {A B}, (A → option B) → M A → M B.
(* stdpp/base.v *)
Instance : Params (@omap) 4
:= {}.
(* stdpp/base.v *)
Notation "m ≫= f"
:= (mbind f m) (at level 60, right associativity) : stdpp_scope.
(* stdpp/base.v *)
Notation "( m ≫=.)"
:= (λ f, mbind f m) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.≫= f )"
:= (mbind f) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(≫=)"
:= (λ m f, mbind f m) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "x ← y ; z"
:= (y ≫= (λ x : _, z))
  (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "' x ← y ; z"
:= (y ≫= (λ x : _, z))
  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "x ;; z"
:= (x ≫= λ _, z)
  (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.
(* stdpp/base.v *)
Notation "ps .*1"
:= (fmap (M:=list) fst ps)
  (at level 1, left associativity, format "ps .*1").
(* stdpp/base.v *)
Notation "ps .*2"
:= (fmap (M:=list) snd ps)
  (at level 1, left associativity, format "ps .*2").
(* stdpp/base.v *)
(* For any monad that has a builtin way to throw an exception/error *)
Class MThrow (E : Type) (M : Type → Type)
:= mthrow : ∀ {A}, E → M A.
(* stdpp/base.v *)
Instance : Params (@mthrow) 4
:= {}.
(* stdpp/base.v *)
(* We use unit as the error content for monads that can only report an error
    without any payload like an option *)
Notation MFail
:= (MThrow ()).
(* stdpp/base.v *)
Notation mfail
:= (mthrow ()).
(* stdpp/base.v *)
Definition guard_or {E} (e : E) `{MThrow E M, MRet M} P `{Decision P} : M P
:=
  match decide P with
  | left H => mret H
  | right _ => mthrow e
  end.
(* stdpp/base.v *)
Notation guard
:= (guard_or ()).
(* stdpp/base.v *)
(* In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K A M : Type)
:= lookup: K → M → option A.
(* stdpp/base.v *)
Instance : Params (@lookup) 5
:= {}.
(* stdpp/base.v *)
Notation "m !! i"
:= (lookup i m) (at level 20) : stdpp_scope.
(* stdpp/base.v *)
Notation "(!!)"
:= lookup (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( m !!.)"
:= (λ i, m !! i) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.!! i )"
:= (lookup i) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
(* The function [lookup_total] should be the total over-approximation
of the partial [lookup] function. *)
Class LookupTotal (K A M : Type)
:= lookup_total : K → M → A.
(* stdpp/base.v *)
Instance : Params (@lookup_total) 5
:= {}.
(* stdpp/base.v *)
Notation "m !!! i"
:= (lookup_total i m) (at level 20) : stdpp_scope.
(* stdpp/base.v *)
Notation "(!!!)"
:= lookup_total (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( m !!!.)"
:= (λ i, m !!! i) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.!!! i )"
:= (lookup_total i) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
(* The singleton map *)
Class SingletonM K A M
:= singletonM: K → A → M.
(* stdpp/base.v *)
Instance : Params (@singletonM) 5
:= {}.
(* stdpp/base.v *)
Notation "{[ k := a ]}"
:= (singletonM k a)
  (at level 0, format "{[ k := a ]}") : stdpp_scope.
(* stdpp/base.v *)
(* The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
Class Insert (K A M : Type)
:= insert: K → A → M → M.
(* stdpp/base.v *)
Instance : Params (@insert) 5
:= {}.
(* stdpp/base.v *)
Notation "<[ k := a ]>"
:= (insert k a)
  (at level 0, right associativity, format "<[ k := a ]>") : stdpp_scope.
(* stdpp/base.v *)
(* The "format" makes sure that linebreaks are placed after the separating semicolons [;] when printing. *)
Notation "{[ k1 := a1 ; k2 := a2 ]}"
:=
  (<[ k1 := a1 ]>{[ k2 := a2 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]>{[ k3 := a3 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]>{[ k4 := a4 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]>{[ k5 := a5 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]>{[ k6 := a6 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]>{[ k7 := a7 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]>{[ k8 := a8 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ; ']'  '/' '[' k8 := a8 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]>{[ k9 := a9 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ; ']'  '/' '[' k8 := a8 ; ']'  '/' '[' k9 := a9 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
    <[ k9 := a9 ]>{[ k10 := a10 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ; ']'  '/' '[' k8 := a8 ; ']'  '/' '[' k9 := a9 ; ']'  '/' '[' k10 := a10 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
    <[ k9 := a9 ]> $ <[ k10 := a10 ]>{[ k11 := a11 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ; ']'  '/' '[' k8 := a8 ; ']'  '/' '[' k9 := a9 ; ']'  '/' '[' k10 := a10 ; ']'  '/' '[' k11 := a11 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
    <[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]>{[ k12 := a12 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ; ']'  '/' '[' k8 := a8 ; ']'  '/' '[' k9 := a9 ; ']'  '/' '[' k10 := a10 ; ']'  '/' '[' k11 := a11 ; ']'  '/' '[' k12 := a12 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ; k13 := a13 ]}"
:=
  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
    <[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]> $ <[ k12 := a12 ]>{[ k13 := a13 ]})
  (at level 0, format
  "{[ '[hv' '[' k1 := a1 ; ']'  '/' '[' k2 := a2 ; ']'  '/' '[' k3 := a3 ; ']'  '/' '[' k4 := a4 ; ']'  '/' '[' k5 := a5 ; ']'  '/' '[' k6 := a6 ; ']'  '/' '[' k7 := a7 ; ']'  '/' '[' k8 := a8 ; ']'  '/' '[' k9 := a9 ; ']'  '/' '[' k10 := a10 ; ']'  '/' '[' k11 := a11 ; ']'  '/' '[' k12 := a12 ; ']'  '/' '[' k13 := a13 ']' ']' ]}") : stdpp_scope.
(* stdpp/base.v *)
(* The function delete [delete k m] should delete the value at key [k] in
[m]. If the key [k] is not a member of [m], the original map should be
returned. *)
Class Delete (K M : Type)
:= delete: K → M → M.
(* stdpp/base.v *)
Instance : Params (@delete) 4
:= {}.
(* stdpp/base.v *)
(* The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
Class Alter (K A M : Type)
:= alter: (A → A) → K → M → M.
(* stdpp/base.v *)
Instance : Params (@alter) 4
:= {}.
(* stdpp/base.v *)
(* The function [partial_alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k] or [None]
if [k] is not a member of [m]. The value at [k] should be deleted if [f]
yields [None]. *)
Class PartialAlter (K A M : Type)
:=
  partial_alter: (option A → option A) → K → M → M.
(* stdpp/base.v *)
Instance : Params (@partial_alter) 4
:= {}.
(* stdpp/base.v *)
(* The function [dom m] should yield the domain of [m]. That is a finite
set of type [D] that contains the keys that are a member of [m].
[D] is an output of the typeclass, i.e., there can be only one instance per map
type [M]. *)
Class Dom (M D : Type)
:= dom: M → D.
(* stdpp/base.v *)
Instance : Params (@dom) 3
:= {}.
(* stdpp/base.v *)
(* The function [merge f m1 m2] should merge the maps [m1] and [m2] by
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)]. *)
Class Merge (M : Type → Type)
:=
  merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
(* stdpp/base.v *)
Instance : Params (@merge) 4
:= {}.
(* stdpp/base.v *)
(* The function [union_with f m1 m2] is supposed to yield the union of [m1]
and [m2] using the function [f] to combine values of members that are in
both [m1] and [m2]. *)
Class UnionWith (A M : Type)
:=
  union_with: (A → A → option A) → M → M → M.
(* stdpp/base.v *)
Instance : Params (@union_with) 3
:= {}.
(* stdpp/base.v *)
(* Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type)
:=
  intersection_with: (A → A → option A) → M → M → M.
(* stdpp/base.v *)
Instance : Params (@intersection_with) 3
:= {}.
(* stdpp/base.v *)
Class DifferenceWith (A M : Type)
:=
  difference_with: (A → A → option A) → M → M → M.
(* stdpp/base.v *)
Instance : Params (@difference_with) 3
:= {}.
(* stdpp/base.v *)
Definition intersection_with_list `{IntersectionWith A M}
  (f : A → A → option A) : M → list M → M
:= fold_right (intersection_with f).
(* stdpp/base.v *)
(* SqSubsetEq registers the "canonical" partial order for a type, and is used
for the \sqsubseteq symbol. *)
Class SqSubsetEq A
:= sqsubseteq: relation A.
(* stdpp/base.v *)
Instance : Params (@sqsubseteq) 2
:= {}.
(* stdpp/base.v *)
Notation "(⊑)"
:= sqsubseteq (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ⊑.)"
:= (sqsubseteq x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊑ y )"
:= (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(⊑@{ A } )"
:= (@sqsubseteq A _) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
(* [sqsubseteq] does not take precedence over the stdlib's instances (like [eq],
[impl], [iff]) or std++'s [equiv].
We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200
:= {}.
(* stdpp/base.v *)
Class Meet A
:= meet: A → A → A.
(* stdpp/base.v *)
Instance : Params (@meet) 2
:= {}.
(* stdpp/base.v *)
Notation "(⊓)"
:= meet (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ⊓.)"
:= (meet x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊓ y )"
:= (λ x, meet x y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Class Join A
:= join: A → A → A.
(* stdpp/base.v *)
Instance : Params (@join) 2
:= {}.
(* stdpp/base.v *)
Notation "(⊔)"
:= join (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ⊔.)"
:= (join x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.⊔ y )"
:= (λ x, join x y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "⊤"
:= top (format "⊤") : stdpp_scope.
(* stdpp/base.v *)
Notation "⊥"
:= bottom (format "⊥") : stdpp_scope.
(* stdpp/base.v *)
(* The classes [SemiSet A C], [Set_ A C], and [TopSet A C] axiomatize sets of
type [C] with elements of type [A]. The first class, [SemiSet] does not include
intersection and difference. It is useful for the case of lists, where decidable
equality is needed to implement intersection and difference, but not union.

Note that we cannot use the name [Set] since that is a reserved keyword. Hence
we use [Set_]. *)
Class SemiSet A C `{ElemOf A C,
    Empty C, Singleton A C, Union C} : Prop
:= {
  not_elem_of_empty (x : A) : x ∉@{C} ∅; (* We prove
  [elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for
  rewriting. *)
  elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
  elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
}.
(* stdpp/base.v *)
Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
    Union C, Intersection C, Difference C} : Prop
:= {
  set_semi_set :: SemiSet A C;
  elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
  elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
}.
(* stdpp/base.v *)
Class TopSet A C `{ElemOf A C, Top C} : Prop
:= {
  elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
  in [sets.v], which is more convenient for rewriting. *)
}.
(* stdpp/base.v *)
(* We axiomative a finite set as a set whose elements can be
enumerated as a list. These elements, given by the [elements] function, may be
in any order and should not contain duplicates. *)
Class Elements A C
:= elements: C → list A.
(* stdpp/base.v *)
Instance : Params (@elements) 3
:= {}.
(* stdpp/base.v *)
(* We redefine the standard library's [In] and [NoDup] using type classes. *)
Inductive list_elem_of {A} : ElemOf A (list A)
:=
  | list_elem_of_here (x : A) l : x ∈ x :: l
  | list_elem_of_further (x y : A) l : x ∈ l → x ∈ y :: l.
(* stdpp/base.v *)
Lemma list_elem_of_In {A} (l : list A) x : x ∈ l ↔ In x l.
Proof.
  split.
  - induction 1; simpl; auto.
  - induction l; destruct 1; subst; constructor; auto.
Qed.
(* stdpp/base.v *)
Inductive NoDup {A} : list A → Prop
:=
  | NoDup_nil_2 : NoDup []
  | NoDup_cons_2 x l : x ∉ l → NoDup l → NoDup (x :: l).
(* stdpp/base.v *)
Lemma NoDup_ListNoDup {A} (l : list A) : NoDup l ↔ List.NoDup l.
Proof.
  split.
  - induction 1; constructor; rewrite <-?list_elem_of_In; auto.
  - induction 1; constructor; rewrite ?list_elem_of_In; auto.
Qed.
(* stdpp/base.v *)
(* Decidability of equality of the carrier set is admissible, but we add it
anyway so as to avoid cycles in type class search. *)
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
    Intersection C, Difference C, Elements A C, EqDecision A} : Prop
:= {
  fin_set_set :: Set_ A C;
  elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
  NoDup_elements (X : C) : NoDup (elements X)
}.
(* stdpp/base.v *)
Class Size C
:= size: C → nat.
(* stdpp/base.v *)
Instance : Params (@size) 2
:= {}.
(* stdpp/base.v *)
(* The class [MonadSet M] axiomatizes a type constructor [M] that can be
used to construct a set [M A] with elements of type [A]. The advantage
of this class, compared to [Set_], is that it also axiomatizes the
the monadic operations. The disadvantage is that not many inhabitants are
possible: we will only provide as inhabitants [propset] and [listset], which are
represented respectively using Boolean functions and lists with duplicates.

More interesting implementations typically need
decidable equality, or a total order on the elements, which do not fit
in a type constructor of type [Type → Type]. *)
Class MonadSet M `{∀ A, ElemOf A (M A),
    ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A),
    !MBind M, !MRet M, !FMap M, !MJoin M} : Prop
:= {
  monad_set_semi_set A :: SemiSet A (M A);
  elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
    x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
  elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y;
  elem_of_fmap {A B} (f : A → B) (X : M A) (x : B) :
    x ∈ f <$> X ↔ ∃ y, x = f y ∧ y ∈ X;
  elem_of_join {A} (X : M (M A)) (x : A) :
    x ∈ mjoin X ↔ ∃ Y : M A, x ∈ Y ∧ Y ∈ X
}.
(* stdpp/base.v *)
(* The [Infinite A] class axiomatizes types [A] with infinitely many elements.
It contains a function [fresh : list A → A] that, given a list [xs], gives an
element [fresh xs ∉ xs].

We do not directly make [fresh] a field of the [Infinite] class, but use a
separate operational type class [Fresh] for it. That way we can overload [fresh]
to pick fresh elements from other data structures like sets. See the file
[fin_sets], where we define [fresh : C → A] for any finite set implementation
[FinSet C A].

Note: we require [fresh] to respect permutations, which is needed to define the
aforementioned [fresh] function on finite sets that respect set equality.

Instead of instantiating [Infinite] directly, consider using [max_infinite] or
[inj_infinite] from the [infinite] module. *)
Class Fresh A C
:= fresh: C → A.
(* stdpp/base.v *)
Instance : Params (@fresh) 3
:= {}.
(* stdpp/base.v *)
Class Infinite A
:= {
  infinite_fresh :: Fresh A (list A);
  infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
  infinite_fresh_Permutation :: Proper (@Permutation A ==> (=)) fresh;
}.
(* stdpp/base.v *)
(* * Miscellaneous *)
Class Half A
:= half: A → A.
(* stdpp/base.v *)
Notation "½"
:= half (format "½") : stdpp_scope.
(* stdpp/base.v *)
Notation "½*"
:= (fmap (M:=list) half) : stdpp_scope.
(* stdpp/binders.v *)
Inductive binder
:= BAnon | BNamed :> string → binder.
(* stdpp/binders.v *)
Notation "<>"
:= BAnon : binder_scope.
(* stdpp/binders.v *)
(* [binder_list] matches [option_list]. *)
Definition binder_list (b : binder) : list string
:=
  match b with
  | BAnon => []
  | BNamed s => [s]
  end.
(* stdpp/binders.v *)
Instance binder_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
(* stdpp/binders.v *)
Instance binder_inhabited : Inhabited binder
:= populate BAnon.
(* stdpp/binders.v *)
Instance binder_countable : Countable binder.
Proof.
 refine (inj_countable'
   (λ b, match b with BAnon => None | BNamed s => Some s end)
   (λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
Qed.
(* stdpp/binders.v *)
(* The functions [cons_binder b ss] and [app_binder bs ss] are typically used
to collect the free variables of an expression. Here [ss] is the current list of
free variables, and [b], respectively [bs], are the binders that are being
added. *)
Definition cons_binder (b : binder) (ss : list string) : list string
:=
  match b with BAnon => ss | BNamed s => s :: ss end.
(* stdpp/binders.v *)
Fixpoint app_binder (bs : list binder) (ss : list string) : list string
:=
  match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
(* stdpp/binders.v *)
Instance set_unfold_cons_binder s b ss P :
  SetUnfoldElemOf s ss P → SetUnfoldElemOf s (b :b: ss) (BNamed s = b ∨ P).
Proof.
  constructor. rewrite <-(set_unfold (s ∈ ss) P).
  destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
Qed.
(* stdpp/binders.v *)
Instance set_unfold_app_binder s bs ss P Q :
  SetUnfoldElemOf (BNamed s) bs P → SetUnfoldElemOf s ss Q →
  SetUnfoldElemOf s (bs +b+ ss) (P ∨ Q).
Proof.
  intros HinP HinQ.
  constructor. rewrite <-(set_unfold (s ∈ ss) Q), <-(set_unfold (BNamed s ∈ bs) P).
  clear HinP HinQ.
  induction bs; set_solver.
Qed.
(* stdpp/binders.v *)
Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
Proof. induction ss1; by f_equal/=. Qed.
(* stdpp/binders.v *)
Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.
(* stdpp/binders.v *)
Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
(* stdpp/binders.v *)
Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
Proof.
  assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
  { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
  induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
    first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
Qed.
(* stdpp/binders.v *)
Definition binder_delete `{Delete string M} (b : binder) (m : M) : M
:=
  match b with BAnon => m | BNamed s => delete s m end.
(* stdpp/binders.v *)
Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M
:=
  match b with BAnon => m | BNamed s => <[s:=x]> m end.
(* stdpp/binders.v *)
Instance : Params (@binder_insert) 4
:= {}.
(* stdpp/binders.v *)
Instance binder_insert_proper `{Equiv A} b :
    Proper ((≡) ==> (≡) ==> (≡@{M A})) (binder_insert b).
Proof. destruct b; solve_proper. Qed.
(* stdpp/binders.v *)
Lemma binder_delete_empty {A} b : binder_delete b ∅ =@{M A} ∅.
Proof. destruct b; simpl; eauto using delete_empty. Qed.
(* stdpp/binders.v *)
Lemma lookup_binder_delete_None {A} (m : M A) b s :
    binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
(* stdpp/binders.v *)
Lemma binder_insert_fmap {A B} (f : A → B) (x : A) b (m : M A) :
    f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
(* stdpp/binders.v *)
Lemma binder_delete_insert {A} b s x (m : M A) :
    b ≠ BNamed s → binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.