This module defines a simple (inefficient) insert sort, used in
various parts of the specification.
Require Export Sorting.
Require Import EquivDec.
Require Import List.
Require Import CoqLibAdd.
Require Import ListAdd.
Require Import Permutation.
Require Import Eqdep_dec.
Require Import RelationClasses.
Section SortingAdd.
Insertion sort
Section InsertionSort.
Context {
A:
Type}.
Context {
R:
A->
A->
Prop}.
Context (
R_dec :
forall a a', {
R a a'} + {~
R a a'}).
Fixpoint insertion_sort_insert a l
:=
match l with
|
nil =>
a ::
nil
|
b::
xs =>
if (
R_dec a b)
then a::
b::
xs
else if (
R_dec b a)
then
b::
insertion_sort_insert a xs
else b::
xs
end.
Fixpoint insertion_sort (
l:
list A)
:=
match l with
|
nil =>
nil
|
a::
xs =>
insertion_sort_insert a (
insertion_sort xs)
end.
Local Hint Constructors LocallySorted :
qcert.
Lemma insertion_sort_insert_Sorted a (
l:
list A) :
Sorted R l ->
Sorted R (
insertion_sort_insert a l).
Proof.
repeat rewrite Sorted_LocallySorted_iff.
induction l;
inversion 1;
subst;
simpl in *;
repeat match goal with
| [|-
context [
R_dec ?
x ?
y]] =>
destruct (
R_dec x y)
end;
eauto with qcert.
Qed.
Local Hint Resolve insertion_sort_insert_Sorted :
qcert.
Lemma insertion_sort_Sorted (
l:
list A) :
Sorted R (
insertion_sort l).
Proof.
induction l; simpl; eauto with qcert.
Qed.
Fixpoint is_list_sorted (
l:
list A) :=
match l with
|
nil =>
true
|
x::
xs =>
match xs with
|
nil =>
true
|
y::
ls =>
if R_dec x y then is_list_sorted xs else false
end
end.
Theorem is_list_sorted_Sorted_iff l:
is_list_sorted l =
true <->
Sorted R l.
Proof.
induction l;
simpl;
intuition.
-
destruct l;
simpl;
eauto.
destruct (
R_dec a a0);
simpl;
intuition;
try discriminate.
-
inversion H1;
subst.
rewrite H0;
auto.
destruct l;
auto.
inversion H5;
subst.
destruct (
R_dec a a0);
eauto.
Qed.
Corollary insertion_sort_is_list_sorted:
forall l,
is_list_sorted (
insertion_sort l) =
true.
Proof.
Lemma is_list_sorted_ext :
forall l (
p1 p2:
is_list_sorted l =
true),
p1 =
p2.
Proof.
Theorem is_list_sorted_StronglySorted `{
Transitive A R}:
forall l,
is_list_sorted l =
true <->
StronglySorted R l.
Proof.
Corollary insertion_sort_StronglySorted `{
Transitive A R}:
forall l,
StronglySorted R (
insertion_sort l).
Proof.
Lemma Forall_nin_irr `{
Irreflexive A R}:
forall a l,
Forall (
R a)
l -> ~
In a l.
Proof.
induction l; [
auto|
intros].
inversion H0;
subst;
intro.
inversion H1;
subst.
eapply irreflexivity;
eauto.
elim IHl;
auto.
Qed.
Lemma StronglySorted_NoDup `{
Irreflexive A R}:
forall l,
StronglySorted R l ->
NoDup l.
Proof.
induction l;
intros.
constructor.
inversion H0;
subst.
constructor;
auto.
eapply Forall_nin_irr;
eauto.
Qed.
Lemma Sorted_NoDup `{
StrictOrder A R}:
forall l,
Sorted R l ->
NoDup l.
Proof.
Lemma is_list_sorted_NoDup `{
StrictOrder A R} :
forall l,
is_list_sorted l =
true ->
NoDup l.
Proof.
Lemma is_list_sorted_cons a r :
is_list_sorted (
a::
r) =
true
<->
(
is_list_sorted r =
true
/\
match r with
|
nil =>
True
|
y::
_ =>
R a y
end).
Proof.
simpl;
destruct r;
intuition;
destruct (
R_dec a a0);
intuition congruence.
Qed.
Lemma is_list_sorted_cons_inv {
a r} :
is_list_sorted (
a::
r) =
true ->
is_list_sorted r =
true.
Proof.
Lemma StronglySorted_cons_in {
x a l} :
StronglySorted R (
a::
l) ->
In x l ->
R a x.
Proof.
inversion 1;
subst;
intros iin.
rewrite Forall_forall in H3.
auto.
Qed.
Lemma in_insertion_sort_insert {
x l a} :
In x (
insertion_sort_insert a l) ->
a =
x \/
In x l.
Proof.
revert x a.
induction l;
simpl; [
intuition | ].
intros x a0.
case_eq (
R_dec a0 a);
simpl;
intros;
trivial.
revert H0.
case_eq (
R_dec a a0);
simpl;
intros;
intuition.
destruct (
IHl _ _ H2);
intuition.
Qed.
Lemma in_insertion_sort {
x l} :
In x (
insertion_sort l) ->
In x l.
Proof.
Lemma is_list_sorted_cons_Forall_lt `{
Transitive A R} (
a:
A) :
forall l,
is_list_sorted (
a ::
l) =
true ->
Forall (
fun x =>
R a x) (
insertion_sort l).
Proof.
Lemma Forall_insertion_sort {
P}
l :
Forall P l ->
Forall P (
insertion_sort l).
Proof.
Lemma insertion_sort_sorted_is_id l :
is_list_sorted l =
true ->
insertion_sort l =
l.
Proof.
induction l;
intros;
simpl in *.
-
reflexivity.
-
assert (
is_list_sorted l =
true).
destruct l;
simpl in *;
try reflexivity.
destruct (
R_dec a a0);
congruence.
specialize (
IHl H0).
rewrite IHl;
clear IHl.
destruct l;
simpl in *;
try reflexivity.
revert H.
destruct (
R_dec a a0);
intros;
trivial.
destruct (
R_dec a0 a);
congruence.
Qed.
Lemma is_list_sorted_insert_sorted `{
Transitive A R}
a l:
is_list_sorted l =
true ->
is_list_sorted (
insertion_sort_insert a l) =
true.
Proof.
Theorem insertion_sort_sorted `{
Transitive A R}:
forall l,
is_list_sorted (
insertion_sort l) =
true.
Proof.
Lemma insertion_sort_idempotent l :
insertion_sort (
insertion_sort l) =
insertion_sort l.
Proof.
Lemma insertion_sort_insert_not_nil a l :
insertion_sort_insert a l <>
nil.
Proof.
induction l;
simpl;
intuition;
try discriminate.
destruct (
R_dec a a0);
simpl in *;
try discriminate.
destruct (
R_dec a0 a);
simpl in *;
try discriminate.
Qed.
Lemma insertion_sort_nil l :
insertion_sort l =
nil ->
l =
nil.
Proof.
Lemma insertion_sort_insert_swap a a0 l `{
StrictOrder A R}:
R a a0 ->
insertion_sort_insert a (
insertion_sort_insert a0 l) =
insertion_sort_insert a0 (
insertion_sort_insert a l).
Proof.
revert a a0.
induction l;
simpl;
intros.
-
destruct (
R_dec a a0);
simpl;
intuition.
destruct (
R_dec a0 a);
simpl;
intuition.
rewrite r0 in r.
eelim irreflexivity;
eauto.
-
destruct (
R_dec a1 a).
+
destruct (
R_dec a0 a).
*
simpl.
destruct (
R_dec a0 a1);
intuition.
destruct (
R_dec a1 a);
intuition.
destruct (
R_dec a1 a0);
intuition.
rewrite r3 in H0;
eelim irreflexivity;
eauto.
*
rewrite r in H0;
intuition.
+
destruct (
R_dec a0 a);
simpl.
*
destruct (
R_dec a1 a);
intuition.
destruct (
R_dec a0 a1);
intuition.
destruct (
R_dec a1 a0).
rewrite r1 in r0;
eelim irreflexivity;
eauto.
destruct (
R_dec a a1);
simpl;
destruct (
R_dec a0 a);
intuition.
*
destruct (
R_dec a a1);
destruct (
R_dec a a0);
simpl.
destruct (
R_dec a0 a).
rewrite r1 in r0;
eelim irreflexivity;
eauto.
destruct (
R_dec a a0);
intuition.
destruct (
R_dec a1 a).
rewrite r2 in r;
eelim irreflexivity;
eauto.
destruct (
R_dec a a1);
intuition.
f_equal;
eauto.
destruct (
R_dec a a0);
intuition.
destruct (
R_dec a1 a).
rewrite r0 in r;
eelim irreflexivity;
eauto.
destruct (
R_dec a0 a);
intuition.
destruct (
R_dec a a1);
intuition.
rewrite H0 in r;
intuition.
destruct (
R_dec a0 a);
intuition.
destruct (
R_dec a a0);
intuition.
destruct (
R_dec a1 a);
intuition.
destruct (
R_dec a a1);
intuition.
Qed.
End InsertionSort.
Properties of filter on sorted lists
Section Filter.
Lemma StronglySorted_filter {
A} {
R}
f {
l} :
@
StronglySorted A R l ->
StronglySorted R (
filter f l).
Proof.
induction l;
simpl;
trivial.
inversion 1;
simpl;
subst.
destruct (
f a);
auto.
constructor;
auto.
apply Forall_filter;
trivial.
Qed.
End Filter.
Properties of In on sorted lists
Section In.
Local Hint Resolve asymmetric_over_cons_inv :
qcert.
Lemma insertion_sort_insert_in_strong {
A R R_dec} {
x l a}
(
contr:
asymmetric_over R (
a::
l)) :
a =
x \/
In x l ->
In x (@
insertion_sort_insert A R R_dec a l).
Proof.
revert x a contr.
induction l;
simpl; [
intuition | ].
intros x a0.
case_eq (
R_dec a0 a);
simpl;
intros;
trivial.
revert H0.
case_eq (
R_dec a a0);
simpl;
intros;
intuition;
subst;
intuition.
-
right;
apply (
IHl x x);
intuition.
apply asymmetric_over_swap in contr.
eauto with qcert.
-
right.
apply (
IHl x a0);
intuition.
apply asymmetric_over_swap in contr.
eauto with qcert.
Qed.
Lemma insertion_sort_insert_in {
A R R_dec} {
x l a}
(
contr:
forall x y, ~
R x y -> ~
R y x ->
x =
y) :
a =
x \/
In x l ->
In x (@
insertion_sort_insert A R R_dec a l).
Proof.
Lemma insertion_sort_in_strong {
A R R_dec} {
x l}
(
contr:
asymmetric_over R l) :
In x l ->
In x (@
insertion_sort A R R_dec l).
Proof.
Local Hint Resolve asymmetric_asymmetric_over :
qcert.
Lemma insertion_sort_in {
A R R_dec} {
x l}
(
contr:
forall x y, ~
R x y -> ~
R y x ->
x =
y) :
In x l ->
In x (@
insertion_sort A R R_dec l).
Proof.
Lemma equivlist_insertion_sort_strong {
A R}
R_dec {
l l'}
(
contr:
asymmetric_over R l) :
equivlist l l' ->
equivlist (@
insertion_sort A R R_dec l) (@
insertion_sort A R R_dec l').
Proof.
Lemma equivlist_insertion_sort {
A R}
R_dec {
l l'}
(
contr:
forall x y, ~
R x y -> ~
R y x ->
x =
y) :
equivlist l l' ->
equivlist (@
insertion_sort A R R_dec l) (@
insertion_sort A R R_dec l').
Proof.
Lemma insertion_sort_insert_insertion_nin {
A:
Type}
lt dec
`{
StrictOrder A lt}
(
trich:
forall a b, {
lt a b} + {
eq a b} + {
lt b a})
(
a:
A)
a0 l :
~
lt a0 a ->
~
lt a a0 ->
insertion_sort_insert dec a0
(
insertion_sort_insert dec a l)
= @
insertion_sort_insert A lt dec a l.
Proof.
revert a a0. induction l; simpl; intros.
- repeat (match_destr; try congruence).
- repeat (match_destr; try congruence);
simpl; repeat (match_destr; try congruence); trivial.
+ rewrite l0 in l1. intuition.
+ rewrite IHl; trivial.
+ destruct (trich a a0) as [[?|?]|?];
try congruence.
+ destruct (trich a a0) as [[?|?]|?];
try congruence.
Qed.
Lemma insertion_sort_insert_cons_app {
A:
Type}
lt dec
`{
StrictOrder A lt}
(
trich:
forall a b, {
lt a b} + {
eq a b} + {
lt b a})
a l l2 :
insertion_sort dec (
insertion_sort_insert dec a l ++
l2) = @
insertion_sort A lt dec (
a::
l ++
l2).
Proof.
Lemma insertion_sort_insertion_sort_app1 {
A}
lt dec `{
StrictOrder A lt}
(
trich:
forall a b, {
lt a b} + {
eq a b} + {
lt b a})
l1 l2 :
insertion_sort dec (
insertion_sort dec l1 ++
l2) =
@
insertion_sort A lt dec (
l1 ++
l2).
Proof.
Lemma insertion_sort_trich_equiv {
A:
Type}
lt dec
(
trich:
forall a b, {
lt a b} + {
eq a b} + {
lt b a}) (
l:
list A)
:
equivlist (@
insertion_sort A lt dec l)
l.
Proof.
Lemma insertion_sort_insert_forall_lt
{
A:
Type}
lt dec (
a:
A) (
l:
list A) :
Forall (
lt a)
l ->
@
insertion_sort_insert A lt dec a l =
a ::
l.
Proof.
destruct l; simpl; trivial.
inversion 1; subst.
match_destr; intuition.
Qed.
Lemma sort_insert_filter_true {
A:
Type}
f lt dec `{
StrictOrder A lt}
(
trich:
forall a b, {
lt a b} + {
eq a b} + {
lt b a})
(
a:
A) (
l:
list A) :
StronglySorted lt l ->
f a =
true ->
filter f (@
insertion_sort_insert A lt dec a l)
=
insertion_sort_insert dec a (
filter f l).
Proof.
revert a.
induction l;
simpl;
intros b lsort fb.
-
rewrite fb;
trivial.
-
inversion lsort;
subst.
case_eq (
f a);
simpl;
intros fa.
+
destruct (
dec b a);
simpl.
*
rewrite fb.
simpl.
match_destr.
*
rewrite <-
IHl;
trivial.
match_destr;
simpl;
rewrite fa;
trivial.
+
match_destr.
*
simpl.
rewrite fb,
fa.
rewrite insertion_sort_insert_forall_lt;
trivial.
apply Forall_filter.
revert H3.
apply Forall_impl_in;
intros.
etransitivity;
eauto.
*
rewrite <-
IHl;
trivial.
match_destr;
simpl;
rewrite fa;
trivial.
destruct (
trich a b)
as [[?|?]|?];
try congruence.
Qed.
Lemma sort_insert_filter_false {
A:
Type}
f lt dec (
a:
A) (
l:
list A) :
f a =
false ->
filter f (@
insertion_sort_insert A lt dec a l) =
filter f l.
Proof.
revert a.
induction l; simpl; intros ? fa.
- rewrite fa; trivial.
- match_destr; simpl.
+ rewrite fa; trivial.
+ match_destr; simpl.
rewrite IHl; trivial.
Qed.
Lemma sort_filter_commute {
A:
Type}
f lt dec
`{
StrictOrder A lt}
(
trich:
forall a b, {
lt a b} + {
eq a b} + {
lt b a})
(
l:
list A) :
filter f (@
insertion_sort A lt dec l)
=
insertion_sort dec (
filter f l).
Proof.
End In.
Properties of map on sorted lists
Section Map.
Lemma map_insertion_sort_insert {
A B}
{
R1 R2}
(
R1_dec :
forall a a' :
A, {
R1 a a'} + {~
R1 a a'})
(
R2_dec :
forall b b' :
B, {
R2 b b'} + {~
R2 b b'})
(
f:
A->
B)
(
consistent:
forall x y,
R1 x y <->
R2 (
f x) (
f y))
a l :
map f (
insertion_sort_insert R1_dec a l) =
insertion_sort_insert R2_dec (
f a) (
map f l).
Proof.
induction l; simpl; trivial.
rewrite <- IHl.
destruct (consistent a a0); destruct (consistent a0 a).
repeat match_destr; simpl; try tauto.
Qed.
Lemma map_insertion_sort {
A B}
{
R1 R2}
(
R1_dec :
forall a a' :
A, {
R1 a a'} + {~
R1 a a'})
(
R2_dec :
forall b b' :
B, {
R2 b b'} + {~
R2 b b'})
(
f:
A->
B)
(
consistent:
forall x y,
R1 x y <->
R2 (
f x) (
f y))
l :
map f (
insertion_sort R1_dec l) =
insertion_sort R2_dec (
map f l).
Proof.
End Map.
Lemma insertion_sort_insert_nin_eq_inv {
A R}
dec (
a:
A)
l₁
l₂ :
insertion_sort_insert (
R:=
R)
dec a l₁ =
insertion_sort_insert dec a l₂ ->
~
In a l₁ ->
~
In a l₂ ->
l₁ =
l₂.
Proof.
revert l₂.
induction l₁; destruct l₂; simpl; intros eqq; trivial.
- intuition.
destruct (dec a a0); simpl in *.
+ invcs eqq.
+ destruct (dec a0 a); invcs eqq; tauto.
- intuition.
destruct (dec a a0); simpl in *.
+ invcs eqq.
+ destruct (dec a0 a); invcs eqq; tauto.
- intuition.
destruct (dec a a0); simpl in *.
+ invcs eqq.
destruct (dec a a1); simpl.
* invcs H4; trivial.
* destruct (dec a1 a); invcs H4; tauto.
+ destruct (dec a0 a).
* destruct (dec a a1); invcs eqq; try tauto.
destruct (dec a1 a); invcs H4; try tauto.
f_equal; eauto.
* { destruct (dec a a1).
- invcs eqq; tauto.
- destruct (dec a1 a); invcs eqq; try tauto.
}
Qed.
End SortingAdd.