/
sort.lean
50 lines (38 loc) · 1.45 KB
/
sort.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Mario Carneiro
-/
import data.list.sort
import data.multiset.basic
import data.string.basic
/-!
# Construct a sorted list from a multiset.
-/
namespace multiset
open list
variables {α : Type*}
section sort
variables (r : α → α → Prop) [decidable_rel r]
[is_trans α r] [is_antisymm α r] [is_total α r]
/-- `sort s` constructs a sorted list from the multiset `s`.
(Uses merge sort algorithm.) -/
def sort (s : multiset α) : list α :=
quot.lift_on s (merge_sort r) $ λ a b h,
eq_of_sorted_of_perm
((perm_merge_sort _ _).trans $ h.trans (perm_merge_sort _ _).symm)
(sorted_merge_sort r _)
(sorted_merge_sort r _)
@[simp] theorem coe_sort (l : list α) : sort r l = merge_sort r l := rfl
@[simp] theorem sort_sorted (s : multiset α) : sorted r (sort r s) :=
quot.induction_on s $ λ l, sorted_merge_sort r _
@[simp] theorem sort_eq (s : multiset α) : ↑(sort r s) = s :=
quot.induction_on s $ λ l, quot.sound $ perm_merge_sort _ _
@[simp] theorem mem_sort {s : multiset α} {a : α} : a ∈ sort r s ↔ a ∈ s :=
by rw [← mem_coe, sort_eq]
@[simp] theorem length_sort {s : multiset α} : (sort r s).length = s.card :=
quot.induction_on s $ length_merge_sort _
end sort
instance [has_repr α] : has_repr (multiset α) :=
⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩
end multiset