Library FinSet.Lib.ListSet

Using DProp to implement the decidable set-equality of lists. This is certainly not the most minimal implementation, as most of it could be lifted from Coq's standard library. But it is very self-contained, and was rather fun to write.

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import FinSet.Lib.DProp.

Inductive member predicate

The point of this predicate is to avoid using full-blown equality to define members. Indeed, the indices are patterns, which can be handled by well-crafted return predicates of pattern matching.

Inductive Mem {A:Type} : list A → Type :=
| head : ∀ x {l}, Mem (x ::l)
| tail : ∀ {x l}, Mem l → Mem (x ::l)
.

Definition no_mem_empty A : ∀ B, @Mem A [] → B :=
  fun B c ⇒ match c with end.

Ltac use_no_mem_empty :=
  lazymatch goal with
  | h:@Mem _ [] |- _ ⇒ eapply no_mem_empty; exact h
  end.

Hint Extern 1 ⇒ use_no_mem_empty.

Fixpoint of_mem {A} {l:list A} (m:Mem l) : A :=
  match m with
  | head x ⇒ x
  | tail m´ ⇒ of_mem m´
  end
.

The members of a list are thoses x such that In x l. It will give the appropriate glue when we use membership predicates and equality to specify operations.

Lemma in_is_mem A (l:list A) (x:A) : In x l ↔ ∃ m:Mem l , x =of_mem m.

Decidable quantifiers on lists members

Program Fixpoint exists_dec {A:Type} (P:A →DProp) (l:list A) : {∃ x:Mem l , P (of_mem x)} + {∀ x:Mem l, DNot (P (of_mem x))} :=
  match l return _ with
  | [] ⇒ right _
  | a::q ⇒ dec_lift (Sumbool.sumbool_or _ _ _ _ (P a) (exists_dec P q))
  end
.

Program Definition dexists {A:Type} (P:A →DProp) (l:list A) : DProp := {|
  dec := exists_dec P l
|}.

Definition dforall {A:Type} (P:A →DProp) (l:list A) : DProp :=
  DNot (dexists (fun x⇒ DNot (P x)) l)
.

Set-like decidable relations on lists

Decidable membership predicate

Definition mem_list {A:Type} (E:A →A →DProp) (x:A) :=
  dexists (E x).

Remark no_mem_list_empty A E x : ∀ B, @mem_list A E x [] → B.

Ltac use_no_mem_list_empty :=
  lazymatch goal with
  | h:Holds (@mem_list _ _ _ []) |- _ ⇒ eapply no_mem_list_empty; exact h
  end.

Hint Extern 1 ⇒ use_no_mem_list_empty.

Lemma mem_list_right {A:Type} (E:A →A →DProp) (x y:A) (l:list A) :
  mem_list E x l → mem_list E x (y ::l).

Lemma mem_list_left {A:Type} (E:A →A →DProp) (x y:A) (l:list A) :
  E x y → mem_list E x (y ::l).

Corollary mem_list_cons {A:Type} (E:A →A →DProp) (x y:A) (l:list A) :
  eq_dprop (mem_list E x (y ::l)) (E x y || mem_list E x l).

Lemma mem_list_app {A:Type} (E:A →A →DProp) (x:A) (l₁ l₂:list A) :
  eq_dprop (mem_list E x (l₁ ++l₂)) (mem_list E x l₁ || mem_list E x l₂).

Program Fixpoint mem_of_mem_list {A:Type} (E:A →A →DProp) (l:list A) (x:A) : mem_list E x l → Mem l :=
  match l return mem_list E x l → Mem l with
  | [] ⇒ fun h ⇒ _
  | a::q ⇒ fun h ⇒ if dec (E x a) then head a
                     else tail (mem_of_mem_list E q x _)
  end
.

Lemma mem_of_mem_list_spec A (E:A →A →DProp) (l:list A) (x:A) (h:mem_list E x l) : E x (of_mem (mem_of_mem_list E l x h)).

Inclusion and equivalence

Definition included_list {A:Type} (E:A →A →DProp) (l₁ l₂:list A) : DProp :=
  dforall (fun x ⇒ mem_list E x l₂) l₁.

Instance included_list_preorder A (E:A →A →DProp) :
     PreOrder E → PreOrder (included_list E).

Corollary mem_included_list A (E:A →A →DProp) (_:Transitive E) : ∀ x l₁ l₂,
   included_list E l₁ l₂ → Basics.impl (mem_list E x l₁) (mem_list E x l₂).

Definition eq_set_list {A:Type} (E:A →A →DProp) (l₁ l₂:list A) : DProp :=
  included_list E l₁ l₂ && included_list E l₂ l₁.

Instance equivalence_preorder A (R:A →A →Prop) (_:Equivalence R) : PreOrder R.

Instance eq_set_list_eq A (E:A →A →DProp) :
     Equivalence E → Equivalence (eq_set_list E).

Corollary mem_eq_set_list A (E:A →A →DProp) (_:Transitive E): ∀ l₁ l₂ x,
  eq_set_list E l₁ l₂ → (mem_list E x l₁ ↔ mem_list E x l₂ ).

Instance mem_eq_set_list_proper A (E:A →A →DProp) (_:Transitive E) :
  Proper (eq ==> eq_set_list E ==> eq_dprop) (mem_list E).

List without duplicates

Fixpoint nodup {A} (R:A →A →DProp) (l:list A) : DProp :=
  match l with
  | [] ⇒ DTrue
  | a::l ⇒ nodup R l && DNot (mem_list R a l)
  end
.

Fixpoint deduplicate {A} (R:A →A →DProp) (l:list A) : list A :=
  match l with
  | [] ⇒ []
  | a::l ⇒
    let dl :=
      List.filter
        (fun x ⇒ if dec (DNot (R a x)) then true else false)
        (deduplicate R l)
    in
    a::dl
  end
.

Lemma filter_sub A R l (p:A →bool) :
  ∀ x, mem_list R x (filter p l) → mem_list R x l.

Lemma filter_nodup A R (l:list A) : ∀ p:A →bool,
  nodup R l → nodup R (filter p l).

Lemma deduplicate_nodup A R (l:list A) : nodup R (deduplicate R l).

Lemma deduplicate_eq_set_list A (R:A →A →DProp) (l:list A) :
  Equivalence R → eq_set_list R l (deduplicate R l).