src/sorted.bend

bend-lawful-stdlib@0.1.0.0 · 231 lines · 16 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/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
18def from(~A: Data, ~o: C.Ord<A>, 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
26def Sorted(~A: Data, ~o: C.Ord<A>, 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.
35def insert.go(-A: Data, -o: C.Ord<A>, 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
42def insert(~A: Data, ~o: C.Ord<A>, +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
49def sort(~A: Data, ~o: C.Ord<A>, 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
59law insert_from.go:
60  for -A: Data
61  for -o: C.Ord<A>
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
73def 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
81law insert_from:
82  for ~A: Data
83  for ~o: C.Ord<A>
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
89def 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
97law insert_sorted.go:
98  for -A: Data
99  for -o: C.Ord<A>
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
109def 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
116law insert_sorted:
117  for ~A: Data
118  for ~o: C.Ord<A>
119  for +x: A
120  for xs: List<&2, A>
121  Sorted(~A, ~o, xs) -> Sorted(~A, ~o, insert(~A, ~o, x, xs))
122
123def 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.
132law sort_sorted:
133  for ~A: Data
134  for ~o: C.Ord<A>
135  for xs: List<&2, A>
136  Sorted(~A, ~o, sort(~A, ~o, xs))
137
138def 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
145def bump(b: Bool, n: Nat) -> Nat:
146  match b:
147    case True{}:
148      1n+n
149    case False{}:
150      n
151
152law 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
158def 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
170def 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
177law insert_count.go:
178  for ~A: Data
179  for ~eq: A -> A -> Bool
180  for -o: C.Ord<A>
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
190def 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
198law insert_count:
199  for ~A: Data
200  for ~o: C.Ord<A>
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
207def 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.
216law sort_count:
217  for ~A: Data
218  for ~o: C.Ord<A>
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
224def 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      {==}