Commit fe9771cc authored by Robbert Krebbers's avatar Robbert Krebbers

Decider for empty listsets.

parent 52a3dc34
...@@ -24,6 +24,16 @@ Proof. ...@@ -24,6 +24,16 @@ Proof.
* by apply elem_of_list_singleton. * by apply elem_of_list_singleton.
* intros [?] [?]. apply elem_of_app. * intros [?] [?]. apply elem_of_app.
Qed. Qed.
Lemma listset_empty_alt X : X listset_car X = [].
Proof.
destruct X as [l]; split; [|by intros; simplify_equality'].
intros [Hl _]; destruct l as [|x l]; [done|]. feed inversion (Hl x); left.
Qed.
Global Instance listset_empty_dec (X : listset A) : Decision (X ).
Proof.
refine (cast_if (decide (listset_car X = [])));
abstract (by rewrite listset_empty_alt).
Defined.
Context `{ x y : A, Decision (x = y)}. Context `{ x y : A, Decision (x = y)}.
......
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