seqset.v 1.07 KB
Newer Older
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.

Section SeqSet.

  (* Let T be any type with decidable equality. *)
  Context {T: eqType}.

  (* We define a set as a sequence that has no duplicates. *)
  Record set :=
  {
    _set_seq :> seq T ;
    _ : uniq _set_seq (* no duplicates *)
  }.

  (* Now we add the ssreflect boilerplate code. *)
  Canonical Structure setSubType := [subType for _set_seq].
  Definition set_eqMixin := [eqMixin of set by <:].
  Canonical Structure set_eqType := EqType set set_eqMixin.
  Canonical Structure mem_set_predType := mkPredType (fun (l : set) => mem_seq (_set_seq l)).
  Definition set_of of phant T := set.

End SeqSet.

Notation " {set R } " := (set_of (Phant R)).

Section Lemmas.

  Context {T: eqType}.
  Variable s: {set T}.

  Lemma set_uniq : uniq s.
  Proof.
    by destruct s.
  Qed.

End Lemmas.

Section LemmasFinType.
  
  Context {T: finType}.
  Variable s: {set T}.

  Lemma set_card : #|s| = size s.
  Proof.
    have UNIQ: uniq s by destruct s.
    by move: UNIQ => /card_uniqP ->.
  Qed.
  
End LemmasFinType.