Library CoLoR.Util.List.ListExtras

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-28
Some additional functions on lists.

Set Implicit Arguments.


initial segment of a list

Section InitialSeg.

  Variable A : Type.

  Fixpoint initialSeg (l: list A) (size: nat) {struct size} : list A :=
  match size, l with
  | O, _ => nil
  | _, nil => nil
  | S n, hd::tl => hd :: initialSeg tl n
  end.

  Lemma initialSeg_full : forall l n, n >= length l -> initialSeg l n = l.

  Lemma initialSeg_length : forall (l: list A) size,
    length (initialSeg l size) = min size (length l).

  Lemma initialSeg_nth : forall (l: list A) size x, x < size ->
    nth_error (initialSeg l size) x = nth_error l x.

  Lemma initialSeg_prefix : forall (l: list A) x p el,
    nth_error (initialSeg l x) p = Some el -> nth_error l p = Some el.

  Lemma initialSeg_app : forall l l' n,
    n <= length l -> initialSeg (l ++ l') n = initialSeg l n.

End InitialSeg.

sublist

Section Seg.

  Variable A : Type.

  Fixpoint seg (l: list A) (from size : nat) {struct from} : list A :=
  match from, l with
  | 0, _ => initialSeg l size
  | _, nil => nil
  | S n, hd::tl => seg tl n size
  end.

  Lemma seg_tillEnd : forall l m n,
    n >= length l - m -> seg l m n = seg l m (length l - m).

  Lemma seg_nth : forall (l: list A) i j x,
    x < j -> nth_error (seg l i j) x = nth_error l (i + x).

  Lemma seg_exceeded l k n : n >= length l -> seg l k n = seg l k (length l).

End Seg.

final segment of a list

Section FinalSeg.

  Variable A: Type.

  Definition finalSeg (l: list A) fromPos
    := seg l fromPos (length l - fromPos).

  Lemma finalSeg_full l : finalSeg l 0 = l.

  Lemma finalSeg1_tail : forall l, finalSeg l 1 = tail l.

  Lemma finalSeg_empty : forall l k, k >= length l -> finalSeg l k = nil.

  Lemma finalSeg_cons : forall a l, finalSeg (a::l) 1 = l.

  Lemma nth_finalSeg_nth: forall l k p,
    nth_error (finalSeg l k) p = nth_error l (k + p).

  Lemma finalSeg_nth_nth : forall l k p, p >= k ->
    nth_error l p = nth_error (finalSeg l k) (p - k).

  Lemma finalSeg_length : forall l k, length (finalSeg l k) = length l - k.

  Lemma finalSeg_app_right : forall (l: list A) k n, n > length l ->
    finalSeg (l ++ k) n = finalSeg k (n - length l).

  Lemma finalSeg_nth_idx : forall l i j a,
    nth_error (finalSeg l i) j = Some a -> length l > i + j.

  Lemma initialFinalSeg_length : forall l k,
    length (initialSeg l k) + length (finalSeg l k) = length l.

  Lemma initialSeg_finalSeg_full : forall l k,
    initialSeg l k ++ finalSeg l k = l.

End FinalSeg.

create copies of an element

Section Copy.

  Variable A : Type.

  Fixpoint copy (n : nat) (el : A) : list A :=
  match n with
  | 0 => nil
  | S n => el :: copy n el
  end.

  Lemma copy_split : forall a m n, copy (m + n) a = copy m a ++ copy n a.

  Lemma copy_length : forall n el, length (copy n el) = n.

  Lemma copy_in : forall n el x, In x (copy n el) -> x = el.

  Lemma nth_copy_in : forall n el x,
    x < n -> nth_error (copy n el) x = Some el.

  Lemma nth_after_copy : forall n el el',
    nth_error (copy n el' ++ el::nil) n = Some el.

  Lemma copy_cons : forall n el, el :: copy n el = copy (S n) el.

  Lemma copy_add : forall n el l, el :: copy n el ++ l = copy n el ++ el :: l.

  Lemma initialSeg_copy : forall el n k,
    initialSeg (copy n el) k = copy (min n k) el.

  Lemma finalSeg_copy : forall l el k n, k <= n ->
     finalSeg (copy n el ++ l) k = copy (n - k) el ++ l.

End Copy.

insert an element

Section InsertNth.

  Variable A : Type.

  Definition insert_nth (l: list A) (n: nat) (el: A) : list A :=
    initialSeg l n ++ el :: finalSeg l n.

  Lemma insert_nth_step : forall a l n el,
    insert_nth (a :: l) (S n) el = a :: insert_nth l n el.

  Lemma nth_insert_nth : forall l p el,
    length l >= p -> nth_error (insert_nth l p el) p = Some el.

End InsertNth.

erase an element

Section DropNth.

  Variable A : Type.

  Definition drop_nth (l: list A) n := initialSeg l n ++ finalSeg l (S n).

  Lemma drop_nth_in_length : forall p l,
    length l > p -> length (drop_nth l p) = pred (length l).

  Lemma drop_nth_beyond : forall l p, length l <= p -> drop_nth l p = l.

  Lemma drop_nth_length : forall l p,
    length (drop_nth l p) >= pred (length l).

  Lemma drop_nth_cons : forall a l, drop_nth (a::l) 0 = l.

  Lemma drop_nth_succ : forall a l p,
    drop_nth (a::l) (S p) = a :: drop_nth l p.

  Lemma drop_nth_insert_nth : forall l p el,
    length l >= p -> drop_nth (insert_nth l p el) p = l.

  Lemma insert_nth_drop_nth : forall p l el, nth_error l p = Some el ->
    insert_nth (drop_nth l p) p el = l.

End DropNth.

number of occurrences of an element

Section CountIn.

  Variables
    (A : Type) (eqA : relation A)
    (eqA_dec : forall x y, {eqA x y} + {~eqA x y})
    (eqA_Equivalence : Equivalence eqA).

  Fixpoint countIn (a: A) (l: list A) : nat :=
    match l with
      | nil => 0
      | x::xs =>
        match eqA_dec a x with
        | left _ => S(countIn a xs)
        | right _ => countIn a xs
        end
    end.

  Lemma in_countIn : forall a a' l, In a l -> eqA a a' -> countIn a' l > 0.

  Lemma count_pos_in : forall a (l: list A),
    countIn a l > 0 -> exists a', eqA a a' /\ In a' l.

  Lemma countIn_nth : forall a (l: list A), countIn a l > 0 ->
    exists p, exists a', eqA a a' /\ nth_error l p = Some a'.

  Lemma countIn_dropNth_eq : forall l p el el',
    nth_error l p = Some el' -> eqA el el' ->
    countIn el (drop_nth l p) = countIn el l - 1.

  Lemma countIn_dropNth_neq : forall l p el el',
    nth_error l p = Some el' -> ~eqA el el' ->
    countIn el (drop_nth l p) = countIn el l.

End CountIn.

erase the last element of a list

Section DropLast.

  Variable A : Type.

  Fixpoint dropLast (l: list A) : list A :=
    match l with
    | nil => nil
    | x::nil => nil
    | x::xs => x :: dropLast xs
    end.

  Lemma dropLast_last : forall a (l: list A),
    l <> nil -> dropLast (l ++ a::nil) = l.

  Lemma dropLast_eq : forall l1 l2, l1 = l2 -> dropLast l1 = dropLast l2.

  Lemma dropLast_app : forall a (l1 l2: list A),
    dropLast (l1 ++ a :: l2) = l1 ++ dropLast (a :: l2).

End DropLast.

last element of a list

Section Last.

  Variable A : Type.

  Fixpoint last (l: list A) : option A :=
    match l with
    | nil => error
    | x::nil => value x
    | x::xs => last xs
    end.

  Lemma last_eq : forall (l1 l2: list A), l1 = l2 -> last l1 = last l2.

  Lemma last_app : forall a (l1 l2: list A),
    last (l1 ++ a :: l2) = last (a :: l2).

  Lemma dropLast_plus_last : forall (l1: list A) a b,
    last (a :: l1) = Some b -> dropLast (a :: l1) ++ b :: nil = a :: l1.

End Last.

remove the first occurrence of an element

Section Remove.

  Variable A : Type.
  Variable eqA : relation A.
  Variable eqA_dec : forall x y, {eqA x y} + {~eqA x y}.

  Fixpoint removeElem (el: A) (l: list A) : list A :=
    match l with
    | nil => nil
    | hd::tl =>
      match eqA_dec el hd with
      | left _ => tl
      | right _ => hd::removeElem el tl
      end
    end.

  Fixpoint removeAll (l m: list A) : list A :=
    match m with
    | nil => l
    | hd::tl => removeAll (removeElem hd l) tl
    end.

  Lemma removeElem_length_in : forall a l, (exists a', eqA a a' /\ In a' l) ->
    length (removeElem a l) = pred (length l).

End Remove.

find the first/last occurrence of an element

Section Find.

  Variable A : Type.
  Variable P : A -> Prop.
  Variable P_dec : forall a : A, {P a} + {~P a}.

Lemma exists_in_list_dec : forall l,
  {exists r, P r /\ In r l} + {~exists r, P r /\ In r l}.

  Fixpoint find_first (l: list A) : option nat :=
    match l with
    | nil => None
    | hd::tl =>
      match P_dec hd with
      | left _ => Some 0
      | right _ =>
        match find_first tl with
        | None => None
        | Some i => Some (S i)
        end
      end
    end.

  Fixpoint find_last (l: list A) : option nat :=
    match l with
    | nil => None
    | hd::tl =>
      match find_last tl with
      | Some i => Some (S i)
      | None =>
        match P_dec hd with
        | left _ => Some 0
        | right _ => None
        end
      end
    end.

  Lemma find_first_ok : forall l p, find_first l = Some p ->
    exists el, nth_error l p = Some el /\ P el.

  Lemma find_last_ok : forall l p, find_last l = Some p ->
    exists el, nth_error l p = Some el /\ P el.

  Lemma find_last_last: forall l p el, nth_error l p = Some el -> P el ->
    exists q, find_last l = Some q /\ q >= p.

Lemma find_first_exist : forall x l, In x l -> P x -> find_first l <> None.

Lemma find_first_Some : forall l,
  find_first l <> None -> exists z, In z l /\ P z.

Lemma find_first_Some_bound : forall l x,
  find_first l = Some x -> x < length l.

Lemma In_find_first2 : forall l z,
  find_first l = Some z -> exists y, l[z] = Some y /\ P y.

Lemma find_first_exact : forall l i,
  find_first l = Some i -> exists z, l[i] = Some z /\ P z.

End Find.


Section Find_more.

Variable A : Type.
Variables P Q : A -> Prop.
Variable P_dec : forall a : A, {P a} + {~P a}.
Variable Q_dec : forall a : A, {Q a} + {~Q a}.

Lemma find_first_indep : (forall x, P x <-> Q x) ->
  forall l, find_first P P_dec l = find_first Q Q_dec l.

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

Lemma eq_In_find_first : forall x l, In x l ->
  exists z, find_first (eq x) (eq_dec x) l = Some z /\ l[z] = Some x.

Lemma eq_find_first_exact : forall l x z,
  find_first (eq x) (eq_dec x) l = Some z -> l[z] = Some x.

Lemma element_at_find_first_eq : forall l x i,
  l[i] = Some x -> exists j, j <= i /\ find_first (eq x) (eq_dec x) l = Some j.

End Find_more.


decidability of finding an element satisfying some relation

Section List_Rel_Dec.

  Variable A : Type.
  Variable B : Type.
  Variable P : A -> Prop.
  Variable R : A -> B -> Prop.

  Lemma many_one_dec : forall (l : list A) r,
    (forall x, In x l -> {R x r} + {~R x r})
    -> {x : A | In x l /\ R x r} + {forall x, In x l -> ~R x r}.

  Lemma list_dec_all : forall (l : list A),
    (forall x, In x l -> {P x} + {~P x}) ->
    {forall x, In x l -> P x} + {exists x, In x l /\ ~P x}.

End List_Rel_Dec.

hints