sets.v 2.29 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
4
From stdpp Require Export collections.
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6

Record set (A : Type) : Type := mkSet { set_car : A  Prop }.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Add Printing Constructor set.
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
Arguments mkSet {_} _.
Arguments set_car {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12
Notation "{[ x | P ]}" := (mkSet (λ x, P))
  (at level 1, format "{[  x  |  P  ]}") : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
13
Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
Robbert Krebbers's avatar
Robbert Krebbers committed
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15
Instance set_top {A} : Top (set A) := {[ _ | True ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18
Instance set_empty {A} : Empty (set A) := {[ _ | False ]}.
Instance set_singleton {A} : Singleton A (set A) := λ y, {[ x | y = x ]}.
Instance set_union {A} : Union (set A) := λ X1 X2, {[ x | x  X1  x  X2 ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
Instance set_intersection {A} : Intersection (set A) := λ X1 X2,
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  {[ x | x  X1  x  X2 ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Instance set_difference {A} : Difference (set A) := λ X1 X2,
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  {[ x | x  X1  x  X2 ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Instance set_collection : Collection A (set A).
Robbert Krebbers's avatar
Robbert Krebbers committed
24
Proof. split; [split | |]; by repeat intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
25

Robbert Krebbers's avatar
Robbert Krebbers committed
26
Lemma elem_of_top {A} (x : A) : x    True.
Ralf Jung's avatar
Ralf Jung committed
27
Proof. done. Qed.
28 29 30
Lemma elem_of_mkSet {A} (P : A  Prop) x : x  {[ x | P x ]}  P x.
Proof. done. Qed.
Lemma not_elem_of_mkSet {A} (P : A  Prop) x : x  {[ x | P x ]}  ¬P x.
31
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32 33 34
Lemma top_subseteq {A} (X : set A) : X  .
Proof. done. Qed.
Hint Resolve top_subseteq.
Ralf Jung's avatar
Ralf Jung committed
35

Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39
Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
Instance set_bind : MBind set := λ A B (f : A  set B) (X : set A),
  mkSet (λ b,  a, b  f a  a  X).
Instance set_fmap : FMap set := λ A B (f : A  B) (X : set A),
Robbert Krebbers's avatar
Robbert Krebbers committed
40
  {[ b |  a, b = f a  a  X ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Instance set_join : MJoin set := λ A (XX : set (set A)),
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  {[ a |  X, a  X  X  XX ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45
Instance set_collection_monad : CollectionMonad set.
Proof. by split; try apply _. Qed.

46 47 48 49 50 51
Instance set_unfold_set_all {A} (x : A) : SetUnfold (x  ( : set A)) True.
Proof. by constructor. Qed.
Instance set_unfold_mkSet {A} (P : A  Prop) x Q :
  SetUnfoldSimpl (P x) Q  SetUnfold (x  mkSet P) Q.
Proof. intros HPQ. constructor. apply HPQ. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
52
Global Opaque set_elem_of set_top set_empty set_singleton.
53 54
Global Opaque set_union set_intersection set_difference.
Global Opaque set_ret set_bind set_fmap set_join.