Commit 2ad56b99 authored by Robbert Krebbers's avatar Robbert Krebbers

`TopSet` instance for `boolset`.

parent e09f7ce3
......@@ -19,15 +19,16 @@ Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
Instance boolset_set `{EqDecision A} : Set_ A (boolset A).
Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
Proof.
split; [split| |].
split; [split; [split| |]|].
- 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, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done.
Qed.
Instance boolset_elem_of_dec {A} : RelDecision (@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment