Library Obs.list_dec

Set Implicit Arguments.

Require Import notations decidable_prop Psatz.
Require Export list_tools.

Lists over a decidable set

Section dec_list.
Context { A : Set } { dec_A : decidable_set A }.

Boolean equality for lists

  Fixpoint equal_list l m :=
    match (l ,m ) with
    | ([],[]) ⇒ true
    | (a::l,b::m) ⇒ eqX a b && equal_list l m
    | _ ⇒ false
    end.

  Lemma equal_list_spec l m : reflect (l = m) (equal_list l m).

The set of lists of As is decidable.

Global Instance dec_list : decidable_set (list A).

Boolean predicate testing whether an element belongs to a list.

  Definition inb (n : A) l := existsb (eqX n) l.

  Lemma inb_spec n l : inb n l = true ↔ n ∈ l.

  Lemma inb_false n l : inb n l = false ↔ ¬ n ∈ l.

This boolean predicate allows us to use the excluded middle with the predicate In.

Lemma inb_dec n l : { inb n l = true ∧ n ∈ l } + { inb n l = false ∧ ¬ n ∈ l }.

Lemma In_dec (n : A) l : { n ∈ l } + { ¬ n ∈ l }.

Boolean function implementing containment test.

  Definition inclb (a b : list A) :=
    forallb (fun x ⇒ inb x b) a.

  Lemma inclb_correct a b : inclb a b = true ↔ a ⊆ b.

Boolean function testing for equivalence of lists.

Definition equivalentb l1 l2 := inclb l1 l2 && inclb l2 l1.

Lemma equivalentb_spec l1 l2 : equivalentb l1 l2 = true ↔ l1 ≈ l2.

If u=u1++a::u2, we call the triple (u1,u2) an a-decomposition of u if a does not appear in u1.

If a is in l, then there exists an a-decomposition of l.

Lemma decomposition (a : A) l :
a ∈ l ↔ ∃ l1 l2 , l = l1 ++ a :: l2 ∧ ¬ a ∈ l1.

Decompositions are unique.

  Lemma decomp_unique (a:A) u1 u2 v1 v2 :
    u1 ++(a ::u2 ) = v1 ++a ::v2 → ¬ In a v1 → ¬ In a u1 → u1 = v1 ∧ u2 = v2.

  Lemma decomp_unambiguous (u1 u2 v1 v2 : list A) a b :
    u1 ++a ::u2 = v1 ++b ::v2 → ¬ In a v1 → ¬ In b u1 → u1 = v1 ∧ a =b ∧ u2 = v2.

{{l}} is a list containing the same elements as l, but without duplication.

  Definition undup l :=
    fold_right (fun a acc ⇒
                  if inb a acc
                  then acc
                  else a ::acc)
               nil
               l.

  Notation " {{ l }} " := (undup l) (at level 0).

{{l}} is shorter than l.

Lemma undup_length l : ⎢{{l }}⎥ ≤ ⎢l ⎥ .

{{l}} contains the same elements as l.

Lemma In_undup a l: a ∈ {{l }} ↔ a ∈ l.

Put differently, {{l}} is equivalent to l.

Lemma undup_equivalent l : {{l }} ≈ l.

The {{}} operator always produces a duplication free list.

Lemma NoDup_undup l : NoDup {{l }}.

The {{}} operator doesn't change duplication free lists.

Lemma NoDup_undup_eq l : NoDup l → l = {{l }}.

A list is without duplication if and only if its mirror is duplication free.

Lemma NoDup_rev {X:Set} (l : list X) : NoDup l ↔ NoDup (rev l).

{{}} preserves both ⊆ and ≈.

Global Instance undup_incl_Proper : Proper (@incl A ==> @incl A) undup.
Global Instance undup_equivalent_Proper : Proper (@equivalent A ==> @equivalent A) undup.

If l is contained in m and doesn't contain duplicates, then it must be shorter than m.

Lemma NoDup_length (l m : list A) :
l ⊆ m → NoDup l → ⎢l ⎥ ≤ ⎢m ⎥ .

l is a fixpoint of map f if and only if {{l}} is a fixpoint of the same list homomorphism map f.

Lemma map_undup_id (l : list A) (f : A → A) :
map f l = l ↔ map f {{l }} = {{l }}.

If f is injective, map f and {{}} commute.

Lemma map_undup_inj (l : list A) (f : A → A) :
(∀ x y, f x = f y → x = y ) → map f {{l }} = {{map f l }}.

NoDup is a decidable property.

