sort.bend
bend-mathlib@0.7.4.0 · 246 lines · 0 definitions
1# bend-mathlib/sort.bend: insertion and merge sort proved sorted over perm.bend's value defs (generic ~le).
2import Base
3import bend-mathlib@0.7.4.0/nat.bend as MNat
4import bend-mathlib@0.7.4.0/list.bend as MList
5import bend-mathlib@0.7.4.0/perm.bend as MPerm
6
7def internal_sorted_single(~A: Data, ~le: A -> A -> Bool, +x: A) -> MList.sorted_by(~A, ~le, x <> Nil{}):
8 {==}
9
10def internal_sorted_cons_cons_intro(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, hxy: {le(x, y) == True{} : Bool}, hyt: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, x <> y <> t):
11 %MList.internal_sorted_cons_true(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), hxy) : {_ == True{} : Bool}
12 hyt
13
14def internal_sorted_le_step(~A: Data, ~le: A -> A -> Bool, -x: A, +y: A, +t: List<&2, A>, b: Bool, e: {le(x, y) == b : Bool}, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> {le(x, y) == True{} : Bool}:
15 match b:
16 case True{}:
17 e
18 case False{}:
19 Empty.absurd({le(x, y) == True{} : Bool}, MNat.internal_false_ne_true(Equal.trans(Bool, False{}, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_false(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)))
20
21def internal_sorted_tail_step(~A: Data, ~le: A -> A -> Bool, -x: A, +y: A, +t: List<&2, A>, b: Bool, e: {le(x, y) == b : Bool}, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> MList.sorted_by(~A, ~le, y <> t):
22 match b:
23 case True{}:
24 Equal.trans(Bool, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, y <> t, t)), List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_true(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)
25 case False{}:
26 Empty.absurd(MList.sorted_by(~A, ~le, y <> t), MNat.internal_false_ne_true(Equal.trans(Bool, False{}, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_false(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)))
27
28def internal_sorted_cons_cons_elim_le(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> {le(x, y) == True{} : Bool}:
29 internal_sorted_le_step(~A, ~le, x, y, t, le(x, y), {==}, h)
30
31def internal_sorted_cons_cons_elim_tail(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> MList.sorted_by(~A, ~le, y <> t):
32 internal_sorted_tail_step(~A, ~le, x, y, t, le(x, y), {==}, h)
33
34def internal_sorted_tail(~A: Data, ~le: A -> A -> Bool, +x: A, +xs: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> xs)) -> MList.sorted_by(~A, ~le, xs):
35 match xs:
36 case Nil{}:
37 {==}
38 case +y <> +t:
39 internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h)
40
41def internal_le_flip_nat(x: Nat, y: Nat, e: {Nat.is_le(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
42 match x y:
43 case 0n 0n:
44 Empty.absurd({True{} == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, e)))
45 case 0n 1n+q:
46 Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, e)))
47 case 1n+p 0n:
48 {==}
49 case 1n+p 1n+q:
50 internal_le_flip_nat(p, q, e)
51
52def internal_le_trans_nat(x: Nat, y: Nat, z: Nat, xy: {Nat.is_le(x, y) == True{} : Bool}, yz: {Nat.is_le(y, z) == True{} : Bool}) -> {Nat.is_le(x, z) == True{} : Bool}:
53 MNat.le_trans(x, y, z, xy, yz)
54
55def internal_cons_ins_step(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +y: A, +x: A, +z: A, +u: List<&2, A>, e: {le(x, z) == b : Bool}, hyx: {le(y, x) == True{} : Bool}, +h: MList.sorted_by(~A, ~le, y <> z <> u), k: {le(z, x) == True{} : Bool} -> MList.sorted_by(~A, ~le, z <> MPerm.insert_by(~A, ~le, x, u))) -> MList.sorted_by(~A, ~le, y <> Bool.pick(List<&2, A>, b, x <> z <> u, z <> MPerm.insert_by(~A, ~le, x, u))):
56 match b:
57 case True{}:
58 internal_sorted_cons_cons_intro(~A, ~le, y, x, z <> u, hyx, internal_sorted_cons_cons_intro(~A, ~le, x, z, u, e, internal_sorted_cons_cons_elim_tail(~A, ~le, y, z, u, h)))
59 case False{}:
60 internal_sorted_cons_cons_intro(~A, ~le, y, z, MPerm.insert_by(~A, ~le, x, u), internal_sorted_cons_cons_elim_le(~A, ~le, y, z, u, h), k(le_total(x, z, e)))
61
62def internal_sorted_cons_ins(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +t: List<&2, A>, +y: A, +x: A, hyx: {le(y, x) == True{} : Bool}, +h: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, y <> MPerm.insert_by(~A, ~le, x, t)):
63 match t:
64 case Nil{}:
65 internal_sorted_cons_cons_intro(~A, ~le, y, x, Nil{}, hyx, internal_sorted_single(~A, ~le, x))
66 case +z <> +u:
67 internal_cons_ins_step(~A, ~le, ~le_total, le(x, z), y, x, z, u, {==}, hyx, h, hzx => internal_sorted_cons_ins(~A, ~le, ~le_total, u, z, x, hzx, internal_sorted_cons_cons_elim_tail(~A, ~le, y, z, u, h)))
68
69def internal_insert_step(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +x: A, +y: A, +t: List<&2, A>, e: {le(x, y) == b : Bool}, +h: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, Bool.pick(List<&2, A>, b, x <> y <> t, y <> MPerm.insert_by(~A, ~le, x, t))):
70 match b:
71 case True{}:
72 internal_sorted_cons_cons_intro(~A, ~le, x, y, t, e, h)
73 case False{}:
74 internal_sorted_cons_ins(~A, ~le, ~le_total, t, y, x, le_total(x, y, e), h)
75
76# Inserting into a sorted list keeps it sorted, for a total comparator.
77def insert_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +x: A, +xs: List<&2, A>, +h: MList.sorted_by(~A, ~le, xs)) -> MList.sorted_by(~A, ~le, MPerm.insert_by(~A, ~le, x, xs)):
78 match xs:
79 case Nil{}:
80 internal_sorted_single(~A, ~le, x)
81 case +y <> t:
82 internal_insert_step(~A, ~le, ~le_total, le(x, y), x, y, t, {==}, h)
83
84# Insertion sort returns a sorted list.
85def isort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>) -> MList.sorted_by(~A, ~le, MPerm.isort_by(~A, ~le, xs)):
86 match xs:
87 case Nil{}:
88 {==}
89 case +x <> t:
90 insert_by_sorted(~A, ~le, ~le_total, x, MPerm.isort_by(~A, ~le, t), isort_by_sorted(~A, ~le, ~le_total, t))
91
92# Insertion sort returns a sorted Nat list.
93def isort_by_sorted_nat(+xs: List<&2, Nat>) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.isort_by(~Nat, ~Nat.is_le, xs)):
94 isort_by_sorted(~Nat, ~Nat.is_le, ~internal_le_flip_nat, xs)
95
96# A recursion, not List.all with a lambda over lo, which --verdict cannot translate (PLAN F38).
97def internal_all_ge(~A: Data, ~le: A -> A -> Bool, +lo: A, xs: List<&2, A>) -> Bool:
98 match xs:
99 case Nil{}:
100 True{}
101 case h <> t:
102 Bool.and(le(lo, h), internal_all_ge(~A, ~le, lo, t))
103
104def internal_least(~A: Data, ~le: A -> A -> Bool, +lo: A, +xs: List<&2, A>) -> Data:
105 {internal_all_ge(~A, ~le, lo, xs) == True{} : Bool}
106
107def internal_least_intro(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: {le(lo, h) == True{} : Bool}, ht: internal_least(~A, ~le, lo, t)) -> internal_least(~A, ~le, lo, h <> t):
108 %Equal.sym(Bool, le(lo, h), True{}, hh) : {Bool.and(_, internal_all_ge(~A, ~le, lo, t)) == True{} : Bool}
109 ht
110
111def internal_least_cons_le(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: internal_least(~A, ~le, lo, h <> t)) -> {le(lo, h) == True{} : Bool}:
112 MList.internal_and_left(le(lo, h), internal_all_ge(~A, ~le, lo, t), hh)
113
114def internal_least_cons_tail(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: internal_least(~A, ~le, lo, h <> t)) -> internal_least(~A, ~le, lo, t):
115 MList.internal_and_right(le(lo, h), internal_all_ge(~A, ~le, lo, t), hh)
116
117def internal_least_trans(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +a: A, +b: A, +xs: List<&2, A>, +hab: {le(a, b) == True{} : Bool}, +hb: internal_least(~A, ~le, b, xs)) -> internal_least(~A, ~le, a, xs):
118 match xs:
119 case Nil{}:
120 {==}
121 case +h <> +t:
122 internal_least_intro(~A, ~le, a, h, t, le_trans(a, b, h, hab, internal_least_cons_le(~A, ~le, b, h, t, hb)), internal_least_trans(~A, ~le, ~le_trans, a, b, t, hab, internal_least_cons_tail(~A, ~le, b, h, t, hb)))
123
124def internal_sorted_least_head(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +xs: List<&2, A>, +x: A, +h: MList.sorted_by(~A, ~le, x <> xs)) -> internal_least(~A, ~le, x, xs):
125 match xs:
126 case Nil{}:
127 {==}
128 case +y <> +t:
129 internal_least_intro(~A, ~le, x, y, t, internal_sorted_cons_cons_elim_le(~A, ~le, x, y, t, h), internal_least_trans(~A, ~le, ~le_trans, x, y, t, internal_sorted_cons_cons_elim_le(~A, ~le, x, y, t, h), internal_sorted_least_head(~A, ~le, ~le_trans, t, y, internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h))))
130
131def internal_sorted_cons_of_least(~A: Data, ~le: A -> A -> Bool, +lo: A, +m: List<&2, A>, hl: internal_least(~A, ~le, lo, m), hm: MList.sorted_by(~A, ~le, m)) -> MList.sorted_by(~A, ~le, lo <> m):
132 match m:
133 case Nil{}:
134 {==}
135 case +z <> +t:
136 internal_sorted_cons_cons_intro(~A, ~le, lo, z, t, internal_least_cons_le(~A, ~le, lo, z, t, hl), hm)
137
138def internal_least_merge_pick(~A: Data, ~le: A -> A -> Bool, +lo: A, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, hx: internal_least(~A, ~le, lo, x <> xt), hy: internal_least(~A, ~le, lo, y <> yt), hm1: internal_least(~A, ~le, lo, MPerm.merge_by(~A, ~le, xt, y <> yt)), hm2: internal_least(~A, ~le, lo, MPerm.merge_by(~A, ~le, x <> xt, yt))) -> internal_least(~A, ~le, lo, Bool.pick(List<&2, A>, b, x <> MPerm.merge_by(~A, ~le, xt, y <> yt), y <> MPerm.merge_by(~A, ~le, x <> xt, yt))):
139 match b:
140 case True{}:
141 internal_least_intro(~A, ~le, lo, x, MPerm.merge_by(~A, ~le, xt, y <> yt), internal_least_cons_le(~A, ~le, lo, x, xt, hx), hm1)
142 case False{}:
143 internal_least_intro(~A, ~le, lo, y, MPerm.merge_by(~A, ~le, x <> xt, yt), internal_least_cons_le(~A, ~le, lo, y, yt, hy), hm2)
144
145def internal_least_merge(~A: Data, ~le: A -> A -> Bool, +lo: A, +xs: List<&2, A>, +ys: List<&2, A>, +hx: internal_least(~A, ~le, lo, xs), +hy: internal_least(~A, ~le, lo, ys)) -> internal_least(~A, ~le, lo, MPerm.merge_by(~A, ~le, xs, ys)):
146 match xs ys:
147 case Nil{} _:
148 hy
149 case +x <> +xt Nil{}:
150 hx
151 case +x <> +xt +y <> +yt:
152 internal_least_merge_pick(~A, ~le, lo, le(x, y), x, xt, y, yt, hx, hy, internal_least_merge(~A, ~le, lo, xt, y <> yt, internal_least_cons_tail(~A, ~le, lo, x, xt, hx), hy), internal_least_merge(~A, ~le, lo, x <> xt, yt, hx, internal_least_cons_tail(~A, ~le, lo, y, yt, hy)))
153
154def internal_merge_sorted_pick(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, +e: {le(x, y) == b : Bool}, hx: MList.sorted_by(~A, ~le, x <> xt), hy: MList.sorted_by(~A, ~le, y <> yt), hm1: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, xt, y <> yt)), hm2: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, x <> xt, yt))) -> MList.sorted_by(~A, ~le, Bool.pick(List<&2, A>, b, x <> MPerm.merge_by(~A, ~le, xt, y <> yt), y <> MPerm.merge_by(~A, ~le, x <> xt, yt))):
155 match b:
156 case True{}:
157 internal_sorted_cons_of_least(~A, ~le, x, MPerm.merge_by(~A, ~le, xt, y <> yt), internal_least_merge(~A, ~le, x, xt, y <> yt, internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx), internal_least_intro(~A, ~le, x, y, yt, e, internal_least_trans(~A, ~le, ~le_trans, x, y, yt, e, internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)))), hm1)
158 case False{}:
159 internal_sorted_cons_of_least(~A, ~le, y, MPerm.merge_by(~A, ~le, x <> xt, yt), internal_least_merge(~A, ~le, y, x <> xt, yt, internal_least_intro(~A, ~le, y, x, xt, le_total(x, y, e), internal_least_trans(~A, ~le, ~le_trans, y, x, xt, le_total(x, y, e), internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx))), internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)), hm2)
160
161# Merging two sorted lists is sorted (needs transitivity, and totality for the un-taken branch).
162def merge_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>, +ys: List<&2, A>, +hx: MList.sorted_by(~A, ~le, xs), +hy: MList.sorted_by(~A, ~le, ys)) -> MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, xs, ys)):
163 match xs ys:
164 case Nil{} _:
165 hy
166 case +x <> +xt Nil{}:
167 hx
168 case +x <> +xt +y <> +yt:
169 internal_merge_sorted_pick(~A, ~le, ~le_trans, ~le_total, le(x, y), x, xt, y, yt, {==}, hx, hy, merge_by_sorted(~A, ~le, ~le_trans, ~le_total, xt, y <> yt, internal_sorted_tail(~A, ~le, x, xt, hx), hy), merge_by_sorted(~A, ~le, ~le_trans, ~le_total, x <> xt, yt, hx, internal_sorted_tail(~A, ~le, y, yt, hy)))
170
171# Merging two sorted Nat lists gives a sorted list.
172def merge_by_sorted_nat(+xs: List<&2, Nat>, +ys: List<&2, Nat>, hx: MList.sorted_by(~Nat, ~Nat.is_le, xs), hy: MList.sorted_by(~Nat, ~Nat.is_le, ys)) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.merge_by(~Nat, ~Nat.is_le, xs, ys)):
173 merge_by_sorted(~Nat, ~Nat.is_le, ~internal_le_trans_nat, ~internal_le_flip_nat, xs, ys, hx, hy)
174
175def internal_length_zero(~A: Data, +xs: List<&2, A>, e: {List.length(&2, A, xs) == 0n : Nat}) -> {xs == Nil{} : List<&2, A>}:
176 match xs:
177 case Nil{}:
178 {==}
179 case +x <> +t:
180 Empty.absurd({x <> t == Nil{} : List<&2, A>}, MNat.zero_ne_succ(List.length(&2, A, t), Equal.sym(Nat, List.length(&2, A, x <> t), 0n, e)))
181
182def internal_sorted_short(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, h: MNat.le(List.length(&2, A, xs), 1n)) -> MList.sorted_by(~A, ~le, xs):
183 match xs:
184 case Nil{}:
185 {==}
186 case +x <> +t:
187 match t:
188 case Nil{}:
189 internal_sorted_single(~A, ~le, x)
190 case +y <> +u:
191 %Equal.sym(List<&2, A>, t, Nil{}, internal_length_zero(~A, t, MNat.le_zero_eq(List.length(&2, A, t), MNat.le_of_succ_le_succ(List.length(&2, A, t), 0n, h)))) : {MList.sorted_by(~A, ~le, x <> _) : Data}
192 internal_sorted_single(~A, ~le, x)
193
194def internal_length_evens_le(~A: Data, +xs: List<&2, A>) -> {Nat.is_le(List.length(&2, A, MPerm.evens(A, xs)), List.length(&2, A, xs)) == True{} : Bool}:
195 match xs:
196 case Nil{}:
197 {==}
198 case +x <> +r:
199 match r:
200 case Nil{}:
201 {==}
202 case +y <> +t:
203 MNat.succ_le_succ(List.length(&2, A, MPerm.evens(A, t)), 1n+List.length(&2, A, t), MNat.le_trans(List.length(&2, A, MPerm.evens(A, t)), List.length(&2, A, t), 1n+List.length(&2, A, t), internal_length_evens_le(~A, t), MNat.le_succ(List.length(&2, A, t))))
204
205def internal_length_odds_le(~A: Data, +xs: List<&2, A>) -> {Nat.is_le(List.length(&2, A, MPerm.odds(A, xs)), List.length(&2, A, xs)) == True{} : Bool}:
206 match xs:
207 case Nil{}:
208 {==}
209 case +x <> +r:
210 match r:
211 case Nil{}:
212 {==}
213 case +y <> +t:
214 MNat.succ_le_succ(List.length(&2, A, MPerm.odds(A, t)), 1n+List.length(&2, A, t), MNat.le_trans(List.length(&2, A, MPerm.odds(A, t)), List.length(&2, A, t), 1n+List.length(&2, A, t), internal_length_odds_le(~A, t), MNat.le_succ(List.length(&2, A, t))))
215
216# Merge sort returns a sorted list once the fuel reaches the input length (invariant: length <= fuel+1).
217def msort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, fuel: Nat, +xs: List<&2, A>, +h: {Nat.is_le(List.length(&2, A, xs), 1n+fuel) == True{} : Bool}) -> MList.sorted_by(~A, ~le, MPerm.msort_by(~A, ~le, fuel, xs)):
218 match fuel:
219 case 0n:
220 internal_sorted_short(~A, ~le, xs, h)
221 case 1n++f:
222 match xs:
223 case Nil{}:
224 merge_by_sorted(~A, ~le, ~le_trans, ~le_total, MPerm.msort_by(~A, ~le, f, MPerm.evens(A, xs)), MPerm.msort_by(~A, ~le, f, MPerm.odds(A, xs)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.evens(A, xs), MNat.zero_le(1n+f)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.odds(A, xs), MNat.zero_le(1n+f)))
225 case +x <> +r:
226 match r:
227 case Nil{}:
228 merge_by_sorted(~A, ~le, ~le_trans, ~le_total, MPerm.msort_by(~A, ~le, f, MPerm.evens(A, x <> r)), MPerm.msort_by(~A, ~le, f, MPerm.odds(A, x <> r)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.evens(A, x <> r), MNat.le_add_right(1n, f)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.odds(A, x <> r), MNat.zero_le(1n+f)))
229 case +y <> +t:
230 merge_by_sorted(~A, ~le, ~le_trans, ~le_total, MPerm.msort_by(~A, ~le, f, MPerm.evens(A, x <> y <> t)), MPerm.msort_by(~A, ~le, f, MPerm.odds(A, x <> y <> t)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.evens(A, x <> y <> t), MNat.succ_le_succ(List.length(&2, A, MPerm.evens(A, t)), f, MNat.le_trans(List.length(&2, A, MPerm.evens(A, t)), List.length(&2, A, t), f, internal_length_evens_le(~A, t), MNat.le_of_succ_le_succ(List.length(&2, A, t), f, MNat.le_of_succ_le_succ(1n+List.length(&2, A, t), 1n+f, h))))), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.odds(A, x <> y <> t), MNat.succ_le_succ(List.length(&2, A, MPerm.odds(A, t)), f, MNat.le_trans(List.length(&2, A, MPerm.odds(A, t)), List.length(&2, A, t), f, internal_length_odds_le(~A, t), MNat.le_of_succ_le_succ(List.length(&2, A, t), f, MNat.le_of_succ_le_succ(1n+List.length(&2, A, t), 1n+f, h))))))
231
232# Merge sort of the full-length fuel sorts its input.
233def sort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>) -> MList.sorted_by(~A, ~le, MPerm.sort_by(~A, ~le, xs)):
234 match xs:
235 case Nil{}:
236 {==}
237 case +x <> +t:
238 msort_by_sorted(~A, ~le, ~le_trans, ~le_total, 1n+List.length(&2, A, t), x <> t, MNat.le_succ(1n+List.length(&2, A, t)))
239
240# Merge sort with fuel = length returns a sorted Nat list (h always holds; sort_by_sorted_nat needs no h).
241def msort_by_sorted_nat(+xs: List<&2, Nat>, +h: {Nat.is_le(List.length(&2, Nat, xs), 1n+List.length(&2, Nat, xs)) == True{} : Bool}) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.msort_by(~Nat, ~Nat.is_le, List.length(&2, Nat, xs), xs)):
242 msort_by_sorted(~Nat, ~Nat.is_le, ~internal_le_trans_nat, ~internal_le_flip_nat, List.length(&2, Nat, xs), xs, h)
243
244# Merge sort returns a sorted Nat list.
245def sort_by_sorted_nat(+xs: List<&2, Nat>) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.sort_by(~Nat, ~Nat.is_le, xs)):
246 sort_by_sorted(~Nat, ~Nat.is_le, ~internal_le_trans_nat, ~internal_le_flip_nat, xs)