Library lists

A file that involves general list sorting with respect to a nonstandard specification. The proofs are not finished.

Require Import List.


Section ListExtras.
Variable T:Type.

Inductive Suffix : list Tlist TProp :=
| Suffix_refl: ∀ xs, Suffix xs xs
| Suffix_cons: ∀ x xs ys, Suffix ys xsSuffix ys (x::xs).

Lemma Suffix_lem1 : ∀ xs ys:list T, Suffix xs ys
  ∃ zs, zs++xs=ys.

Lemma Suffix_incl : ∀ xs ys:list T, Suffix xs ys
  incl xs ys.

Section Sorting.

  Variable R:T->T->bool.

  Fixpoint insert x (l : list T) :=
    match l with
      | nilcons x nil
      | cons y m
        if R x y then (cons y (insert x m)) else (cons x l)
    end.

  Fixpoint sort (l : list T) : list T :=
    match l with
      | nilnil
      | cons x minsert x (sort m)
    end.

  Lemma insert_ext : ∀ xs a a0,
    a = a0In a0 xsIn a0 (insert a xs).
    Require Setoid.

  Lemma insert_sort_ext : ∀ xs a a0,
    a = a0In a0 xsIn a0 (insert a (sort xs)).
    Require Setoid.

  Lemma sort_ext : ∀ (xs:list T),
    let ys := sort xs in
      incl xs ysincl ys xs.

  Lemma sort_suffix :
      ∀ xs zs z, Suffix (z::zs) (sort xs) →
        ∀ z', In z' zsR z z' = true.

  Lemma sort_correct : ∀ (xs:list T),
    let ys := sort xs in
      incl xs ysincl ys xs
      ∀ z zs, Suffix (z::zs) ys
        ∀ z', In z' zsR z z' = true.

  Lemma nodup_sort : ∀ (xs:list T),
    NoDup xsNoDup (sort xs).


End Sorting.

Section Removing_consecutive_duplicates.

  Variable R:T->T->bool.
  Variable eqT_dec:forall x y:T, {x=y}+{x<>y}.

  Fixpoint nodup' (xs:list T) : list T :=
    match xs with
      | nilnil
      | cons y yscons y
        match ys with
          | nilnil
          | cons z zs
            if eqT_dec y z then (nodup' zs) else cons z (nodup' zs)
        end
    end.

  Definition nodup (xs:list T) : list T := nodup' (sort R xs).

  Lemma nodup_correct : ∀ xs:list T,
    let ys := nodup xs in
      incl xs ysincl ys xsNoDup ys.

End Removing_consecutive_duplicates.

End ListExtras.


This page has been generated by coqdoc