Definition NoDupb l := l =?= {{l }}.

Lemma NoDupb_NoDup l : NoDupb l = true ↔ NoDup l.

Remove an element from a list.

  Definition rm (a : A) l := (fun x ⇒ negb (a =?=x)) :> l.
  Notation " l ∖ a " := (rm a l) (at level 50).

  Lemma rm_In b a l : b ∈ l ∖ a ↔ b ∈ l ∧ a ≠b.

  Lemma rm_equiv a l : a ∈ l → l ≈ a ::(l ∖ a ).

  Global Instance rm_equivalent_Proper a : Proper ((@equivalent A )==> (@equivalent A )) (rm a).

  Global Instance rm_incl_Proper a : Proper ((@incl A )==> (@incl A )) (rm a).

  Lemma rm_notin a l : ¬ a ∈ l → l ∖ a = l.

Remove the first occurrence of an element from a list.

  Fixpoint rmfst (a : A) l :=
  match l with
  | [] ⇒ []
  | b::l ⇒ if a =?=b then l else b::(rmfst a l )
  end.
  Notation " l ⊖ a " := (rmfst a l) (at level 50).

  Lemma rmfst_notin a l : ¬ a ∈ l → l ⊖ a = l.

  Lemma rmfst_in a l1 l2 : ¬ a ∈ l1 → (l1 ++ a :: l2 ) ⊖ a = l1 ++l2.

l ⊖ a is contained in the list l.

Lemma rmfst_decr a l : l ⊖ a ⊆ l.

The operation rmfst commutes with itself.

Lemma rmfst_comm (l : list A) a b : (l ⊖ a ) ⊖ b = (l ⊖ b ) ⊖ a.

If we try to remove a from l++m, one of three things may happen:

a appears in l, so we obtain (l⊖ a)++m;
a appears in m but not in l, so we obtain l++(m⊖ a);
a does not appear in l or m, so we obtain l++m.

  Lemma rmfst_app_dec (l m:list A) a :
    (∃ l1 l2 , l = l1 ++a ::l2 ∧ ¬ a ∈ l1 ∧ (l ++m ) ⊖ a = l1 ++l2 ++m )
    ∨ (∃ m1 m2 , m = m1 ++a ::m2 ∧ ¬ a ∈ (l ++m1 ) ∧ (l ++m ) ⊖ a = l ++m1 ++m2 )
    ∨ (¬ a ∈ (l ++m ) ∧ (l ++m ) ⊖ a = l ++m ).

This lemma highlights the existence of a list l1-l2: the list m shown to exist here is such that it contains no elements from l1, but concatenating l1 and m yields a list equivalent to l1++l2. Furthermore, we produce m without inserting any duplicates.

Lemma split_app_unambiguous (l1 l2 : list A) :
∃ m , l1 ++l2 ≈ l1 ++m ∧ NoDup m ∧ (∀ a, a ∈ m → ¬ a ∈ l1 ).

Sometimes we will need to count the number of occurrences of a particular element in a given list.

Notation nb a l := ⎢eqX a :> l⎥.

An equivalent (but slightly less convenient) function was defined in the standard library.

Lemma nb_count_occ (a : A) l : nb a l = count_occ X_dec l a.

For convenience, we translate all the lemmas regarding count_occ in terms of nb.

  Lemma nb_nil (x : A) : nb x [] = 0.

  Lemma nb_In l (x : A) : x ∈ l ↔ nb x l > 0.

  Lemma nb_not_In (l : list A) (x : A): ¬ x ∈ l ↔ nb x l = 0.

  Lemma NoDup_nb (l : list A) : NoDup l ↔ (∀ x : A, nb x l ≤ 1).

  Lemma nb_inv_nil (l : list A) : (∀ x : A, nb x l = 0) ↔ l = [].

  Lemma nb_cons_neq (l : list A) (x y : A) : x ≠ y → nb y (x :: l) = nb y l.

  Lemma nb_cons_eq (l : list A) (x y : A) : x = y → nb y (x :: l) = S (nb y l).

  Lemma NoDup_nb' (l : list A) : NoDup l ↔ (∀ x : A, x ∈ l → nb x l = 1).

If l is contained in m and if m has no duplicates, then the length of l can be obtained by summing over m the function that maps a to the number of occurrences of a in l.

  Lemma length_sum_filter l m:
    l ⊆ m → NoDup m → ⎢l ⎥ = sum (fun a ⇒ nb a l) m.

  Lemma sum_incr_0_left f (l m : list A) :
    (∀ x, ¬ x ∈ l → f x = 0) → sum f {{l }} = sum f {{m ++l }}.

  Lemma sum_incr_0_right f (l m : list A) :
    (∀ x, ¬ x ∈ l → f x = 0) → sum f {{l }} = sum f {{l ++m }}.

