1 import Base
2 import ./class.bend as C
3
4 # sorted.bend: insertion sort over any C.Ord, with laws that its output is
5 # sorted and keeps every element's count.
6 #
7 # import ./sorted.bend as Sorted
8 # Sorted.sort(~Nat, ~Nat.ord(), xs)
9 #
10 # The order's decision returns a proof of the side that holds. insert
11 # branches on that proof, and the sortedness proof receives the same
12 # proof in each branch, so it needs no transitivity. The laws are proven
13 # once, with the order opaque.
14 #
15 # Insertion sort is O(n^2). Base's List.sort is a merge sort with no laws.
16
17 # every element is at least lo, and the list ascends
18 def from(~A: Data, ~o: C.Ord, lo: A, xs: List<&2, A>) -> Type:
19 match xs:
20 case Nil{}:
21 Unit
22 case h <> t:
23 (C.Ord.R(A, o, lo, h) & from(~A, ~o, h, t))
24
25 # the list ascends
26 def Sorted(~A: Data, ~o: C.Ord, xs: List<&2, A>) -> Type:
27 match xs:
28 case Nil{}:
29 Unit
30 case h <> t:
31 from(~A, ~o, h, t)
32
33 # insert's step after comparing x with h. The recursive insert is passed
34 # as a thunk so that the x-first branch does not run it.
35 def insert.go(-A: Data, -o: C.Ord, x: A, h: A, t: List<&2, A>, rec: Unit -> List<&2, A>, c: Or(C.Ord.R(A, o, x, h), C.Ord.R(A, o, h, x))) -> List<&2, A>:
36 match c:
37 case Inl{e}:
38 x <> h <> t
39 case Inr{e}:
40 h <> rec(Unit{})
41
42 def insert(~A: Data, ~o: C.Ord, +x: A, xs: List<&2, A>) -> List<&2, A>:
43 match xs:
44 case Nil{}:
45 [x]
46 case +h <> +t:
47 insert.go(A, o, x, h, t, u => insert(~A, ~o, x, t), C.Ord.dec(A, o, x, h))
48
49 def sort(~A: Data, ~o: C.Ord, xs: List<&2, A>) -> List<&2, A>:
50 match xs:
51 case Nil{}:
52 Nil{}
53 case h <> t:
54 insert(~A, ~o, h, sort(~A, ~o, t))
55
56 # A match does not refine hypotheses already in scope, so these laws take
57 # their hypotheses after the match, as functions returned by each arm.
58
59 law insert_from.go:
60 for -A: Data
61 for -o: C.Ord
62 for -lo: A
63 for -x: A
64 for -h: A
65 for -t: List<&2, A>
66 for -rec: Unit -> List<&2, A>
67 for s: from(~A, ~o, lo, h <> t)
68 for lx: C.Ord.R(A, o, lo, x)
69 for ih: from(~A, ~o, h, t) -> C.Ord.R(A, o, h, x) -> from(~A, ~o, h, rec(Unit{}))
70 for c: Or(C.Ord.R(A, o, x, h), C.Ord.R(A, o, h, x))
71 from(~A, ~o, lo, insert.go(A, o, x, h, t, rec, c))
72
73 def insert_from.go(A, o, lo, x, h, t, rec, s, lx, ih, c):
74 (lh, st) = s
75 match c:
76 case Inl{e}:
77 (lx, e, st)
78 case Inr{e}:
79 (lh, ih(st, e))
80
81 law insert_from:
82 for ~A: Data
83 for ~o: C.Ord
84 for +x: A
85 for xs: List<&2, A>
86 for -lo: A
87 from(~A, ~o, lo, xs) -> C.Ord.R(A, o, lo, x) -> from(~A, ~o, lo, insert(~A, ~o, x, xs))
88
89 def insert_from(A, o, x, xs, lo):
90 match xs:
91 case Nil{}:
92 s => lx => (lx, Unit{})
93 case +h <> +t:
94 s => lx => insert_from.go(A, o, lo, x, h, t, u => insert(~A, ~o, x, t), s, lx,
95 insert_from(~A, ~o, x, t, h), C.Ord.dec(A, o, x, h))
96
97 law insert_sorted.go:
98 for -A: Data
99 for -o: C.Ord
100 for -x: A
101 for -h: A
102 for -t: List<&2, A>
103 for -rec: Unit -> List<&2, A>
104 for s: from(~A, ~o, h, t)
105 for ih: from(~A, ~o, h, t) -> C.Ord.R(A, o, h, x) -> from(~A, ~o, h, rec(Unit{}))
106 for c: Or(C.Ord.R(A, o, x, h), C.Ord.R(A, o, h, x))
107 Sorted(~A, ~o, insert.go(A, o, x, h, t, rec, c))
108
109 def insert_sorted.go(A, o, x, h, t, rec, s, ih, c):
110 match c:
111 case Inl{e}:
112 (e, s)
113 case Inr{e}:
114 ih(s, e)
115
116 law insert_sorted:
117 for ~A: Data
118 for ~o: C.Ord
119 for +x: A
120 for xs: List<&2, A>
121 Sorted(~A, ~o, xs) -> Sorted(~A, ~o, insert(~A, ~o, x, xs))
122
123 def insert_sorted(A, o, x, xs):
124 match xs:
125 case Nil{}:
126 s => Unit{}
127 case +h <> +t:
128 s => insert_sorted.go(A, o, x, h, t, u => insert(~A, ~o, x, t), s,
129 insert_from(~A, ~o, x, t, h), C.Ord.dec(A, o, x, h))
130
131 # sort's output is sorted.
132 law sort_sorted:
133 for ~A: Data
134 for ~o: C.Ord
135 for xs: List<&2, A>
136 Sorted(~A, ~o, sort(~A, ~o, xs))
137
138 def sort_sorted(A, o, xs):
139 match xs:
140 case Nil{}:
141 Unit{}
142 case h <> +t:
143 insert_sorted(~A, ~o, h, sort(~A, ~o, t))(sort_sorted(~A, ~o, t))
144
145 def bump(b: Bool, n: Nat) -> Nat:
146 match b:
147 case True{}:
148 1n+n
149 case False{}:
150 n
151
152 law bump_swap:
153 for a: Bool
154 for b: Bool
155 for -n: Nat
156 {bump(a, bump(b, n)) == bump(b, bump(a, n)) : Nat}
157
158 def bump_swap(a, b, n):
159 match a b:
160 case True{} True{}:
161 {==}
162 case True{} False{}:
163 {==}
164 case False{} True{}:
165 {==}
166 case False{} False{}:
167 {==}
168
169 # how many elements of xs ~eq calls equal to y
170 def count(~A: Data, ~eq: A -> A -> Bool, +y: A, xs: List<&2, A>) -> Nat:
171 match xs:
172 case Nil{}:
173 0n
174 case h <> t:
175 bump(eq(y, h), count(~A, ~eq, y, t))
176
177 law insert_count.go:
178 for ~A: Data
179 for ~eq: A -> A -> Bool
180 for -o: C.Ord
181 for +y: A
182 for +x: A
183 for +h: A
184 for +t: List<&2, A>
185 for -rec: Unit -> List<&2, A>
186 for ih: {bump(eq(y, x), count(~A, ~eq, y, t)) == count(~A, ~eq, y, rec(Unit{})) : Nat}
187 for c: Or(C.Ord.R(A, o, x, h), C.Ord.R(A, o, h, x))
188 {bump(eq(y, x), count(~A, ~eq, y, h <> t)) == count(~A, ~eq, y, insert.go(A, o, x, h, t, rec, c)) : Nat}
189
190 def insert_count.go(A, eq, o, y, x, h, t, rec, ih, c):
191 match c:
192 case Inl{e}:
193 {==}
194 case Inr{e}:
195 %ih : {bump(eq(y, x), bump(eq(y, h), count(~A, ~eq, y, t))) == bump(eq(y, h), _) : Nat}
196 bump_swap(eq(y, x), eq(y, h), count(~A, ~eq, y, t))
197
198 law insert_count:
199 for ~A: Data
200 for ~o: C.Ord
201 for ~eq: A -> A -> Bool
202 for +y: A
203 for +x: A
204 for xs: List<&2, A>
205 {bump(eq(y, x), count(~A, ~eq, y, xs)) == count(~A, ~eq, y, insert(~A, ~o, x, xs)) : Nat}
206
207 def insert_count(A, o, eq, y, x, xs):
208 match xs:
209 case Nil{}:
210 {==}
211 case +h <> +t:
212 insert_count.go(~A, ~eq, o, y, x, h, t, u => insert(~A, ~o, x, t),
213 insert_count(~A, ~o, ~eq, y, x, t), C.Ord.dec(A, o, x, h))
214
215 # sort keeps every element's count.
216 law sort_count:
217 for ~A: Data
218 for ~o: C.Ord
219 for ~eq: A -> A -> Bool
220 for +y: A
221 for xs: List<&2, A>
222 {count(~A, ~eq, y, xs) == count(~A, ~eq, y, sort(~A, ~o, xs)) : Nat}
223
224 def sort_count(A, o, eq, y, xs):
225 match xs:
226 case Nil{}:
227 {==}
228 case +h <> +t:
229 %insert_count(~A, ~o, ~eq, y, h, sort(~A, ~o, t)) : {count(~A, ~eq, y, h <> t) == _ : Nat}
230 %sort_count(~A, ~o, ~eq, y, t) : {count(~A, ~eq, y, h <> t) == bump(eq(y, h), _) : Nat}
231 {==}