Library CoLoR.Util.List.ListShrink

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Stephane Le Roux, 2006-10-17
prefix, suffix, cut, elimination of doubles, etc.

Set Implicit Arguments.


prefix

Section prefix.

  Variable A : Type.

  Fixpoint prefix (l l' : list A) : Prop :=
    match l with
      | nil => True
      | x::l => match l' with
                  | nil => False
                  | y::l' => x=y /\ prefix l l'
                end
    end.

  Lemma prefix_nil : forall l : list A, prefix l nil -> l = nil.

  Lemma reflexive_prefix : forall l : list A, prefix l l.

  Lemma prefix_incl : forall l l' : list A, prefix l l' -> incl l l'.

  Lemma prefix_app_right_right : forall l l' l'',
    prefix l l' -> prefix l (l' ++ l'').

  Lemma prefix_smaller : forall (x : A) l l',
    l <> l'++x::nil -> prefix l (l'++x::nil) -> prefix l l'.

End prefix.

suffix

Section suffix.

  Variable A : Type.

  Definition suffix (l l' : list A) : Prop := prefix (rev l)(rev l').

  Lemma suffix_incl : forall l l' : list A, suffix l l' -> incl l l'.

  Lemma suffix_smaller : forall l (x : A) l',
    l <> x::l' -> suffix l (x::l') -> suffix l l'.

End suffix.

cut

Section cut.

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

  Fixpoint cut (x : A) (l : list A) : list A :=
    match l with
      | nil => nil
      | y::l' => if eq_dec x y then l else cut x l'
    end.

  Lemma suffix_cut : forall (x : A) l, suffix (cut x l) l.

  Lemma cut_head : forall (x : A) l, In x l -> cut x l = x::(tail (cut x l)).

  Lemma length_cut : forall (x : A) l, length (cut x l) <= length l.

  Lemma length_tail_cut_cons : forall (x y : A) l,
    length (tail (cut x (y::l))) <= length l.

  Lemma nodup_cut : forall (x : A) l,
    nodup l -> nodup (cut x l).

  Lemma incl_cut : forall (x : A) l, incl (cut x l) l.

End cut.

shrink

Section shrink.

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

  Fixpoint shrink (l :list A) : list A :=
    match l with
      | nil => nil
      | x::l => if In_dec eq_dec x (shrink l) then cut eq_dec x (shrink l)
        else x::(shrink l)
    end.

  Lemma nodup_shrink : forall l : list A, nodup (shrink l).

  Lemma incl_shrink : forall l : list A, incl (shrink l) l.


  Lemma length_shrink : forall l l' : list A,
    incl l l' -> length (shrink l) <= length l'.

End shrink.