sorting.v 9.73 KB
Newer Older
1
2
3
4
(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
standard library, but without using the module system. *)
From Coq Require Export Sorted.
From stdpp Require Export orders list.
5
Set Default Proof Using "Type".
6
7
8
9
10
11
12
13
14
15

Section merge_sort.
  Context {A} (R : relation A) `{ x y, Decision (R x y)}.

  Fixpoint list_merge (l1 : list A) : list A  list A :=
    fix list_merge_aux l2 :=
    match l1, l2 with
    | [], _ => l2
    | _, [] => l1
    | x1 :: l1, x2 :: l2 =>
16
       if decide (R x1 x2) then x1 :: list_merge l1 (x2 :: l2)
17
18
       else x2 :: list_merge_aux l2
    end.
19
  Global Arguments list_merge !_ !_ / : assert.
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

  Local Notation stack := (list (option (list A))).
  Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack :=
    match st with
    | [] => [Some l]
    | None :: st => Some l :: st
    | Some l' :: st => None :: merge_list_to_stack st (list_merge l' l)
    end.
  Fixpoint merge_stack (st : stack) : list A :=
    match st with
    | [] => []
    | None :: st => merge_stack st
    | Some l :: st => list_merge l (merge_stack st)
    end.
  Fixpoint merge_sort_aux (st : stack) (l : list A) : list A :=
    match l with
    | [] => merge_stack st
    | x :: l => merge_sort_aux (merge_list_to_stack st [x]) l
    end.
  Definition merge_sort : list A  list A := merge_sort_aux [].
End merge_sort.

Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
45
46
(** Helper definition for [Sorted_reverse] below *)
Inductive TlRel {A} (R : relation A) (a : A) : list A  Prop :=
  | TlRel_nil : TlRel R a []
  | TlRel_cons b l : R b a  TlRel R a (l ++ [b]).

47
48
49
50
(** ** Properties of the [Sorted] and [StronglySorted] predicate *)
Section sorted.
  Context {A} (R : relation A).

51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
  Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
    StronglySorted R (l1 ++ l2)  x1  l1  x2  l2  R x1 x2.
  Proof.
    induction l1 as [|x1' l1 IH]; simpl; [by rewrite elem_of_nil|].
    intros [? Hall]%StronglySorted_inv [->|?]%elem_of_cons ?; [|by auto].
    rewrite Forall_app, !Forall_forall in Hall. naive_solver.
  Qed.
  Lemma StronglySorted_app_inv_l l1 l2 :
    StronglySorted R (l1 ++ l2)  StronglySorted R l1.
  Proof.
    induction l1 as [|x1' l1 IH]; simpl;
      [|inversion_clear 1]; decompose_Forall; constructor; auto.
  Qed.
  Lemma StronglySorted_app_inv_r l1 l2 :
    StronglySorted R (l1 ++ l2)  StronglySorted R l2.
  Proof.
    induction l1 as [|x1' l1 IH]; simpl;
      [|inversion_clear 1]; decompose_Forall; auto.
  Qed.

71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
  Lemma Sorted_StronglySorted `{!Transitive R} l :
    Sorted R l  StronglySorted R l.
  Proof. by apply Sorted.Sorted_StronglySorted. Qed.
  Lemma StronglySorted_unique `{!AntiSymm (=) R} l1 l2 :
    StronglySorted R l1  StronglySorted R l2  l1  l2  l1 = l2.
  Proof.
    intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
    { symmetry. by apply Permutation_nil. }
    destruct Hl2 as [|x2 l2 ? Hx2].
    { by apply Permutation_nil in E. }
    assert (x1 = x2); subst.
    { rewrite Forall_forall in Hx1, Hx2.
      assert (x2  x1 :: l1) as Hx2' by (by rewrite E; left).
      assert (x1  x2 :: l2) as Hx1' by (by rewrite <-E; left).
      inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
86
    f_equal. by apply IH, (inj (x2 ::.)).
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
  Qed.
  Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
    Sorted R l1  Sorted R l2  l1  l2  l1 = l2.
  Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.

  Global Instance HdRel_dec x `{ y, Decision (R x y)} l :
    Decision (HdRel R x l).
  Proof.
   refine
    match l with
    | [] => left _
    | y :: l => cast_if (decide (R x y))
    end; abstract first [by constructor | by inversion 1].
  Defined.
  Global Instance Sorted_dec `{ x y, Decision (R x y)} :  l,
    Decision (Sorted R l).
  Proof.
   refine
    (fix go l :=
    match l return Decision (Sorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
    end); clear go; abstract first [by constructor | by inversion 1].
  Defined.
  Global Instance StronglySorted_dec `{ x y, Decision (R x y)} :  l,
    Decision (StronglySorted R l).
  Proof.
   refine
    (fix go l :=
    match l return Decision (StronglySorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
    end); clear go; abstract first [by constructor | by inversion 1].
  Defined.

122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
  Section fmap.
    Context {B} (f : A  B).
    Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
      ( y, R1 x y  R2 (f x) (f y))  HdRel R1 x l  HdRel R2 (f x) (f <$> l).
    Proof. destruct 2; constructor; auto. Qed.
    Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
      ( x y, R1 x y  R2 (f x) (f y))  Sorted R1 l  Sorted R2 (f <$> l).
    Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
    Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
      ( x y, R1 x y  R2 (f x) (f y)) 
      StronglySorted R1 l  StronglySorted R2 (f <$> l).
    Proof.
      induction 2; csimpl; constructor;
        rewrite ?Forall_fmap; eauto using Forall_impl.
    Qed.
  End fmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
140
141
142
143
144
145
146
147
148
149
150

  Lemma HdRel_reverse l x : HdRel R x l  TlRel (flip R) x (reverse l).
  Proof. destruct 1; rewrite ?reverse_cons; by constructor. Qed.

  Lemma Sorted_snoc l x : Sorted R l  TlRel R x l  Sorted R (l ++ [x]).
  Proof.
    induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl.
    { repeat constructor. }
    constructor. apply IH.
    - inversion Htl as [|? [|??]]; simplify_list_eq; by constructor.
    - destruct Hhd; constructor; [|done].
      inversion Htl as [|? [|??]]; by try discriminate_list.
  Qed.
151
152
End sorted.

Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
157
158
159
Lemma Sorted_reverse {A} (R : relation A) l :
  Sorted R l  Sorted (flip R) (reverse l).
Proof.
  induction 1; rewrite ?reverse_nil, ?reverse_cons;
    auto using Sorted_snoc, HdRel_reverse.
Qed.

160
161
(** ** Correctness of merge sort *)
Section merge_sort_correct.
162
  Context  {A} (R : relation A) `{ x y, Decision (R x y)}.
163

164
165
166
167
  Lemma list_merge_nil_l l2 : list_merge R [] l2 = l2.
  Proof. by destruct l2. Qed.
  Lemma list_merge_nil_r l1 : list_merge R l1 [] = l1.
  Proof. by destruct l1. Qed.
168
169
170
171
172
173
174
175
176
177
178
  Lemma list_merge_cons x1 x2 l1 l2 :
    list_merge R (x1 :: l1) (x2 :: l2) =
      if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
      else x2 :: list_merge R (x1 :: l1) l2.
  Proof. done. Qed.
  Lemma HdRel_list_merge x l1 l2 :
    HdRel R x l1  HdRel R x l2  HdRel R x (list_merge R l1 l2).
  Proof.
    destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2];
      rewrite ?list_merge_cons; simpl; repeat case_decide; auto.
  Qed.
179
  Lemma Sorted_list_merge `{!Total R} l1 l2 :
180
181
182
    Sorted R l1  Sorted R l2  Sorted R (list_merge R l1 l2).
  Proof.
    intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
183
      (* FIXME: trailing [?] works around Coq bug #12944. *)
184
      induction 1 as [|x2 l2 IH2 ?]; rewrite ?list_merge_cons; simpl;
185
      repeat case_decide;
186
187
      repeat match goal with H : ¬R _ _ |- _ => apply total_not in H end;
      constructor; eauto using HdRel_list_merge, HdRel_cons.
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
  Qed.
  Lemma merge_Permutation l1 l2 : list_merge R l1 l2  l1 ++ l2.
  Proof.
    revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
      induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
      repeat case_decide; auto.
    - by rewrite (right_id_L [] (++)).
    - by rewrite IH2, Permutation_middle.
  Qed.

  Local Notation stack := (list (option (list A))).
  Inductive merge_stack_Sorted : stack  Prop :=
    | merge_stack_Sorted_nil : merge_stack_Sorted []
    | merge_stack_Sorted_cons_None st :
       merge_stack_Sorted st  merge_stack_Sorted (None :: st)
    | merge_stack_Sorted_cons_Some l st :
       Sorted R l  merge_stack_Sorted st  merge_stack_Sorted (Some l :: st).
  Fixpoint merge_stack_flatten (st : stack) : list A :=
    match st with
    | [] => []
    | None :: st => merge_stack_flatten st
    | Some l :: st => l ++ merge_stack_flatten st
    end.

212
  Lemma Sorted_merge_list_to_stack `{!Total R} st l :
213
214
215
216
217
218
219
220
221
222
223
224
225
    merge_stack_Sorted st  Sorted R l 
    merge_stack_Sorted (merge_list_to_stack R st l).
  Proof.
    intros Hst. revert l.
    induction Hst; repeat constructor; naive_solver auto using Sorted_list_merge.
  Qed.
  Lemma merge_list_to_stack_Permutation st l :
    merge_stack_flatten (merge_list_to_stack R st l) 
      l ++ merge_stack_flatten st.
  Proof.
    revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
    by rewrite IH, merge_Permutation, (assoc_L _), (comm (++) l).
  Qed.
226
  Lemma Sorted_merge_stack `{!Total R} st :
227
228
229
230
231
232
233
    merge_stack_Sorted st  Sorted R (merge_stack R st).
  Proof. induction 1; simpl; auto using Sorted_list_merge. Qed.
  Lemma merge_stack_Permutation st : merge_stack R st  merge_stack_flatten st.
  Proof.
    induction st as [|[] ? IH]; intros; simpl; auto.
    by rewrite merge_Permutation, IH.
  Qed.
234
  Lemma Sorted_merge_sort_aux `{!Total R} st l :
235
236
237
238
239
240
241
242
243
244
245
246
247
    merge_stack_Sorted st  Sorted R (merge_sort_aux R st l).
  Proof.
    revert st. induction l; simpl;
      auto using Sorted_merge_stack, Sorted_merge_list_to_stack.
  Qed.
  Lemma merge_sort_aux_Permutation st l :
    merge_sort_aux R st l  merge_stack_flatten st ++ l.
  Proof.
    revert st. induction l as [|?? IH]; simpl; intros.
    - by rewrite (right_id_L [] (++)), merge_stack_Permutation.
    - rewrite IH, merge_list_to_stack_Permutation; simpl.
      by rewrite Permutation_middle.
  Qed.
248
  Lemma Sorted_merge_sort `{!Total R} l : Sorted R (merge_sort R l).
249
250
251
  Proof. apply Sorted_merge_sort_aux. by constructor. Qed.
  Lemma merge_sort_Permutation l : merge_sort R l  l.
  Proof. unfold merge_sort. by rewrite merge_sort_aux_Permutation. Qed.
252
  Lemma StronglySorted_merge_sort `{!Transitive R, !Total R} l :
253
254
255
    StronglySorted R (merge_sort R l).
  Proof. auto using Sorted_StronglySorted, Sorted_merge_sort. Qed.
End merge_sort_correct.