bset.v 1.65 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2 3
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
4
From stdpp Require Export prelude.
5
Set Default Proof Using "Type".
6 7

Record bset (A : Type) : Type := mkBSet { bset_car : A  bool }.
8 9 10
Arguments mkBSet {_} _ : assert.
Arguments bset_car {_} _ _ : assert.

11
Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
12
Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
13 14
Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
  mkBSet (λ y, bool_decide (y = x)).
15 16 17 18 19 20 21
Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x.
Instance bset_union {A} : Union (bset A) := λ X1 X2,
  mkBSet (λ x, bset_car X1 x || bset_car X2 x).
Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
  mkBSet (λ x, bset_car X1 x && bset_car X2 x).
Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
  mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
22
Instance bset_collection `{EqDecision A} : Collection A (bset A).
23 24
Proof.
  split; [split| |].
25 26 27 28 29
  - by intros x ?.
  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
  - split. apply orb_prop_elim. apply orb_prop_intro.
  - split. apply andb_prop_elim. apply andb_prop_intro.
  - intros X Y x; unfold elem_of, bset_elem_of; simpl. 
30 31
    destruct (bset_car X x), (bset_car Y x); simpl; tauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Instance bset_elem_of_dec {A} : RelDecision (@{bset A}).
33
Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
34 35 36 37

Typeclasses Opaque bset_elem_of.
Global Opaque bset_empty bset_singleton bset_union
  bset_intersection bset_difference.