listset_nodup.v 2.52 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
6
From stdpp Require Export collections list.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8

Record listset_nodup A := ListsetNoDup {
9
  listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12 13 14 15 16 17 18
}.
Arguments ListsetNoDup {_} _ _.
Arguments listset_nodup_car {_} _.
Arguments listset_nodup_prf {_} _.

Section list_collection.
Context {A : Type} `{ x y : A, Decision (x = y)}.
Notation C := (listset_nodup A).

19
Instance listset_nodup_elem_of: ElemOf A C := λ x l, x  listset_nodup_car l.
20
Instance listset_nodup_empty: Empty C := ListsetNoDup [] (@NoDup_nil_2 _).
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Instance listset_nodup_singleton: Singleton A C := λ x,
22
  ListsetNoDup [x] (NoDup_singleton x).
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Instance listset_nodup_union: Union C := λ l k,
24
  let (l',Hl) := l in let (k',Hk) := k
25
  in ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Instance listset_nodup_intersection: Intersection C := λ l k,
27
  let (l',Hl) := l in let (k',Hk) := k
28 29 30 31
  in ListsetNoDup _ (NoDup_list_intersection _ k' Hl).
Instance listset_nodup_difference: Difference C := λ l k,
  let (l',Hl) := l in let (k',Hk) := k
  in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
Robbert Krebbers's avatar
Robbert Krebbers committed
32

33
Instance: Collection A C.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Proof.
35
  split; [split | | ].
36 37 38 39 40
  - by apply not_elem_of_nil.
  - by apply elem_of_list_singleton.
  - intros [??] [??] ?. apply elem_of_list_union.
  - intros [??] [??] ?. apply elem_of_list_intersection.
  - intros [??] [??] ?. apply elem_of_list_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43 44
Qed.

Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
Global Instance: FinCollection A C.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Proof. split. apply _. done. by intros [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
End list_collection.

Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
  eapply @listset_nodup_elem_of : typeclass_instances.
Hint Extern 1 (Empty (listset_nodup _)) =>
  eapply @listset_nodup_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (listset_nodup _)) =>
  eapply @listset_nodup_singleton : typeclass_instances.
Hint Extern 1 (Union (listset_nodup _)) =>
  eapply @listset_nodup_union : typeclass_instances.
Hint Extern 1 (Intersection (listset_nodup _)) =>
  eapply @listset_nodup_intersection : typeclass_instances.
Hint Extern 1 (Difference (listset_nodup _)) =>
  eapply @listset_nodup_difference : typeclass_instances.
Hint Extern 1 (Elements _ (listset_nodup _)) =>
  eapply @listset_nodup_elems : typeclass_instances.