proofs/nat_order.bend
stelliferous@0.0.3.0 · 525 lines · 0 definitions
1import Base
2import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
3
4import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
5import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
6import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
7import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
8
9def not_below(+lower: Nat,+value: Nat,room: {Nat.is_le(lower,value) == True{} : Bool}) -> {Nat.is_lt(value,lower) == False{} : Bool}:
10 match lower value:
11 case 0n 0n: {==}
12 case 0n 1n+value: {==}
13 case 1n+lower 0n: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(room))
14 case 1n+lower 1n+value: not_below(lower,value,room)
15
16def cancel_offset_le(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}) ->
17 {Nat.is_le(left,right) == True{} : Bool}:
18 match offset:
19 case 0n: ordered
20 case 1n+previous: cancel_offset_le(previous,left,right,ordered)
21
22def equal_of_is_eq(+left: Nat,+right: Nat,equal: {Nat.is_eq(left,right) == True{} : Bool}) -> {left == right : Nat}:
23 match left right:
24 case 0n 0n: {==}
25 case 0n 1n+rest: Empty.absurd({0n == 1n+rest : Nat},WordEncoding.false_true(equal))
26 case 1n+rest 0n: Empty.absurd({1n+rest == 0n : Nat},WordEncoding.false_true(equal))
27 case 1n+ +previous 1n+ +last:
28 %equal_of_is_eq(previous,last,equal) : {1n+previous == 1n+_ : Nat}
29 {==}
30
31def subtract_zero(+value: Nat) -> {Nat.sub(value,0n) == value : Nat}:
32 match value:
33 case 0n: {==}
34 case 1n+rest: {==}
35
36def zero_subtract(value: Nat) -> {Nat.sub(0n,value) == 0n : Nat}:
37 match value:
38 case 0n: {==}
39 case 1n+rest: {==}
40
41def subtract_shift(+first: Nat,+row: Nat) -> {Nat.sub(Nat.add(first,row),first) == row : Nat}:
42 match first:
43 case 0n: subtract_zero(row)
44 case 1n+rest: subtract_shift(rest,row)
45
46def restore_shift(+first: Nat,+row: Nat,lower: {Nat.is_le(first,row) == True{} : Bool}) -> {Nat.add(first,Nat.sub(row,first)) == row : Nat}:
47 match first row:
48 case 0n row: subtract_zero(row)
49 case 1n+first 0n: Empty.absurd({Nat.add(1n+first,Nat.sub(0n,1n+first)) == 0n : Nat},WordEncoding.false_true(lower))
50 case 1n+ +first 1n+ +row:
51 Equal.cong(Nat,Nat,n => 1n+n,Nat.add(first,Nat.sub(row,first)),row,restore_shift(first,row,lower))
52
53def cancel_sum(+offset: Nat,+left: Nat,+right: Nat,equation: {Nat.add(offset,left) == Nat.add(offset,right) : Nat}) -> {left == right : Nat}:
54 Equal.trans(Nat,left,Nat.sub(Nat.add(offset,left),offset),right,Equal.sym(Nat,Nat.sub(Nat.add(offset,left),offset),left,subtract_shift(offset,left)),
55 Equal.trans(Nat,Nat.sub(Nat.add(offset,left),offset),Nat.sub(Nat.add(offset,right),offset),right,
56 Equal.cong(Nat,Nat,sum => Nat.sub(sum,offset),Nat.add(offset,left),Nat.add(offset,right),equation),subtract_shift(offset,right)))
57
58def positive_difference(+end: Nat,+begin: Nat,positive: {Nat.is_lt(begin,end) == True{} : Bool}) -> {Nat.is_lt(0n,Nat.sub(end,begin)) == True{} : Bool}:
59 match end begin:
60 case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
61 case 0n 1n+begin: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
62 case 1n+end 0n: {==}
63 case 1n+end 1n+begin: positive_difference(end,begin,positive)
64
65def positive_has_last(+size: Nat,positive: {Nat.is_lt(0n,size) == True{} : Bool}) -> {1n+Nat.sub(size,1n) == size : Nat}:
66 match size:
67 case 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(positive))
68 case 1n+ +rest:
69 %subtract_zero(rest) : {1n+Nat.sub(rest,0n) == 1n+_ : Nat}
70 {==}
71
72def split_at_element(+total: Nat,+index: Nat,inside: {Nat.is_lt(index,total) == True{} : Bool}) ->
73 {Nat.add(index,1n+Nat.sub(total,1n+index)) == total : Nat}:
74 match total index:
75 case 0n 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(inside))
76 case 1n+ +rest 0n:
77 Equal.cong(Nat,Nat,n => 1n+n,Nat.sub(rest,0n),rest,subtract_zero(rest))
78 case 0n 1n+ +index:
79 Empty.absurd({Nat.add(1n+index,1n) == 0n : Nat},WordEncoding.false_true(inside))
80 case 1n+ +rest 1n+ +index:
81 Equal.cong(Nat,Nat,n => 1n+n,Nat.add(index,1n+Nat.sub(rest,1n+index)),rest,split_at_element(rest,index,inside))
82
83# No number is below zero.
84def below_zero(+value: Nat,below: {Nat.is_lt(value,0n) == True{} : Bool}) -> Empty:
85 match value:
86 case 0n: WordEncoding.false_true(below)
87 case 1n+rest: WordEncoding.false_true(below)
88
89type UpperBound<-value: Nat,-limit: Nat> is Data:
90 Before{inside: {Nat.is_lt(value,limit) == True{} : Bool}}
91 At{equal: {value == limit : Nat}}
92
93def lift_upper_bound(+value: Nat,+limit: Nat,bound: UpperBound<value,limit>) -> UpperBound<1n+value,1n+limit>:
94 match bound:
95 case Before{inside}: Before{inside}
96 case At{equal}: At{Equal.cong(Nat,Nat,n => 1n+n,value,limit,equal)}
97
98def upper_bound_cases(+value: Nat,+limit: Nat,bounded: {Nat.is_le(value,limit) == True{} : Bool}) -> UpperBound<value,limit>:
99 match value limit:
100 case 0n 0n: At{{==}}
101 case 0n 1n+rest: Before{{==}}
102 case 1n+rest 0n: Empty.absurd(UpperBound<1n+rest,0n>,WordEncoding.false_true(bounded))
103 case 1n+ +previous 1n+ +last: lift_upper_bound(previous,last,upper_bound_cases(previous,last,bounded))
104
105def comparison_not_less(+comparison: Cmp,h: {Cmp.is_lt(comparison) == False{} : Bool}) -> {Cmp.is_ge(comparison) == True{} : Bool}:
106 match comparison:
107 case LT{}:
108 Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
109 case EQ{}: {==}
110 case GT{}: {==}
111
112def comparison_less_not_equal(+comparison: Cmp,less: {Cmp.is_lt(comparison) == True{} : Bool}) -> {Cmp.is_eq(comparison) == False{} : Bool}:
113 match comparison:
114 case LT{}: {==}
115 case EQ{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(less))
116 case GT{}: Empty.absurd({False{} == False{} : Bool},WordEncoding.false_true(less))
117
118def less_not_equal(+left: Nat,+right: Nat,less: {Nat.is_lt(left,right) == True{} : Bool}) -> {Nat.is_eq(left,right) == False{} : Bool}:
119 comparison_less_not_equal(Nat.cmp(left,right),less)
120
121def equal_reflexive(+value: Nat) -> {Nat.is_eq(value,value) == True{} : Bool}:
122 match value:
123 case 0n: {==}
124 case 1n+rest: equal_reflexive(rest)
125
126def equal_symmetric(+left: Nat,+right: Nat) -> {Nat.is_eq(left,right) == Nat.is_eq(right,left) : Bool}:
127 match left right:
128 case 0n 0n: {==}
129 case 0n 1n+right: {==}
130 case 1n+left 0n: {==}
131 case 1n+left 1n+right: equal_symmetric(left,right)
132
133def zero_le(+a: Nat) -> {Nat.is_le(0n,a) == True{} : Bool}:
134 match a:
135 case 0n:
136 {==}
137 case 1n+p:
138 {==}
139
140def reflexive(+a: Nat) -> {Nat.is_le(a,a) == True{} : Bool}:
141 match a:
142 case 0n:
143 {==}
144 case 1n+p:
145 reflexive(p)
146
147def offset_le(offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_le(left,right) == True{} : Bool}) ->
148 {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}:
149 match offset:
150 case 0n: ordered
151 case 1n+rest: offset_le(rest,left,right,ordered)
152
153def offset_lt(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_lt(left,right) == True{} : Bool}) ->
154 {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}:
155 match offset:
156 case 0n: ordered
157 case 1n+rest: offset_lt(rest,left,right,ordered)
158
159def cancel_offset_lt(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}) ->
160 {Nat.is_lt(left,right) == True{} : Bool}:
161 match offset:
162 case 0n: ordered
163 case 1n+rest: cancel_offset_lt(rest,left,right,ordered)
164
165def successor(+a: Nat,+b: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(a,1n+b) == True{} : Bool}:
166 match a:
167 case 0n:
168 {==}
169 case 1n+ +p:
170 match b:
171 case 0n:
172 Empty.absurd({Nat.is_le(1n+p,1n) == True{} : Bool},WordEncoding.false_true(h))
173 case 1n+q:
174 successor(p,q,h)
175
176def transitive(+a: Nat,+b: Nat,+c: Nat,ab: {Nat.is_le(a,b) == True{} : Bool},bc: {Nat.is_le(b,c) == True{} : Bool}) -> {Nat.is_le(a,
177 c) == True{} : Bool}:
178 match a:
179 case 0n:
180 zero_le(c)
181 case 1n+ +p:
182 match b:
183 case 0n:
184 Empty.absurd({Nat.is_le(1n+p,c) == True{} : Bool},WordEncoding.false_true(ab))
185 case 1n+ +q:
186 match c:
187 case 0n:
188 Empty.absurd({Nat.is_le(1n+p,0n) == True{} : Bool},WordEncoding.false_true(bc))
189 case 1n+r:
190 transitive(p,q,r,ab,bc)
191
192def le_add(+a: Nat,+b: Nat) -> {Nat.is_le(a,Nat.add(a,b)) == True{} : Bool}:
193 match a:
194 case 0n:
195 zero_le(b)
196 case 1n+p:
197 le_add(p,b)
198
199def le_double(+a: Nat) -> {Nat.is_le(a,Nat.double(a)) == True{} : Bool}:
200 %Addition.double(a) : {Nat.is_le(a,_) == True{} : Bool}
201 le_add(a,a)
202
203def double_le(+a: Nat,+b: Nat,ordered: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(Nat.double(a),Nat.double(b)) == True{} : Bool}:
204 match a b:
205 case 0n b: zero_le(Nat.double(b))
206 case 1n+a 0n: Empty.absurd({Nat.is_le(Nat.double(1n+a),0n) == True{} : Bool},WordEncoding.false_true(ordered))
207 case 1n+a 1n+b: double_le(a,b,ordered)
208
209def sub_le(+a: Nat,+b: Nat) -> {Nat.is_le(Nat.sub(a,b),a) == True{} : Bool}:
210 match a b:
211 case 0n 0n:
212 {==}
213 case 0n 1n+b:
214 {==}
215 case 1n+ +a 0n:
216 reflexive(1n+a)
217 case 1n+ +a 1n+ +b:
218 successor(Nat.sub(a,b),a,sub_le(a,b))
219
220def sub_lt(+a: Nat,+b: Nat,+c: Nat,order: {Nat.is_le(b,a) == True{} : Bool},bound: {Nat.is_lt(a,Nat.add(b,
221 c)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a,b),c) == True{} : Bool}:
222 match a b:
223 case 0n 0n:
224 bound
225 case 0n 1n+b:
226 Empty.absurd({Nat.is_lt(0n,c) == True{} : Bool},WordEncoding.false_true(order))
227 case 1n+a 0n:
228 bound
229 case 1n+a 1n+b:
230 sub_lt(a,b,c,order,bound)
231
232def ge_le(+a: Nat,+b: Nat) -> {Nat.is_ge(a,b) == Nat.is_le(b,a) : Bool}:
233 match a b:
234 case 0n 0n:
235 {==}
236 case 0n 1n+b:
237 {==}
238 case 1n+a 0n:
239 {==}
240 case 1n+a 1n+b:
241 ge_le(a,b)
242
243def ge_true(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == True{} : Bool}) -> {Nat.is_le(b,a) == True{} : Bool}:
244 %ge_le(a,b) : {_ == True{} : Bool}
245 h
246
247def ge_false(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == False{} : Bool}) -> {Nat.is_lt(a,b) == True{} : Bool}:
248 match a b:
249 case 0n 0n:
250 Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
251 case 0n 1n+b:
252 {==}
253 case 1n+a 0n:
254 Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
255 case 1n+a 1n+b:
256 ge_false(a,b,h)
257
258def digit_lt(+a: Nat,+b: Nat,+bit: Bool,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(Comparison.digit(bit,a),
259 Nat.double(b)) == True{} : Bool}:
260 match a b bit:
261 case 0n 0n bit:
262 Empty.absurd({Nat.is_lt(Comparison.digit(bit,0n),0n) == True{} : Bool},WordEncoding.false_true(h))
263 case 0n 1n+b False{}:
264 {==}
265 case 0n 1n+b True{}:
266 {==}
267 case 1n+a 0n bit:
268 Empty.absurd({Nat.is_lt(Comparison.digit(bit,1n+a),0n) == True{} : Bool},WordEncoding.false_true(h))
269 case 1n+a 1n+b False{}:
270 digit_lt(a,b,False{},h)
271 case 1n+a 1n+b True{}:
272 digit_lt(a,b,True{},h)
273
274def digit_bounded(+a: Nat,+b: Nat,+bit: Bool,+cap: Nat,small: {Nat.is_lt(a,b) == True{} : Bool},large: {Nat.is_le(Nat.double(b),
275 cap) == True{} : Bool}) -> {Nat.is_le(Comparison.digit(bit,a),cap) == True{} : Bool}:
276 Bounds.strict_le(Comparison.digit(bit,a),cap,Bounds.nat_trans(Comparison.digit(bit,a),Nat.double(b),cap,digit_lt(a,b,bit,
277 small),large))
278
279def commutative(+a: Nat,+b: Nat) -> {Nat.add(a,b) == Nat.add(b,a) : Nat}:
280 match a:
281 case 0n:
282 Equal.sym(Nat,Nat.add(b,0n),b,Addition.zero_right(b))
283 case 1n+ +p:
284 %Equal.sym(Nat,Nat.add(b,1n+p),1n+Nat.add(b,p),Addition.successor_right(b,p)) : {1n+Nat.add(p,b) == _ : Nat}
285 %commutative(p,b) : {1n+Nat.add(p,b) == 1n+_ : Nat}
286 {==}
287
288def le_lt_trans(+a: Nat,+b: Nat,+c: Nat,ab: {Nat.is_le(a,b) == True{} : Bool},bc: {Nat.is_lt(b,c) == True{} : Bool}) -> {Nat.is_lt(a,
289 c) == True{} : Bool}:
290 match a b c:
291 case 0n 0n 0n:
292 Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
293 case 0n 1n+b 0n:
294 Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
295 case 0n b 1n+c:
296 {==}
297 case 1n+a 0n c:
298 Empty.absurd({Nat.is_lt(1n+a,c) == True{} : Bool},WordEncoding.false_true(ab))
299 case 1n+a 1n+b 0n:
300 Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(bc))
301 case 1n+a 1n+b 1n+c:
302 le_lt_trans(a,b,c,ab,bc)
303
304def advance_room(+i: Nat,+tail: Nat,+cap: Nat,h: {Nat.is_le(Nat.add(i,1n+tail),cap) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+i,tail),
305 cap) == True{} : Bool}:
306 %Addition.successor_right(i,tail) : {Nat.is_le(_,cap) == True{} : Bool}
307 h
308
309def room_index(+i: Nat,+tail: Nat,+cap: Nat,h: {Nat.is_le(Nat.add(i,1n+tail),cap) == True{} : Bool}) -> {Nat.is_lt(i,cap) == True{} : Bool}:
310 le_lt_trans(i,Nat.add(i,tail),cap,le_add(i,tail),Bounds.predecessor_strict(Nat.add(i,tail),cap,advance_room(i,tail,cap,h)))
311
312# Order structure shared by padding, allocation and mixed-radix indexing.
313def lt_succ(+a: Nat,+b: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_lt(a,1n+b) == True{} : Bool}:
314 match a b:
315 case 0n 0n:
316 {==}
317 case 0n 1n+b:
318 {==}
319 case 1n+a 0n:
320 Empty.absurd({Nat.is_lt(1n+a,1n) == True{} : Bool},WordEncoding.false_true(h))
321 case 1n+a 1n+b:
322 lt_succ(a,b,h)
323
324# Order structure shared by padding, allocation and mixed-radix indexing.
325def add_le(+a: Nat,+b: Nat,+c: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a,c),Nat.add(b,c)) == True{} : Bool}:
326 match a b:
327 case 0n 0n:
328 reflexive(c)
329 case 0n 1n+ +b:
330 successor(c,Nat.add(b,c),
331 %commutative(c,b) : {Nat.is_le(c,_) == True{} : Bool}
332 le_add(c,b))
333 case 1n+a 0n:
334 Empty.absurd({Nat.is_le(Nat.add(1n+a,c),c) == True{} : Bool},WordEncoding.false_true(h))
335 case 1n+a 1n+b:
336 add_le(a,b,c,h)
337
338# Order structure shared by padding, allocation and mixed-radix indexing.
339def add_lt(+a: Nat,+b: Nat,+c: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a,c),Nat.add(b,c)) == True{} : Bool}:
340 match a b:
341 case 0n 0n:
342 Empty.absurd({Nat.is_lt(c,c) == True{} : Bool},WordEncoding.false_true(h))
343 case 0n 1n+ +b:
344 lt_succ(c,Nat.add(b,c),
345 %commutative(c,b) : {Nat.is_le(c,_) == True{} : Bool}
346 le_add(c,b))
347 case 1n+a 0n:
348 Empty.absurd({Nat.is_lt(Nat.add(1n+a,c),c) == True{} : Bool},WordEncoding.false_true(h))
349 case 1n+a 1n+b:
350 add_lt(a,b,c,h)
351
352# Order structure shared by padding, allocation and mixed-radix indexing.
353def strict_follow(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(1n+a,b) == True{} : Bool}:
354 match a b:
355 case 0n 0n:
356 Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(h))
357 case 0n 1n+b:
358 zero_le(b)
359 case 1n+a 0n:
360 Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(h))
361 case 1n+a 1n+b:
362 strict_follow(a,b,h)
363
364# Translate a comparison against a remaining extent to its absolute position.
365def below_difference(+offset: Nat,+value: Nat,+end: Nat,ordered: {Nat.is_le(offset,end) == True{} : Bool}) ->
366 {Nat.is_lt(value,Nat.sub(end,offset)) == Nat.is_lt(Nat.add(offset,value),end) : Bool}:
367 match offset end:
368 case 0n end:
369 %Equal.sym(Nat,Nat.sub(end,0n),end,subtract_zero(end)) : {Nat.is_lt(value,_) == Nat.is_lt(value,end) : Bool}
370 {==}
371 case 1n+offset 0n:
372 Empty.absurd({Nat.is_lt(value,Nat.sub(0n,1n+offset)) == Nat.is_lt(Nat.add(1n+offset,value),0n) : Bool},WordEncoding.false_true(ordered))
373 case 1n+offset 1n+end: below_difference(offset,value,end,ordered)
374
375# Two opposite bounds identify a natural number.
376def antisymmetric(+left: Nat,+right: Nat,forward: {Nat.is_le(left,right) == True{} : Bool},backward: {Nat.is_le(right,left) == True{} : Bool}) -> {left == right : Nat}:
377 match left right:
378 case 0n 0n: {==}
379 case 0n 1n+right: Empty.absurd({0n == 1n+right : Nat},WordEncoding.false_true(backward))
380 case 1n+left 0n: Empty.absurd({1n+left == 0n : Nat},WordEncoding.false_true(forward))
381 case 1n+ +left 1n+ +right:
382 Equal.cong(Nat,Nat,value => 1n+value,left,right,antisymmetric(left,right,forward,backward))
383
384# Additive complements describe reflected digits without subtraction premises.
385def below_sum(+value: Nat,+more: Nat) -> {Nat.is_lt(value,Nat.add(value,1n+more)) == True{} : Bool}:
386 match value:
387 case 0n: {==}
388 case 1n+ +rest: below_sum(rest,more)
389
390def below_complement(+value: Nat,+more: Nat,+total: Nat,place: {Nat.add(value,1n+more) == total : Nat}) -> {Nat.is_lt(value,total) == True{} : Bool}:
391 %place : {Nat.is_lt(value,_) == True{} : Bool}
392 below_sum(value,more)
393
394def subtract_one_complement(+left: Nat,+right: Nat) -> {Nat.sub(Nat.add(left,1n+right),1n) == Nat.add(left,right) : Nat}:
395 Equal.trans(Nat,Nat.sub(Nat.add(left,1n+right),1n),Nat.sub(1n+Nat.add(left,right),1n),Nat.add(left,right),
396 Equal.cong(Nat,Nat,value => Nat.sub(value,1n),Nat.add(left,1n+right),1n+Nat.add(left,right),Addition.successor_right(left,right)),subtract_zero(Nat.add(left,right)))
397
398def reflected_complement(+digit: Nat,+reflected: Nat,+extent: Nat,place: {Nat.add(digit,1n+reflected) == extent : Nat}) ->
399 {Nat.sub(Nat.sub(extent,1n),digit) == reflected : Nat}:
400 Equal.trans(Nat,Nat.sub(Nat.sub(extent,1n),digit),Nat.sub(Nat.add(digit,reflected),digit),reflected,
401 Equal.cong(Nat,Nat,value => Nat.sub(value,digit),Nat.sub(extent,1n),Nat.add(digit,reflected),
402 Equal.trans(Nat,Nat.sub(extent,1n),Nat.sub(Nat.add(digit,1n+reflected),1n),Nat.add(digit,reflected),
403 Equal.cong(Nat,Nat,value => Nat.sub(value,1n),extent,Nat.add(digit,1n+reflected),Equal.sym(Nat,Nat.add(digit,1n+reflected),extent,place)),subtract_one_complement(digit,reflected))),subtract_shift(digit,reflected))
404
405# Truncated subtraction is adjoint to addition for non-strict bounds.
406def subtraction_le(+end: Nat,+offset: Nat,+value: Nat) ->
407 {Nat.is_le(Nat.sub(end,offset),value) == Nat.is_le(end,Nat.add(offset,value)) : Bool}:
408 match end offset:
409 case 0n 0n: {==}
410 case 0n 1n+rest: zero_le(value)
411 case 1n+rest 0n: {==}
412 case 1n+rest 1n+offset: subtraction_le(rest,offset,value)
413
414# The strict counterpart includes offsets beyond the endpoint.
415def subtraction_lt(+end: Nat,+offset: Nat,+value: Nat) ->
416 {Nat.is_lt(value,Nat.sub(end,offset)) == Nat.is_lt(Nat.add(offset,value),end) : Bool}:
417 match end offset:
418 case 0n 0n: {==}
419 case 0n 1n+rest: not_below(0n,value,zero_le(value))
420 case 1n+rest 0n: {==}
421 case 1n+rest 1n+offset: subtraction_lt(rest,offset,value)
422
423def strict_complement(+left: Nat,+right: Nat) ->
424 {Nat.is_lt(left,right) == Bool.not(Nat.is_le(right,left)) : Bool}:
425 match left right:
426 case 0n 0n: {==}
427 case 0n 1n+rest: {==}
428 case 1n+rest 0n: {==}
429 case 1n+left 1n+right: strict_complement(left,right)
430
431def drop_left_le(+offset: Nat,+count: Nat,+stride: Nat,span: {Nat.is_le(Nat.add(offset,count),stride) == True{} : Bool}) ->
432 {Nat.is_le(count,stride) == True{} : Bool}:
433 transitive(count,Nat.add(offset,count),stride,
434 %commutative(count,offset) : {Nat.is_le(count,_) == True{} : Bool}
435 le_add(count,offset),span)
436
437# Adding the window's image-relative start translates a valid padded row.
438def subtract_from_sum(+offset: Nat,+coordinate: Nat,+padding: Nat,ordered: {Nat.is_le(padding,coordinate) == True{} : Bool}) ->
439 {Nat.sub(Nat.add(offset,coordinate),padding) == Nat.add(offset,Nat.sub(coordinate,padding)) : Nat}:
440 match coordinate padding:
441 case +coordinate 0n: Equal.trans(Nat,Nat.sub(Nat.add(offset,coordinate),0n),Nat.add(offset,coordinate),Nat.add(offset,Nat.sub(coordinate,0n)),subtract_zero(Nat.add(offset,coordinate)),
442 Equal.cong(Nat,Nat,value => Nat.add(offset,value),coordinate,Nat.sub(coordinate,0n),Equal.sym(Nat,Nat.sub(coordinate,0n),coordinate,subtract_zero(coordinate))))
443 case 0n 1n+padding: Empty.absurd({Nat.sub(Nat.add(offset,0n),1n+padding) == Nat.add(offset,0n) : Nat},WordEncoding.false_true(ordered))
444 case 1n+ +coordinate 1n+ +padding:
445 %Equal.sym(Nat,Nat.add(offset,1n+coordinate),1n+Nat.add(offset,coordinate),Addition.successor_right(offset,coordinate)) :
446 {Nat.sub(_,1n+padding) == Nat.add(offset,Nat.sub(coordinate,padding)) : Nat}
447 subtract_from_sum(offset,coordinate,padding,ordered)
448
449def le_offset(+offset: Nat,+left: Nat,+right: Nat) -> {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == Nat.is_le(left,right) : Bool}:
450 match offset:
451 case 0n: {==}
452 case 1n+ +rest: le_offset(rest,left,right)
453
454def lt_offset(+offset: Nat,+left: Nat,+right: Nat) -> {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == Nat.is_lt(left,right) : Bool}:
455 match offset:
456 case 0n: {==}
457 case 1n+ +rest: lt_offset(rest,left,right)
458
459# A mapped interval remains image-local, including a zero interval at the
460# next image boundary. This lemma separates row geometry from stored values.
461def subtract_below(+value: Nat,+amount: Nat,inside: {Nat.is_le(value,amount) == True{} : Bool}) -> {Nat.sub(value,amount) == 0n : Nat}:
462 match value amount:
463 case 0n amount: zero_subtract(amount)
464 case 1n+value 0n: Empty.absurd({Nat.sub(1n+value,0n) == 0n : Nat},WordEncoding.false_true(inside))
465 case 1n+ +value 1n+ +amount: subtract_below(value,amount,inside)
466
467def product_positive(+left: Nat,+right: Nat,left_positive: {Nat.is_lt(0n,left) == True{} : Bool},right_positive: {Nat.is_lt(0n,right) == True{} : Bool}) ->
468 {Nat.is_lt(0n,Nat.mul(left,right)) == True{} : Bool}:
469 match left right:
470 case 0n right: Empty.absurd({Nat.is_lt(0n,Nat.mul(0n,right)) == True{} : Bool},WordEncoding.false_true(left_positive))
471 case 1n+left 0n: Empty.absurd({Nat.is_lt(0n,Nat.mul(1n+left,0n)) == True{} : Bool},WordEncoding.false_true(right_positive))
472 case 1n+left 1n+right: {==}
473
474def not_less(+left: Nat,+right: Nat,order: {Nat.is_lt(left,right) == False{} : Bool}) -> {Nat.is_le(right,left) == True{} : Bool}:
475 match left right:
476 case left 0n: zero_le(left)
477 case 0n 1n+right: Empty.absurd({Nat.is_le(1n+right,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},order)))
478 case 1n+left 1n+right: not_less(left,right,order)
479
480def positive_bound(+value: Nat,+limit: Nat,inside: {Nat.is_lt(value,limit) == True{} : Bool}) -> {Nat.is_lt(0n,limit) == True{} : Bool}:
481 le_lt_trans(0n,value,limit,zero_le(value),inside)
482
483def nonzero_positive(+value: Nat,nonzero: {Nat.is_eq(value,0n) == False{} : Bool}) -> {Nat.is_lt(0n,value) == True{} : Bool}:
484 match value:
485 case 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},nonzero)))
486 case 1n+rest: {==}
487
488def zero_below(+value: Nat,bounded: {Nat.is_le(value,0n) == True{} : Bool}) -> {value == 0n : Nat}:
489 match value:
490 case 0n: {==}
491 case 1n+rest: Empty.absurd({1n+rest == 0n : Nat},WordEncoding.false_true(bounded))
492
493def positive_one(+length: Nat,positive: {Nat.is_lt(0n,length) == True{} : Bool}) -> {Nat.is_le(1n,length) == True{} : Bool}:
494 strict_follow(0n,length,positive)
495
496def last_below(+length: Nat,positive: {Nat.is_lt(0n,length) == True{} : Bool}) ->
497 {Nat.is_lt(Nat.sub(length,1n),length) == True{} : Bool}:
498 %positive_has_last(length,positive) : {Nat.is_lt(Nat.sub(length,1n),_) == True{} : Bool}
499 lt_succ(Nat.sub(length,1n),Nat.sub(length,1n),reflexive(Nat.sub(length,1n)))
500
501def twice(+value: Nat) -> {Nat.mul(2n,value) == Nat.add(value,value) : Nat}:
502 Equal.cong(Nat,Nat,tail => Nat.add(value,tail),Nat.add(value,0n),value,Addition.zero_right(value))
503
504def times_one(+value: Nat) -> {Nat.mul(value,1n) == value : Nat}:
505 match value:
506 case 0n: {==}
507 case 1n+ +rest:
508 Equal.cong(Nat,Nat,value => 1n+value,Nat.mul(rest,1n),rest,times_one(rest))
509
510def before_last(+offset: Nat,+length: Nat,inside: {Nat.is_lt(offset,length) == True{} : Bool}) ->
511 {Nat.is_le(offset,Nat.sub(length,1n)) == True{} : Bool}:
512 match length:
513 case 0n:
514 Empty.absurd({Nat.is_le(offset,0n) == True{} : Bool},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(offset,0n),True{},Equal.sym(Bool,Nat.is_lt(offset,0n),False{},Division.lt_zero(offset)),inside)))
515 case 1n+ +last:
516 %Equal.sym(Nat,Nat.sub(last,0n),last,subtract_zero(last)) : {Nat.is_le(offset,_) == True{} : Bool}
517 Division.lt_succ_le(offset,last,inside)
518
519def difference_positive(+begin: Nat,+finish: Nat,positive: {Nat.is_lt(0n,Nat.sub(finish,begin)) == True{} : Bool}) ->
520 {Nat.is_lt(begin,finish) == True{} : Bool}:
521 match begin finish:
522 case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
523 case 0n 1n+finish: {==}
524 case 1n+begin 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
525 case 1n+ +begin 1n+ +finish: difference_positive(begin,finish,positive)