Library FinSet.Quotients.UList
This file defines a high level interface for lists with no
duplicates of types with decidable equality. They form a retract
of lists.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import FinSet.Lib.DProp.
Require Import FinSet.Lib.ListSet.
Require Import FinSet.Quotients.Retract.
Require Import FinSet.Quotients.Countable.
Definition UList (A:Type) (R:A→A→DProp) : Type :=
{ l:list A | Canonize (nodup R l) }.
Program Definition ulist {A} {R:A→A→DProp} :
Retract (list A) (UList A R) := {|
inj l := l;
proj l := deduplicate R l
|}.
Lemma ulist_ext A R :
∀ l₁ l₂:UList A R, ulist.(inj) l₁ = ulist.(inj) l₂ → l₁ = l₂.
Lemma ulist_nodup A R : ∀ l:UList A R, nodup R (ulist.(inj) l).
Lemma ulist_eq_set A (R:A→A→DProp) (e:Equivalence R) :
∀ l:list A, eq_set_list R ((ulist (R:=R)).(inj) (ulist.(proj) l)) l.
Definition eq_set_ulist {A} R (l₁ l₂:UList A R) : DProp :=
eq_set_list R (ulist.(inj) l₁) (ulist.(inj) l₂).
Instance eq_set_eq A (R:A→A→DProp) :
Equivalence R → Equivalence (eq_set_ulist R).
Instance ulist_proper A (R:A→A→DProp) (e:Equivalence R) :
Proper (eq_set_ulist R ==> eq_set_list R) ulist.(inj).