enumeration.v

Require Import generic_quotient.

Module Type Enumeration_signature.
Parameter type : choiceType -> Type.
Section Operations.
Context {T : choiceType}.
 Parameter of_seq : seq T -> type T.
 Parameter seq : type T -> seq_eqclass T.
 Axiom eq : forall e1 e2, seq e1 =i seq e2 -> e1 = e2.
 Axiom mem : forall s, seq (of_seq s) =i s.
 Axiom uniq : forall e, uniq (seq e).
End Operations.
End Enumeration_signature.

Module Enumeration : Enumeration_signature.
Section OverType.
Context {T : choiceType}.

Lemma enum_relP : @equiv_class_of (seq T) (relpre undup perm_eq).
Proof. by split=> [x|x y|x y z] //=; [apply: perm_sym | apply: perm_trans]. Qed.
Definition enum_rel := EquivRelPack enum_relP.

Definition type := {eq_quot enum_rel}%qT.
Implicit Types (e : type) (s : seq T).
Definition of_seq s : type := (\pi s)%qT.
Local Coercion seq e : seq_eqclass T := undup (repr e).

Lemma uniq e : uniq e. Proof. exact: undup_uniq. Qed.

Lemma mem s : of_seq s =i s.
Proof.
move=> x; rewrite -[RHS]mem_undup.
by apply/perm_mem/(@eqmodP _ enum_rel); rewrite reprK.
Qed.

Lemma eq e1 e2 : e1 =i e2 -> e1 = e2.
Proof.
move/perm_undup; rewrite !undup_id ?undup_uniq // => eq_e12.
by rewrite -[e1]reprK -[e2]reprK; apply/eqquotP.
Qed.

End OverType.
End Enumeration.

Coercion Enumeration.seq : Enumeration.type >-> seq_eqclass.
Lemma Enumeration_seqK T : cancel (@Enumeration.seq T) Enumeration.of_seq.
Proof. by move=> e; apply/Enumeration.eq/Enumeration.mem. Qed.