Library Coq.Sorting.Sorting
Require
Import
List
Multiset
Permutation
Relations
.
Section
defs
.
Variable
A
:
Type
.
Variable
leA
:
relation
A
.
Variable
eqA
:
relation
A
.
Let
gtA
(
x
y
:A) := ~
leA
x
y
.
Hypothesis
leA_dec
:
forall
x
y
:A, {
leA
x
y
} + {
leA
y
x
}.
Hypothesis
eqA_dec
:
forall
x
y
:A, {
eqA
x
y
} + {~
eqA
x
y
}.
Hypothesis
leA_refl
:
forall
x
y
:A,
eqA
x
y
->
leA
x
y
.
Hypothesis
leA_trans
:
forall
x
y
z
:A,
leA
x
y
->
leA
y
z
->
leA
x
z
.
Hypothesis
leA_antisym
:
forall
x
y
:A,
leA
x
y
->
leA
y
x
->
eqA
x
y
.
Hint
Resolve
leA_refl
.
Hint
Immediate
eqA_dec
leA_dec
leA_antisym
.
Let
emptyBag
:=
EmptyBag
A
.
Let
singletonBag
:=
SingletonBag
_
eqA_dec
.
lelistA
Inductive
lelistA
(
a
:A) :
list
A
->
Prop
:=
|
nil_leA
:
lelistA
a
nil
|
cons_leA
:
forall
(
b
:A) (
l
:list
A
),
leA
a
b
->
lelistA
a
(
b
::
l
).
Lemma
lelistA_inv
:
forall
(
a
b
:A) (
l
:list
A
),
lelistA
a
(
b
::
l
) ->
leA
a
b
.
Definition for a list to be sorted
Inductive
sort
:
list
A
->
Prop
:=
|
nil_sort
:
sort
nil
|
cons_sort
:
forall
(
a
:A) (
l
:list
A
),
sort
l
->
lelistA
a
l
->
sort
(
a
::
l
).
Lemma
sort_inv
:
forall
(
a
:A) (
l
:list
A
),
sort
(
a
::
l
) ->
sort
l
/\
lelistA
a
l
.
Lemma
sort_rect
:
forall
P
:list
A
->
Type
,
P
nil
->
(
forall
(
a
:A) (
l
:list
A
),
sort
l
->
P
l
->
lelistA
a
l
->
P
(
a
::
l
)) ->
forall
y
:list
A
,
sort
y
->
P
y
.
Lemma
sort_rec
:
forall
P
:list
A
->
Set
,
P
nil
->
(
forall
(
a
:A) (
l
:list
A
),
sort
l
->
P
l
->
lelistA
a
l
->
P
(
a
::
l
)) ->
forall
y
:list
A
,
sort
y
->
P
y
.
Merging two sorted lists
Inductive
merge_lem
(
l1
l2
:list
A
) :
Type
:=
merge_exist
:
forall
l
:list
A
,
sort
l
->
meq
(
list_contents
_
eqA_dec
l
)
(
munion
(
list_contents
_
eqA_dec
l1
) (
list_contents
_
eqA_dec
l2
)) ->
(
forall
a
:A,
lelistA
a
l1
->
lelistA
a
l2
->
lelistA
a
l
) ->
merge_lem
l1
l2
.
Lemma
merge
:
forall
l1
:list
A
,
sort
l1
->
forall
l2
:list
A
,
sort
l2
->
merge_lem
l1
l2
.
End
defs
.
Hint
Constructors
sort
:
datatypes
v62
.
Hint
Constructors
lelistA
:
datatypes
v62
.