Library CoLoR.Util.List.ListNodup

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-02-16
  • Stephane Le Roux, 2006-10-17
Lists without duplicated elements

Set Implicit Arguments.


Section S.

  Variable A : Type.

Predicate saying if a list has no duplicated element.

  Fixpoint nodup (l : list A) : Prop :=
    match l with
      | nil => True
      | a :: l' => ~In a l' /\ nodup l'
    end.

  Lemma nodup_app_elim_right :
    forall l l', nodup (l++l') -> nodup l'.

  Lemma nodup_midex_incl_length : eq_midex A ->
    forall l l', nodup l -> incl l l' -> length l <= length l'.

Properties of nodup.

  Variable eq_dec : forall x y : A, {x=y}+{~x=y}.

  Lemma nodup_unique : forall l (x:A),
    nodup l -> forall n m, l[n] = Some x -> l[m] = Some x -> n=m.

  Lemma nodup_incl_length : forall l l' : list A,
    nodup l -> incl l l' -> length l <= length l'.

  Lemma nodup_last : forall (a : A) l,
    nodup l -> ~In a l -> nodup (l ++ a :: nil).

  Lemma nodup_rev : forall l : list A,
    nodup l -> nodup (rev l).

  Lemma nodup_app_elim : forall l m : list A, nodup (l ++ m) ->
    nodup l /\ nodup m /\ forall x, In x l -> ~In x m.


  Lemma nodup_app_cons : forall l (x : A) m,
    nodup (l ++ x :: m) -> ~In x l /\ ~In x m.

  Lemma length_remove_nodup (x : A) : forall l, nodup l ->
    In x l -> length (remove eq_dec x l) = length l - 1.

  Lemma nodup_incl_length_le :
    forall l m : list A, nodup l -> l [= m -> length l <= length m.

  Lemma nodup_remove (x : A) :
    forall l, nodup l -> nodup (remove eq_dec x l).

  Lemma In_nodup_elim (x : A) : forall l, In x l -> nodup l ->
    exists l1 l2, l = l1 ++ x :: l2 /\ ~In x l1 /\ ~In x l2.


  Lemma inj_nth_nodup (x : A) l i j : nodup l ->
    i < length l -> j < length l -> nth i l x = nth j l x -> i = j.

  Lemma nodup_select (f : A->Prop) (f_dec : forall x, {f x}+{~f x}) :
    forall l, nodup l -> nodup (select f_dec l).

Least prefix with no duplicated element.

  Fixpoint greatest_nodup_prefix_aux (acc l : list A) : list A :=
    match l with
      | nil => rev acc
      | cons x l =>
        match In_dec eq_dec x acc with
          | left _ => rev acc
          | right _ => greatest_nodup_prefix_aux (x :: acc) l
        end
    end.

  Notation greatest_nodup_prefix := (greatest_nodup_prefix_aux nil).

greatest_nodup_prefix properties

  Lemma greatest_nodup_prefix_aux_correct : forall l acc,
    nodup acc -> nodup (greatest_nodup_prefix_aux acc l).

  Lemma greatest_nodup_prefix_correct : forall l,
    nodup (greatest_nodup_prefix l).

  Lemma greatest_nodup_prefix_aux_elim : forall l acc,
    exists p, greatest_nodup_prefix_aux acc l = rev acc ++ p.

  Lemma greatest_nodup_prefix_aux_app : forall m l acc,
    nodup l -> (forall x, In x l -> ~In x acc) ->
    greatest_nodup_prefix_aux acc (l ++ m)
    = greatest_nodup_prefix_aux (rev l ++ acc) m.


  Lemma greatest_nodup_prefix_app : forall m l, nodup l ->
    greatest_nodup_prefix (l ++ m)
    = greatest_nodup_prefix_aux (rev l) m.


  Lemma nodup_greatest_nodup_prefix : forall l,
    nodup l -> greatest_nodup_prefix l = l.

  Lemma greatest_nodup_prefix_intro: forall l,
    l = greatest_nodup_prefix l
    \/ exists x, In x (greatest_nodup_prefix l)
                 /\ exists p, l = greatest_nodup_prefix l ++ x :: p.

  Lemma greatest_nodup_prefix_intro' : forall l,
    exists m, l = greatest_nodup_prefix l ++ m.

  Lemma nodup_intro: forall l : list A, nodup l
    \/ exists m x p, l = m ++ x :: p /\ nodup m /\ In x m.

  Lemma nodup_intro' : forall l : list A,
    exists m p, l = m ++ p /\ nodup m.

Remove duplicated elements of a list.

  Fixpoint remdup l :=
    match l with
      | nil => nil
      | t :: q => t :: remove eq_dec t (remdup q)
    end.

  Lemma nodup_remdup : forall l, nodup (remdup l).

  Lemma remdup_incl : forall l, remdup l [= l.

  Lemma incl_remdup : forall l, l [= remdup l.

  Lemma In_remdup x : forall l, In x (remdup l) <-> In x l.

Boolean function deciding nodup.


  Variables (beq : A -> A -> bool)
            (beq_ok : forall x y, beq x y = true <-> x = y).

  Fixpoint bnodup (l : list A) : bool :=
    match l with
      | nil => true
      | a :: l' => negb (mem beq a l') && bnodup l'
    end.

  Lemma bnodup_ok : forall l, bnodup l = true <-> nodup l.

End S.


Properties of nodup involving more than one type.


Lemma nodup_map_inj A B (f : A -> B) :
  injective f -> forall l, nodup l -> nodup (map f l).

Tactics.

Ltac nodup beq_ok := rewrite <- (bnodup_ok beq_ok); check_eq.