Skip to content

Instantly share code, notes, and snippets.

@y-taka-23

y-taka-23/coq_qsort.v

Last active December 11, 2015 01:49
Show Gist options
  • Save y-taka-23/4526374 to your computer and use it in GitHub Desktop.
Save y-taka-23/4526374 to your computer and use it in GitHub Desktop.
Download ZIP
Validation of the Quick Sort
Raw
coq_qsort.v
(******************************************************)
(** //// Validation of the Quick Sort //// *)
(******************************************************)
Section QuickSort.
Require Import Arith List.
Require Import Recdef.
Require Import Sorting.Sorted Sorting.Permutation.
(*////////////////////////////////////////////////////*)
(** Preliminaries *)
(*////////////////////////////////////////////////////*)
Section Preliminaries.
Variable A : Type.
(* Predicate : sublist l1 l2 <=> l1 is a sublist of l2. *)
Inductive sublist : list A -> list A -> Prop :=
| Sublist_nil : forall l : list A,
sublist nil l
| Sublist_cons1 : forall (x : A) (l1 l2 : list A),
sublist l1 l2 ->
sublist l1 (x :: l2)
| Sublist_cons2 : forall (x : A) (l1 l2 : list A),
sublist l1 l2 ->
sublist (x :: l1) (x :: l2).
(* Definition : Filter for the negatation *)
Fixpoint antifilter {A : Type} (f : A -> bool) (l : list A)
: list A :=
match l with
| nil => nil
| x :: l' => if f x
then antifilter f l'
else x :: antifilter f l'
end.
(* (filter f l) is a sublist of l. *)
Lemma filter_sublist : forall (f : A -> bool) (l : list A),
sublist (filter f l) l.
Proof.
intros f l.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply Sublist_nil.
(* Case : l = x :: l' *)
simpl.
case (f x).
(* Case : f x = true *)
apply Sublist_cons2.
apply H_l'.
(* Case : f x = false *)
apply Sublist_cons1.
apply H_l'.
Qed.
(* (antifilter f l) is a sublist of l. *)
Lemma antifilter_sublist : forall (f : A -> bool) (l : list A),
sublist (antifilter f l) l.
Proof.
intros f l.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply Sublist_nil.
(* Case : l = x :: l' *)
simpl.
case (f x).
(* Case : f x = true *)
apply Sublist_cons1.
apply H_l'.
(* Case : f x = false *)
apply Sublist_cons2.
apply H_l'.
Qed.
(* Sublists are shorter than or equal to the superlists. *)
Lemma sublist_length : forall l1 l2 : list A,
sublist l1 l2 ->
(l1 = l2 \/ length l1 < length l2).
Proof.
intros l1 l2 H_sub.
induction H_sub as [l2 | x l1 l2' H_sub H_ind |
x l1' l2' H_sub H_ind].
(* Case : l1 = nil *)
induction l2 as [| x l2' H_l2'].
(* Case : l2 = nil *)
left.
reflexivity.
(* Case : l2 = x1 :: l2' *)
right.
simpl.
apply lt_O_Sn.
(* Case : l2 = x :: l2' *)
right.
destruct H_ind as [H | H].
(* Case : l1 = l2' *)
rewrite H.
simpl.
apply lt_n_Sn.
(* Case : length l1 < length l2' *)
simpl.
apply (lt_trans (length l1) (length l2')
(S (length l2')) H).
apply lt_n_Sn.
(* Case : l1 = x :: l1', l2 = x :: l2' *)
destruct H_ind as [H | H].
(* Case : l1' = l2' *)
left.
rewrite H.
reflexivity.
(* Case : length l1' < length l2' *)
right.
simpl.
apply lt_n_S.
apply H.
Qed.
(* All components of (filter f l) are true for test function f. *)
Lemma filter_true : forall (f : A -> bool) (l : list A) (x : A),
In x (filter f l) -> f x = true.
Proof.
intros f l x H.
induction l as [| y l' H_l'].
(* Case : l = nil *)
simpl in H.
contradiction.
(* Case : l = y :: l' *)
simpl in H.
case_eq (f y).
(* Case : f y = true *)
intro H_y.
rewrite H_y in H.
unfold In in H.
destruct H as [H | H].
(* Case : y = x *)
rewrite <- H.
apply H_y.
(* Case : In x (filter f l') *)
apply H_l' in H.
apply H.
(* Case : f y = false *)
intro H_y.
rewrite H_y in H.
apply H_l' in H.
apply H.
Qed.
(* All components of (filter f l) are false for test function f. *)
Lemma antifilter_false : forall (f : A -> bool)
(l : list A) (x : A),
In x (antifilter f l) -> f x = false.
Proof.
intros f l x H.
induction l as [| y l' H_l'].
(* Case : l = nil *)
simpl in H.
contradiction.
(* Case : l = y :: l' *)
simpl in H.
case_eq (f y).
(* Case : f y = true *)
intro H_y.
rewrite H_y in H.
apply H_l' in H.
apply H.
(* Case : f y = false *)
intro H_y.
rewrite H_y in H.
destruct H as [H | H].
(* Case : y = x *)
rewrite <- H.
apply H_y.
(* Case : In x (antifilter f l') *)
apply H_l' in H.
apply H.
Qed.
(* sublist relation implies inclusion as component sets. *)
Lemma sublist_in : forall (l1 l2 : list A) (x : A),
In x l1 -> sublist l1 l2 -> In x l2.
Proof.
intros l1 l2 x H_in H_sub.
induction H_sub as [ | y l1 l2' H_sub H_ind |
y l1' l2' H_sub H_ind].
(* Case : l1 = nil *)
contradiction.
(* Case : l2 = y :: l2' *)
right.
apply (H_ind H_in).
(* Case : l1 = y :: l1', l2 = y :: l2' *)
destruct H_in as [H_in | H_in].
(* Case : y = x *)
left.
apply H_in.
(* Case : In x l1' *)
right.
apply (H_ind H_in).
Qed.
(* filter and antifilter split lists. *)
Lemma filter_or : forall (f : A -> bool) (l : list A) (x : A),
In x l <->
(In x (filter f l) \/ In x (antifilter f l)).
Proof.
intros f l x.
split.
(* Proof : Direction -> *)
intro H.
induction l as [| y l' H_l'].
(* Case : l = nil *)
left.
change (In x nil).
apply H.
(* Case : l = y :: l' *)
unfold In in H.
fold (In x l') in H.
destruct H as [H | H].
(* Case : y = x *)
rewrite H.
case_eq (f x).
(* Case : f x = true *)
intro H_x.
left.
unfold filter.
rewrite H_x.
left.
reflexivity.
(* Case : f x = false *)
intro H_x.
right.
unfold antifilter.
rewrite H_x.
left.
reflexivity.
(* Case : In x l' *)
apply H_l' in H.
destruct H as [H | H].
(* Case : In x (filter f l') *)
left.
case_eq (f y).
(* Case : f y = true *)
intro H_y.
unfold filter.
rewrite H_y.
right.
apply H.
(* Case : f y = false *)
intro H_y.
unfold filter.
rewrite H_y.
apply H.
(* Case : In x (antifilter f l') *)
right.
case_eq (f y).
(* Case : f y = true *)
intro H_y.
unfold antifilter.
rewrite H_y.
apply H.
(* Case : f y = false *)
intro H_y.
unfold antifilter.
rewrite H_y.
right.
apply H.
(* Proof : Direction <- *)
intro H.
destruct H as [H | H].
(* Case : In x (filter f l) *)
apply (sublist_in (filter f l) l x H).
apply filter_sublist.
(* Case : In x (antifilter f l) *)
apply (sublist_in (antifilter f l) l x H).
apply antifilter_sublist.
Qed.
(* The merger of filter and antifilter *)
(* is the permutation of the original. *)
Lemma filter_Permutation : forall (f : A -> bool) (l : list A),
Permutation
(filter f l ++ antifilter f l) l.
Proof.
intros f l.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply perm_nil.
(* Case : l = x :: l' *)
simpl.
case (f x).
(* Case : f x = true *)
simpl.
apply perm_skip.
apply H_l'.
(* Case : f x = false *)
simpl.
apply Permutation_sym.
apply Permutation_cons_app.
apply Permutation_sym.
apply H_l'.
Qed.
End Preliminaries.
(*////////////////////////////////////////////////////*)
(** Algorithm *)
(*////////////////////////////////////////////////////*)
(* Definition : Quick sort *)
Function qsort (l : list nat) {measure length} : list nat :=
match l with
| nil => nil
| n :: l' => let lts := antifilter (leb n) l' in
let ges := filter (leb n) l' in
(qsort lts) ++ n :: (qsort ges)
end.
Proof.
(* Proof : length (filter (beb n) l') < length l *)
intros l n l' H_l.
simpl.
apply le_lt_trans with (length l').
(* Proof : length (filter (leb n) l') <= length l' *)
assert (filter (leb n) l' = l' \/
length (filter (leb n) l') < length l')
as H_len.
(* Proof of the assertion *)
apply sublist_length.
apply filter_sublist.
destruct H_len as [H_eq | H_lt].
(* Case : filter (leb n) l' = l' *)
rewrite H_eq.
reflexivity.
(* Case : length (filter (leb n) l') < length l' *)
apply lt_le_weak.
apply H_lt.
(* Proof : length l' < S (length l') *)
apply lt_n_Sn.
(* Proof : length (antifilter (leb n) l') < length l *)
intros l n l' H_l.
simpl.
apply le_lt_trans with (length l').
(* Proof : length (antifilter (leb n) l') <=
length l' *)
assert (antifilter (leb n) l' = l' \/
length (antifilter (leb n) l') < length l')
as H_len.
(* Proof of the assertion *)
apply sublist_length.
apply antifilter_sublist.
destruct H_len as [H_eq | H_lt].
(* Case : antifilter (leb n) l' = l' *)
rewrite H_eq.
reflexivity.
(* Case : length (antifilter (leb n) l' <
length l' *)
apply lt_le_weak.
apply H_lt.
(* Proof : length l' < S (length l') *)
apply lt_n_Sn.
Defined.
(*////////////////////////////////////////////////////*)
(** Validation 1 : Sorted *)
(*////////////////////////////////////////////////////*)
(* Compatibility of HdRel with appending *)
Lemma HdRel_app : forall (n : nat) (l1 l2 : list nat),
HdRel le n l1 -> HdRel le n l2 ->
HdRel le n (l1 ++ l2).
Proof.
intro n.
induction l1 as [| m l1' H_l1'].
(* Case : l1 = nil *)
intros l2 H_1 H_2.
simpl.
apply H_2.
(* Case : l1 = m :: l1' *)
intros l2 H_1 H_2.
simpl. Print HdRel_cons.
apply HdRel_cons.
inversion H_1 as [| tmp1 tmp2 H_le (tmp3, tmp4)].
clear tmp1 tmp2 tmp3 tmp4.
apply H_le.
Qed.
(* Compatibility of sorted property with appending *)
Lemma Sorted_app : forall (l1 l2 : list nat),
Sorted le l1 -> Sorted le l2 ->
(forall n1 n2 : nat,
In n1 l1 -> In n2 l2 -> n1 <= n2) ->
Sorted le (l1 ++ l2).
Proof.
induction l1 as [| m l1' H_l1'].
(* Case : l1 = nil *)
intros l2 H_1 H_2 H_le.
simpl.
apply H_2.
(* Case : l1 = m :: l1' *)
intros l2 H_1 H_2 H_le.
simpl.
inversion H_1 as [| tmp1 tmp2 H_sort H_hr (tmp3, tmp4)].
clear tmp1 tmp2 tmp3 tmp4.
apply Sorted_cons.
(* Proof : Sorted le (l1' ++ l2) *)
apply H_l1'.
(* Proof : Sorted le l1' *)
apply H_sort.
(* Proof : Sorted le l2 *)
apply H_2.
(* Proof : In n1 l1' -> In n2 l2 -> n1 <= n2 *)
intros n1 n2 H_n1 H_n2.
apply H_le.
(* Proof : In n1 (m :: l1') *)
unfold In.
right.
apply H_n1.
(* Proof : In n2 l2 *)
apply H_n2.
(* Proof : HdRel m (l1' ++ l2) *)
apply HdRel_app.
(* Proof : HdRel le m l1' *)
apply H_hr.
(* Proof : HdRel le m l2 *)
induction l2 as [| p l2' H_l2'].
(* Case : l2 = nil *)
apply HdRel_nil.
(* Case : l2 = p :: l2' *)
apply HdRel_cons.
apply (H_le m p).
(* Proof : In m (m :: l1') *)
unfold In.
left.
reflexivity.
(* Proof : In m (m :: l1') *)
unfold In.
left.
reflexivity.
Qed.
(* Compatibility of In with qsort *)
Lemma qsort_in : forall (l : list nat) (n : nat),
In n l <-> In n (qsort l).
Proof.
intros l n.
split.
(* Proof : Direction -> *)
intro H.
functional induction (qsort l)
as [| _ m l' _ H' H'' H_lt H_ge].
(* Case : l = nil *)
apply H.
(* Case : l = m :: l' *)
apply in_app_iff.
unfold In in H.
fold (In n l') in H.
destruct H as [H | H].
(* Case : m = n *)
right.
rewrite H.
unfold In.
left.
reflexivity.
(* Case : In n l' *)
apply (filter_or nat (leb m) l' n) in H.
destruct H as [H | H].
(* Case : In n (filter (leb m) l') *)
right.
unfold In.
right.
apply H_ge.
apply H.
(* Case : In n (antifilter (leb m) l') *)
left.
apply H_lt.
apply H.
(* Proof : Direction <- *)
intro H.
functional induction (qsort l)
as [| _ m l' _ H' H'' H_lt H_ge].
(* Case : l = nil *)
apply H.
apply in_app_iff in H.
unfold In.
fold (In n l').
destruct H as [H | H].
(* Case : In n (qsort (antifilter (leb m) l')) *)
right.
apply (filter_or nat (leb m) l' n).
right.
apply H_lt.
apply H.
(* Case : In n (m :: qsort (filter (leb m) l')) *)
unfold In in H.
fold (In n (qsort (filter (leb m) l'))) in H.
destruct H as [H | H].
(* Case : m = n *)
left.
apply H.
(* Case : In n (qsort (filter (leb m) l')) *)
right.
apply (filter_or nat (leb m) l' n).
left.
apply H_ge.
apply H.
Qed.
(* Validation 1 : The outputs of qsort are sorted. *)
Theorem qsort_Sorted : forall l : list nat, Sorted le (qsort l).
Proof.
intro l.
functional induction (qsort l) as [| _ n l' _ H H' H_lt H_ge].
(* Case : l = nil *)
apply Sorted_nil.
(* Case : l = n :: l' *)
apply Sorted_app.
(* Proof : Sorted le (qsort (antifilter (leb n) l')) *)
apply H_lt.
(* Proof : Sorted le (n :: qsort (filter (leb n) l')) *)
apply Sorted_cons.
(* Proof : Sorted le (qsort (filter (leb n) l')) *)
apply H_ge.
(* Proof : HdRel le n (qsort (filter (leb n) l')) *)
remember (qsort (filter (leb n) l')) as ms.
induction ms as [| m l'' H_l''].
(* Case : ms = nil *)
apply HdRel_nil.
(* Case : ms = m :: l'' *)
apply HdRel_cons.
assert (In m (filter (leb n) l')) as H_m.
(* Proof of the assertion *)
apply qsort_in.
rewrite <- Heqms.
unfold In.
left.
reflexivity.
apply filter_true in H_m.
apply leb_complete.
apply H_m.
(* Proof : Properties of lts and ges. *)
intros n1 n2 H_n1 H_n2.
apply lt_le_weak.
apply lt_le_trans with n.
(* Proof : n1 < n *)
apply leb_complete_conv.
apply (antifilter_false nat (leb n) l').
apply qsort_in.
apply H_n1.
(* Proof : n <= n2 *)
destruct H_n2 as [H_n2 | H_n2].
(* Case : n = n2 *)
rewrite H_n2.
apply le_refl.
(* Case : In n2 (qsort (filter (leb n) l')) *)
apply leb_complete.
apply (filter_true nat (leb n) l').
apply qsort_in.
apply H_n2.
Qed.
(*////////////////////////////////////////////////////*)
(** Validation 2 : Permutation *)
(*////////////////////////////////////////////////////*)
(* Validation 2 : The outputs of qsort are *)
(* the permutations of the inputs. *)
Theorem qsort_Permutation : forall l : list nat,
Permutation (qsort l) l.
Proof.
intro l.
functional induction (qsort l) as [| _ n l' _ H H' H_lt H_ge].
(* Case : l = nil *)
apply perm_nil.
(* Case : l = n :: l' *)
symmetry.
apply Permutation_cons_app.
apply perm_trans with (antifilter (leb n) l' ++
filter (leb n) l').
(* Proof : Permutation l'(antifilter (leb n) l' ++
filter (leb n) l') *)
rewrite Permutation_app_comm.
apply Permutation_sym.
apply filter_Permutation.
(* Proof : Permutation (antifilter (leb n) l' ++
filter (leb n) l')
(qsort (antifilter (leb n) l') ++
qsort (filter (leb n) l')) *)
apply Permutation_app.
(* Proof : Permutation
(antifilter (leb n) l')
(qsort (antifilter (leb n) l')) *)
apply Permutation_sym.
apply H_lt.
(* Proof : Permutation
(filter (leb n) l')
(qsort (filter (leb n) l')) *)
apply Permutation_sym.
apply H_ge.
Qed.
End QuickSort.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment