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 T → list T → Prop :=
| Suffix_refl: ∀ xs, Suffix xs xs
| Suffix_cons: ∀ x xs ys, Suffix ys xs → Suffix 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
| nil ⇒ cons 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
| nil ⇒ nil
| cons x m ⇒ insert x (sort m)
end.
Lemma insert_ext : ∀ xs a a0,
a = a0 ∨ In a0 xs ↔ In a0 (insert a xs).
Require Setoid.
Lemma insert_sort_ext : ∀ xs a a0,
a = a0 ∨ In a0 xs ↔ In a0 (insert a (sort xs)).
Require Setoid.
Lemma sort_ext : ∀ (xs:list T),
let ys := sort xs in
incl xs ys ∧ incl ys xs.
Lemma sort_suffix :
∀ xs zs z, Suffix (z::zs) (sort xs) →
∀ z', In z' zs → R z z' = true.
Lemma sort_correct : ∀ (xs:list T),
let ys := sort xs in
incl xs ys ∧ incl ys xs ∧
∀ z zs, Suffix (z::zs) ys →
∀ z', In z' zs → R z z' = true.
Lemma nodup_sort : ∀ (xs:list T),
NoDup xs → NoDup (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
| nil ⇒ nil
| cons y ys ⇒ cons y
match ys with
| nil ⇒ nil
| 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 ys ∧ incl ys xs ∧ NoDup ys.
End Removing_consecutive_duplicates.
End ListExtras.
This page has been generated by coqdoc