A list m appears in shuffles l exactly when for every a:A there are as may occurrences of a in l as in m.

Lemma shuffles_spec (m l : list A) : m ∈ shuffles l ↔ ∀ a, nb a l = nb a m.

Intersection of finite sets

  Definition intersect u v := (fun a ⇒ inb a v ) :> u.
  Infix " ∩ " := intersect (at level 50).

  Lemma intersect_spec u v a : a ∈ u ∩ v ↔ a ∈ u ∧ a ∈ v.

  Global Instance intersect_proper_incl :
    Proper (@incl _ ==> @incl _ ==> @incl _) intersect.

  Global Instance intersect_proper :
    Proper (@equivalent _ ==> @equivalent _ ==> @equivalent _) intersect.

  Lemma interect_nil u : u ∩ [] = [].

  Lemma intersect_app_l u v w : (u ++v ) ∩ w = (u ∩w )++(v ∩w ).

  Lemma intersect_app_r u v w : u ∩(v ++w ) ≈ (u ∩v )++(u ∩w ).

  Lemma intersect_ass u v w : u ∩ (v ∩ w ) = (u ∩ v ) ∩ w.
  Lemma intersect_comm u v : u ∩ v ≈ v ∩ u.

  Lemma intersect_meet_l u v : u ⊆ v → u ∩ v = u.

  Lemma intersect_incl u v : u ∩ v ⊆ u.

Difference of finite sets

  Definition difference u v := (fun a ⇒ negb (inb a v)) :> u.
  Infix " − " := difference (at level 50).

  Lemma difference_spec u v a : a ∈ u − v ↔ a ∈ u ∧ ¬ a ∈ v.

  Global Instance difference_proper :
    Proper (@equivalent _ ==> @equivalent _ ==> @equivalent _) difference.

  Global Instance difference_proper_inf :
    Proper (@incl _ ==> Basics.flip (@incl _) ==> @incl _) difference.

  Remark difference_right_subs u v w : u ≈ v → w − u = w − v.

  Lemma difference_app_l u v w : (u ++v )−w = (u −w )++(v −w ).
  Lemma difference_app_r u v w : u −(v ++w ) ≈ (u −v )∩(u −w ).
  Lemma difference_inter_r u v w : u −(v ∩w ) ≈ (u −v )++(u −w ).
  Lemma difference_inter_l u v w : (u ∩v )−w ≈ (u −w )∩(v −w ).
  Lemma difference_nil u : u − [] = u.

  Lemma difference_incl u v : u − v ⊆ u.

  Lemma difference_intersect u v : v ∩ (u − v ) = [].

End dec_list.
Notation " l ∖ a " := (rm a l) (at level 50).
Notation " l ⊖ a " := (rmfst a l) (at level 50).
Notation nb a l := ⎢eqX a :> l⎥.
Notation " {{ l }} " := (undup l) (at level 0).
Infix " ∩ " := intersect (at level 50).
  Infix " − " := difference (at level 50).

Lemma nb_map {A B :Set} `{decidable_set A,decidable_set B} (f : A → B) :
  (∀ x1 x2 : A, f x1 = f x2 → x1 = x2 ) →
  ∀ (x : A) (l : list A), nb x l = nb (f x) (map f l).

Lemma rmfst_flip {A B : Set} `{decidable_set A,decidable_set B} (s : list (A ×B)) a b :
  s ` ⊖ (a ,b ) = (s ⊖ (b ,a ))`.

insert commutes with map.

Lemma insert_map {A B : Set} `{decidable_set A,decidable_set B} :
∀ (f : A → B) l a, insert (f a) (map f l) = map (map f) (insert a l).

shuffles commutes with map.

Lemma shuffles_map {A B : Set} `{decidable_set A,decidable_set B} :
  ∀ (f : A → B) l, shuffles (map f l) = map (map f) (shuffles l).

Global Instance DecidableProp_In (A : Set) (x : A) l :
  decidable_set A → DecidableProp (x ∈ l).
Global Instance DecidableProp_Incl (A : Set) (l m : list A) :
  decidable_set A → DecidableProp (l ⊆ m).
Global Instance DecidableProp_Equiv (A : Set) (l m : list A) :
  decidable_set A → DecidableProp (l ≈ m).