base.v

Instance: Params (@mjoin) 3 := {}.
Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
Arguments fmap {_ _ _ _} _ !_ / : assert.
Instance: Params (@fmap) 4 := {}.
Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4 := {}.

Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
Notation "(.≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.

Notation "x ← y ; z" := (y ≫= (λ x : _, z))
  (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.

Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. ))
  (at level 20, x1 binder, xn binder, y at level 100, z at level 200,
   only parsing, right associativity) : stdpp_scope.

Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.

Notation "x ;; z" := (x ≫= λ _, z)
  (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.

Notation "ps .*1" := (fmap (M:=list) fst ps)
  (at level 2, left associativity, format "ps .*1").
Notation "ps .*2" := (fmap (M:=list) snd ps)
  (at level 2, left associativity, format "ps .*2").

Class MGuard (M : Type → Type) :=
  mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
Arguments mguard _ _ _ !_ _ _ / : assert.
Notation "'guard' P ; z" := (mguard P (λ _, z))
  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.

(** * Operations on maps *)
(** 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.
Hint Mode Lookup - - ! : typeclass_instances.
Instance: Params (@lookup) 4 := {}.
Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
Notation "(!!)" := lookup (only parsing) : stdpp_scope.
Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.

(** 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.
Hint Mode LookupTotal - - ! : typeclass_instances.
Instance: Params (@lookup_total) 4 := {}.
Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
Notation "(.!!! i )" := (lookup_total i) (only parsing) : stdpp_scope.
Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.

(** The singleton map *)
Class SingletonM K A M := singletonM: K → A → M.
Hint Mode SingletonM - - ! : typeclass_instances.
Instance: Params (@singletonM) 5 := {}.
Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.

(** 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.
Hint Mode Insert - - ! : typeclass_instances.
Instance: Params (@insert) 5 := {}.
Notation "<[ k := a ]>" := (insert k a)
  (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.

(** 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.
Hint Mode Delete - ! : typeclass_instances.
Instance: Params (@delete) 4 := {}.
Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.

(** 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.
Hint Mode Alter - - ! : typeclass_instances.
Instance: Params (@alter) 5 := {}.
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.

(** 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.
Hint Mode PartialAlter - - ! : typeclass_instances.
Instance: Params (@partial_alter) 4 := {}.
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.

(** The function [dom C m] should yield the domain of [m]. That is a finite
set of type [C] that contains the keys that are a member of [m]. *)
Class Dom (M C : Type) := dom: M → C.
Hint Mode Dom ! ! : typeclass_instances.
Instance: Params (@dom) 3 := {}.
Arguments dom : clear implicits.
Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.

(** 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.
Hint Mode Merge ! : typeclass_instances.
Instance: Params (@merge) 4 := {}.
Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.

(** 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.
Hint Mode UnionWith - ! : typeclass_instances.
Instance: Params (@union_with) 3 := {}.
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.

(** Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type) :=
  intersection_with: (A → A → option A) → M → M → M.
Hint Mode IntersectionWith - ! : typeclass_instances.
Instance: Params (@intersection_with) 3 := {}.
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.

Class DifferenceWith (A M : Type) :=
  difference_with: (A → A → option A) → M → M → M.
Hint Mode DifferenceWith - ! : typeclass_instances.
Instance: Params (@difference_with) 3 := {}.
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.

Definition intersection_with_list `{IntersectionWith A M}
  (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
Arguments intersection_with_list _ _ _ _ _ !_ / : assert.

Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
Hint Mode LookupE - - - ! : typeclass_instances.
Instance: Params (@lookupE) 6 := {}.
Notation "m !!{ Γ } i" := (lookupE Γ i m)
  (at level 20, format "m  !!{ Γ }  i") : stdpp_scope.
Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : stdpp_scope.
Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.

Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
Hint Mode InsertE - - - ! : typeclass_instances.
Instance: Params (@insertE) 6 := {}.
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : stdpp_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.


(** * Notations for lattices. *)
(** SqSubsetEq registers the "canonical" partial order for a type, and is used
for the \sqsubseteq symbol. *)
Class SqSubsetEq A := sqsubseteq: relation A.
Hint Mode SqSubsetEq ! : typeclass_instances.
Instance: Params (@sqsubseteq) 2 := {}.
Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.

Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.

Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.

Hint Extern 0 (_ ⊑ _) => reflexivity : core.

Class Meet A := meet: A → A → A.
Hint Mode Meet ! : typeclass_instances.
Instance: Params (@meet) 2 := {}.
Infix "⊓" := meet (at level 40) : stdpp_scope.
Notation "(⊓)" := meet (only parsing) : stdpp_scope.
Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.

Class Join A := join: A → A → A.
Hint Mode Join ! : typeclass_instances.
Instance: Params (@join) 2 := {}.
Infix "⊔" := join (at level 50) : stdpp_scope.
Notation "(⊔)" := join (only parsing) : stdpp_scope.
Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.

Class Top A := top : A.
Hint Mode Top ! : typeclass_instances.
Notation "⊤" := top (format "⊤") : stdpp_scope.

Class Bottom A := bottom : A.
Hint Mode Bottom ! : typeclass_instances.
Notation "⊥" := bottom (format "⊥") : stdpp_scope.


(** * Axiomatization of sets *)
(** 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
}.
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
}.
Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
    Union C, Intersection C, Difference C} : Prop := {
  top_set_set :> Set_ A C;
  elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
  in [sets.v], which is more convenient for rewriting. *)
}.

(** 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.
Hint Mode Elements - ! : typeclass_instances.
Instance: Params (@elements) 3 := {}.

(** We redefine the standard library's [In] and [NoDup] using type classes. *)
Inductive elem_of_list {A} : ElemOf A (list A) :=
  | elem_of_list_here (x : A) l : x ∈ x :: l
  | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
Existing Instance elem_of_list.

Lemma elem_of_list_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.

Inductive NoDup {A} : list A → Prop :=
  | NoDup_nil_2 : NoDup []
  | NoDup_cons_2 x l : x ∉ l → NoDup l → NoDup (x :: l).

Lemma NoDup_ListNoDup {A} (l : list A) : NoDup l ↔ List.NoDup l.
Proof.
  split.
  - induction 1; constructor; rewrite <-?elem_of_list_In; auto.
  - induction 1; constructor; rewrite ?elem_of_list_In; auto.
Qed.

(** 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)
}.
Class Size C := size: C → nat.
Hint Mode Size ! : typeclass_instances.
Arguments size {_ _} !_ / : simpl nomatch, assert.
Instance: Params (@size) 2 := {}.

(** 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 inhabits are
possible (we will only provide an inhabitant using unordered lists without
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
}.

(** 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 structure 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 respects 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.
Hint Mode Fresh - ! : typeclass_instances.
Instance: Params (@fresh) 3 := {}.
Arguments fresh : simpl never.

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;
}.
Arguments infinite_fresh : simpl never.

(** * Miscellaneous *)
Class Half A := half: A → A.
Hint Mode Half ! : typeclass_instances.
Notation "½" := half (format "½") : stdpp_scope.
Notation "½*" := (fmap (M:=list) half) : stdpp_scope.