Require Import Coqlib.
Require Import List.
Section S.
Variable A :
Type.
Variable le :
A ->
A ->
bool.
Fixpoint insert (
e :
A) (
l :
list A) :
list A :=
match l with
|
nil =>
e ::
l
|
e' ::
l =>
if le e e'
then e ::
e' ::
l
else e' :: (
insert e l)
end.
Lemma In_insert :
forall l e a,
In e (
insert a l) <->
(
e =
a \/
In e l).
Proof.
induction l ; simpl ; intros.
intuition.
destr. rewrite IHl in H0. firstorder.
right. rewrite IHl. auto.
right. rewrite IHl. auto.
Qed.
Fixpoint sort (
l :
list A) :=
match l with
|
nil =>
nil
|
e ::
l =>
insert e (
sort l)
end.
Lemma In_sort :
forall l e,
In e l <->
In e (
sort l).
Proof.
induction l ;
simpl.
-
tauto.
-
intros.
rewrite IHl.
rewrite In_insert.
intuition.
Qed.
Inductive Sorted:
list A ->
Prop :=
|
Sorted_nil:
Sorted nil
|
Sorted_cons:
forall hd tl,
(
forall x,
In x tl ->
le hd x =
true) ->
Sorted tl ->
Sorted (
hd ::
tl).
Hypothesis le_trans:
forall a b c,
le a b =
true ->
le b c =
true ->
le a c =
true.
Hypothesis le_false:
forall a b,
le a b =
false ->
le b a =
true.
Lemma insert_sorted:
forall l (
s:
Sorted l)
a,
Sorted (
insert a l).
Proof.
induction 1;
simpl;
intros.
-
constructor.
easy.
constructor.
-
destr.
+
constructor;
auto.
*
simpl;
destr.
apply H in H1.
eapply le_trans;
eauto.
*
constructor;
auto.
+
constructor;
auto.
simpl;
intros.
rewrite In_insert in H0.
destr.
subst.
apply le_false;
auto.
apply H;
auto.
Qed.
Lemma sort_sorted:
forall l,
Sorted (
sort l).
Proof.
induction l;
simpl;
intros.
-
constructor.
-
apply insert_sorted;
auto.
Qed.
Lemma insert_split:
forall a l,
exists l1 l2,
insert a l =
l1 ++
a::
l2 /\
l =
l1 ++
l2.
Proof.
induction l;
simpl;
intros.
-
exists nil,
nil.
split;
reflexivity.
-
destruct IHl as [
l1 [
l2 [
B C]]].
destr.
exists nil, (
a0::
l);
split;
reflexivity.
rewrite B.
exists (
a0::
l1),
l2;
split.
reflexivity.
rewrite C;
reflexivity.
Qed.
Require Import Permutation.
Lemma sort_permut:
forall l,
Permutation l (
sort l).
Proof.
Lemma filter_if:
forall A (
f:
A ->
bool) (
a:
bool)
b c,
filter f (
if a then b else c) =
if a then filter f b else filter f c.
Proof.
intros; destr.
Qed.
Lemma insert_le:
forall l a0 a,
le a0 a =
true ->
(
forall x :
A,
In x l ->
le a x =
true) ->
insert a0 l =
a0::
l.
Proof.
induction l;
simpl;
intros;
auto.
destr.
erewrite le_trans in Heqb.
congruence.
eauto.
apply H0.
auto.
Qed.
Lemma filter_insert:
forall f l a,
Sorted l ->
filter f (
insert a l) =
(
if f a then insert a (
filter f l)
else filter f l).
Proof.
induction l;
simpl;
intros;
auto.
rewrite filter_if.
simpl.
rewrite IHl by (
inv H;
auto).
repeat destr.
inv H.
erewrite insert_le.
auto.
eauto.
intros.
apply H2.
rewrite filter_In in H.
destr.
Qed.
Lemma filter_sort:
forall f l,
filter f (
sort l) =
sort (
filter f l).
Proof.
End S.
Require Import Ctypes.
Require Import PpsimplZ.
Require Import Psatz.
Definition le1 (
a b : (
AST.ident *
type)) :
bool :=
proj_sumbool (
zle (
sizeof (
snd a)) (
sizeof (
snd b))).
Lemma le1_trans:
forall a b c,
le1 a b =
true ->
le1 b c =
true ->
le1 a c =
true.
Proof.
Lemma le1_false:
forall a b,
le1 a b =
false ->
le1 b a =
true.
Proof.
Definition varsort :=
sort _ le1.
Definition varsort_sorted :=
sort_sorted _ _ le1_trans le1_false.
Definition varsort_permut :=
sort_permut _ le1.
Definition varsort_filter :=
filter_sort _ _ le1_trans le1_false.
Definition le2 (
a b : (
AST.ident *
Z)) :
bool :=
proj_sumbool (
zle ((
snd a)) (
snd b)).
Lemma le2_trans:
forall a b c,
le2 a b =
true ->
le2 b c =
true ->
le2 a c =
true.
Proof.
Lemma le2_false:
forall a b,
le2 a b =
false ->
le2 b a =
true.
Proof.
Definition varsort' :=
sort _ le2.
Definition varsort'
_sorted :=
sort_sorted _ _ le2_trans le2_false.
Definition varsort'
_permut :=
sort_permut _ le2.
Definition varsort'
_filter :=
filter_sort _ _ le2_trans le2_false.