From HB Require Import structures.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

(** In this section, we define a notion of a set (based on a sequence
    without duplicates). *)
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 to support [_ == _]
      and [_ ∈ _] operations. *)
  Set Warnings "-redundant-canonical-projection".
  HB.instance Definition _  setSubType := [isSub for _set_seq].
Projection value has no head constant:
fun (K : set -> Type)
  (K_S : forall (x : seq T) (Px : uniq x),
         K (Build_set x Px)) (u : set) =>
match u as xxx return (K xxx) with
| Build_set x Px => K_S x Px
end in canonical instance
HB_unnamed_factory_2 of isSub.Sub_rect, ignoring it.
[projection-no-head-constant,records,default]
Projection value has no head constant:
fun (K : set -> Type)
  (K_S : forall (x : seq T) (Px : uniq x),
         K (Build_set x Px)) (u : set) =>
match u as xxx return (K xxx) with
| Build_set x Px => K_S x Px
end in canonical instance
HB_unnamed_factory_2 of isSub.Sub_rect, ignoring it.
[projection-no-head-constant,records,default]
  HB.instance Definition _ := [Equality of set by <:].
  Canonical Structure mem_set_predType := PredType (fun (l : set) => mem_seq (_set_seq l)).
  Set Warnings "redundant-canonical-projection".
  Definition set_of of phant T := set.

End SeqSet.
Projection value has no head constant:
fun (K : set -> Type)
  (K_S : forall (x : seq T) (Px : uniq x),
         K (Build_set x Px)) (u : set) =>
match u as xxx return (K xxx) with
| Build_set x Px => K_S x Px
end in canonical instance
HB_unnamed_factory_2 of isSub.Sub_rect, ignoring it.
[projection-no-head-constant,records,default]

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

(** Next we prove a basic lemma about sets. *)
Section Lemmas.

  (** Consider a set [s]. *)
  Context {T : eqType}.
  Variable s : {set T}.

  (** Then we show that element of [s] are unique. *)
  Lemma set_uniq : uniq s.
T: eqType
s: {setT}
uniq s
  Proof.
T: eqType
s: {setT}
uniq s by destruct s. Qed.

End Lemmas.