1	import Base
2	import ./natural_addition.bend as Addition
3	
4	import ./u32_comparison.bend as Comparison
5	import ./nat_to_u32_bounds.bend as Bounds
6	import ./word_encoding.bend as WordEncoding
7	
8	def not_below(+lower: Nat,+value: Nat,room: {Nat.is_le(lower,value) == True{} : Bool}) -> {Nat.is_lt(value,lower) == False{} : Bool}:
9	  match lower value:
10	    case 0n 0n: {==}
11	    case 0n 1n+value: {==}
12	    case 1n+lower 0n: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(room))
13	    case 1n+lower 1n+value: not_below(lower,value,room)
14	
15	def cancel_offset_le(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}) ->
16	  {Nat.is_le(left,right) == True{} : Bool}:
17	  match offset:
18	    case 0n: ordered
19	    case 1n+previous: cancel_offset_le(previous,left,right,ordered)
20	
21	def equal_of_is_eq(+left: Nat,+right: Nat,equal: {Nat.is_eq(left,right) == True{} : Bool}) -> {left == right : Nat}:
22	  match left right:
23	    case 0n 0n: {==}
24	    case 0n 1n+rest: Empty.absurd({0n == 1n+rest : Nat},WordEncoding.false_true(equal))
25	    case 1n+rest 0n: Empty.absurd({1n+rest == 0n : Nat},WordEncoding.false_true(equal))
26	    case 1n+ +previous 1n+ +last:
27	      %equal_of_is_eq(previous,last,equal) : {1n+previous == 1n+_ : Nat}
28	      {==}
29	
30	def subtract_zero(+value: Nat) -> {Nat.sub(value,0n) == value : Nat}:
31	  match value:
32	    case 0n: {==}
33	    case 1n+rest: {==}
34	
35	def zero_subtract(value: Nat) -> {Nat.sub(0n,value) == 0n : Nat}:
36	  match value:
37	    case 0n: {==}
38	    case 1n+rest: {==}
39	
40	def subtract_shift(+first: Nat,+row: Nat) -> {Nat.sub(Nat.add(first,row),first) == row : Nat}:
41	  match first:
42	    case 0n: subtract_zero(row)
43	    case 1n+rest: subtract_shift(rest,row)
44	
45	def restore_shift(+first: Nat,+row: Nat,lower: {Nat.is_le(first,row) == True{} : Bool}) -> {Nat.add(first,Nat.sub(row,first)) == row : Nat}:
46	  match first row:
47	    case 0n row: subtract_zero(row)
48	    case 1n+first 0n: Empty.absurd({Nat.add(1n+first,Nat.sub(0n,1n+first)) == 0n : Nat},WordEncoding.false_true(lower))
49	    case 1n+ +first 1n+ +row:
50	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(first,Nat.sub(row,first)),row,restore_shift(first,row,lower))
51	
52	def cancel_sum(+offset: Nat,+left: Nat,+right: Nat,equation: {Nat.add(offset,left) == Nat.add(offset,right) : Nat}) -> {left == right : Nat}:
53	  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)),
54	    Equal.trans(Nat,Nat.sub(Nat.add(offset,left),offset),Nat.sub(Nat.add(offset,right),offset),right,
55	      Equal.cong(Nat,Nat,sum => Nat.sub(sum,offset),Nat.add(offset,left),Nat.add(offset,right),equation),subtract_shift(offset,right)))
56	
57	def positive_difference(+end: Nat,+begin: Nat,positive: {Nat.is_lt(begin,end) == True{} : Bool}) -> {Nat.is_lt(0n,Nat.sub(end,begin)) == True{} : Bool}:
58	  match end begin:
59	    case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
60	    case 0n 1n+begin: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
61	    case 1n+end 0n: {==}
62	    case 1n+end 1n+begin: positive_difference(end,begin,positive)
63	
64	def positive_has_last(+size: Nat,positive: {Nat.is_lt(0n,size) == True{} : Bool}) -> {1n+Nat.sub(size,1n) == size : Nat}:
65	  match size:
66	    case 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(positive))
67	    case 1n+ +rest:
68	      %subtract_zero(rest) : {1n+Nat.sub(rest,0n) == 1n+_ : Nat}
69	      {==}
70	
71	def split_at_element(+total: Nat,+index: Nat,inside: {Nat.is_lt(index,total) == True{} : Bool}) ->
72	  {Nat.add(index,1n+Nat.sub(total,1n+index)) == total : Nat}:
73	  match total index:
74	    case 0n 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(inside))
75	    case 1n+ +rest 0n:
76	      Equal.cong(Nat,Nat,n => 1n+n,Nat.sub(rest,0n),rest,subtract_zero(rest))
77	    case 0n 1n+ +index:
78	      Empty.absurd({Nat.add(1n+index,1n) == 0n : Nat},WordEncoding.false_true(inside))
79	    case 1n+ +rest 1n+ +index:
80	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(index,1n+Nat.sub(rest,1n+index)),rest,split_at_element(rest,index,inside))
81	
82	type UpperBound<-value: Nat,-limit: Nat> is Data:
83	  Before{inside: {Nat.is_lt(value,limit) == True{} : Bool}}
84	  At{equal: {value == limit : Nat}}
85	
86	def lift_upper_bound(+value: Nat,+limit: Nat,bound: UpperBound<value,limit>) -> UpperBound<1n+value,1n+limit>:
87	  match bound:
88	    case Before{inside}: Before{inside}
89	    case At{equal}: At{Equal.cong(Nat,Nat,n => 1n+n,value,limit,equal)}
90	
91	def upper_bound_cases(+value: Nat,+limit: Nat,bounded: {Nat.is_le(value,limit) == True{} : Bool}) -> UpperBound<value,limit>:
92	  match value limit:
93	    case 0n 0n: At{{==}}
94	    case 0n 1n+rest: Before{{==}}
95	    case 1n+rest 0n: Empty.absurd(UpperBound<1n+rest,0n>,WordEncoding.false_true(bounded))
96	    case 1n+ +previous 1n+ +last: lift_upper_bound(previous,last,upper_bound_cases(previous,last,bounded))
97	
98	def comparison_not_less(+comparison: Cmp,h: {Cmp.is_lt(comparison) == False{} : Bool}) -> {Cmp.is_ge(comparison) == True{} : Bool}:
99	  match comparison:
100	    case LT{}:
101	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
102	    case EQ{}: {==}
103	    case GT{}: {==}
104	
105	def comparison_less_not_equal(+comparison: Cmp,less: {Cmp.is_lt(comparison) == True{} : Bool}) -> {Cmp.is_eq(comparison) == False{} : Bool}:
106	  match comparison:
107	    case LT{}: {==}
108	    case EQ{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(less))
109	    case GT{}: Empty.absurd({False{} == False{} : Bool},WordEncoding.false_true(less))
110	
111	def less_not_equal(+left: Nat,+right: Nat,less: {Nat.is_lt(left,right) == True{} : Bool}) -> {Nat.is_eq(left,right) == False{} : Bool}:
112	  comparison_less_not_equal(Nat.cmp(left,right),less)
113	
114	def equal_reflexive(+value: Nat) -> {Nat.is_eq(value,value) == True{} : Bool}:
115	  match value:
116	    case 0n: {==}
117	    case 1n+rest: equal_reflexive(rest)
118	
119	def equal_symmetric(+left: Nat,+right: Nat) -> {Nat.is_eq(left,right) == Nat.is_eq(right,left) : Bool}:
120	  match left right:
121	    case 0n 0n: {==}
122	    case 0n 1n+right: {==}
123	    case 1n+left 0n: {==}
124	    case 1n+left 1n+right: equal_symmetric(left,right)
125	
126	def zero_le(+a: Nat) -> {Nat.is_le(0n,a) == True{} : Bool}:
127	  match a:
128	    case 0n:
129	      {==}
130	    case 1n+p:
131	      {==}
132	
133	def reflexive(+a: Nat) -> {Nat.is_le(a,a) == True{} : Bool}:
134	  match a:
135	    case 0n:
136	      {==}
137	    case 1n+p:
138	      reflexive(p)
139	
140	def offset_le(offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_le(left,right) == True{} : Bool}) ->
141	  {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}:
142	  match offset:
143	    case 0n: ordered
144	    case 1n+rest: offset_le(rest,left,right,ordered)
145	
146	def offset_lt(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_lt(left,right) == True{} : Bool}) ->
147	  {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}:
148	  match offset:
149	    case 0n: ordered
150	    case 1n+rest: offset_lt(rest,left,right,ordered)
151	
152	def cancel_offset_lt(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}) ->
153	  {Nat.is_lt(left,right) == True{} : Bool}:
154	  match offset:
155	    case 0n: ordered
156	    case 1n+rest: cancel_offset_lt(rest,left,right,ordered)
157	
158	def successor(+a: Nat,+b: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(a,1n+b) == True{} : Bool}:
159	  match a:
160	    case 0n:
161	      {==}
162	    case 1n+ +p:
163	      match b:
164	        case 0n:
165	          Empty.absurd({Nat.is_le(1n+p,1n) == True{} : Bool},WordEncoding.false_true(h))
166	        case 1n+q:
167	          successor(p,q,h)
168	
169	def 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,
170	    c) == True{} : Bool}:
171	  match a:
172	    case 0n:
173	      zero_le(c)
174	    case 1n+ +p:
175	      match b:
176	        case 0n:
177	          Empty.absurd({Nat.is_le(1n+p,c) == True{} : Bool},WordEncoding.false_true(ab))
178	        case 1n+ +q:
179	          match c:
180	            case 0n:
181	              Empty.absurd({Nat.is_le(1n+p,0n) == True{} : Bool},WordEncoding.false_true(bc))
182	            case 1n+r:
183	              transitive(p,q,r,ab,bc)
184	
185	def le_add(+a: Nat,+b: Nat) -> {Nat.is_le(a,Nat.add(a,b)) == True{} : Bool}:
186	  match a:
187	    case 0n:
188	      zero_le(b)
189	    case 1n+p:
190	      le_add(p,b)
191	
192	def le_double(+a: Nat) -> {Nat.is_le(a,Nat.double(a)) == True{} : Bool}:
193	  %Addition.double(a) : {Nat.is_le(a,_) == True{} : Bool}
194	  le_add(a,a)
195	
196	def 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}:
197	  match a b:
198	    case 0n b: zero_le(Nat.double(b))
199	    case 1n+a 0n: Empty.absurd({Nat.is_le(Nat.double(1n+a),0n) == True{} : Bool},WordEncoding.false_true(ordered))
200	    case 1n+a 1n+b: double_le(a,b,ordered)
201	
202	def sub_le(+a: Nat,+b: Nat) -> {Nat.is_le(Nat.sub(a,b),a) == True{} : Bool}:
203	  match a b:
204	    case 0n 0n:
205	      {==}
206	    case 0n 1n+b:
207	      {==}
208	    case 1n+ +a 0n:
209	      reflexive(1n+a)
210	    case 1n+ +a 1n+ +b:
211	      successor(Nat.sub(a,b),a,sub_le(a,b))
212	
213	def sub_lt(+a: Nat,+b: Nat,+c: Nat,order: {Nat.is_le(b,a) == True{} : Bool},bound: {Nat.is_lt(a,Nat.add(b,
214	        c)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a,b),c) == True{} : Bool}:
215	  match a b:
216	    case 0n 0n:
217	      bound
218	    case 0n 1n+b:
219	      Empty.absurd({Nat.is_lt(0n,c) == True{} : Bool},WordEncoding.false_true(order))
220	    case 1n+a 0n:
221	      bound
222	    case 1n+a 1n+b:
223	      sub_lt(a,b,c,order,bound)
224	
225	def ge_le(+a: Nat,+b: Nat) -> {Nat.is_ge(a,b) == Nat.is_le(b,a) : Bool}:
226	  match a b:
227	    case 0n 0n:
228	      {==}
229	    case 0n 1n+b:
230	      {==}
231	    case 1n+a 0n:
232	      {==}
233	    case 1n+a 1n+b:
234	      ge_le(a,b)
235	
236	def ge_true(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == True{} : Bool}) -> {Nat.is_le(b,a) == True{} : Bool}:
237	  %ge_le(a,b) : {_ == True{} : Bool}
238	  h
239	
240	def ge_false(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == False{} : Bool}) -> {Nat.is_lt(a,b) == True{} : Bool}:
241	  match a b:
242	    case 0n 0n:
243	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
244	    case 0n 1n+b:
245	      {==}
246	    case 1n+a 0n:
247	      Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
248	    case 1n+a 1n+b:
249	      ge_false(a,b,h)
250	
251	def digit_lt(+a: Nat,+b: Nat,+bit: Bool,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(Comparison.digit(bit,a),
252	    Nat.double(b)) == True{} : Bool}:
253	  match a b bit:
254	    case 0n 0n bit:
255	      Empty.absurd({Nat.is_lt(Comparison.digit(bit,0n),0n) == True{} : Bool},WordEncoding.false_true(h))
256	    case 0n 1n+b False{}:
257	      {==}
258	    case 0n 1n+b True{}:
259	      {==}
260	    case 1n+a 0n bit:
261	      Empty.absurd({Nat.is_lt(Comparison.digit(bit,1n+a),0n) == True{} : Bool},WordEncoding.false_true(h))
262	    case 1n+a 1n+b False{}:
263	      digit_lt(a,b,False{},h)
264	    case 1n+a 1n+b True{}:
265	      digit_lt(a,b,True{},h)
266	
267	def 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),
268	      cap) == True{} : Bool}) -> {Nat.is_le(Comparison.digit(bit,a),cap) == True{} : Bool}:
269	  Bounds.strict_le(Comparison.digit(bit,a),cap,Bounds.nat_trans(Comparison.digit(bit,a),Nat.double(b),cap,digit_lt(a,b,bit,
270	        small),large))
271	
272	def commutative(+a: Nat,+b: Nat) -> {Nat.add(a,b) == Nat.add(b,a) : Nat}:
273	  match a:
274	    case 0n:
275	      Equal.sym(Nat,Nat.add(b,0n),b,Addition.zero_right(b))
276	    case 1n+ +p:
277	      %Equal.sym(Nat,Nat.add(b,1n+p),1n+Nat.add(b,p),Addition.successor_right(b,p)) : {1n+Nat.add(p,b) == _ : Nat}
278	      %commutative(p,b) : {1n+Nat.add(p,b) == 1n+_ : Nat}
279	      {==}
280	
281	def 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,
282	    c) == True{} : Bool}:
283	  match a b c:
284	    case 0n 0n 0n:
285	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
286	    case 0n 1n+b 0n:
287	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
288	    case 0n b 1n+c:
289	      {==}
290	    case 1n+a 0n c:
291	      Empty.absurd({Nat.is_lt(1n+a,c) == True{} : Bool},WordEncoding.false_true(ab))
292	    case 1n+a 1n+b 0n:
293	      Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(bc))
294	    case 1n+a 1n+b 1n+c:
295	      le_lt_trans(a,b,c,ab,bc)
296	
297	def 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),
298	    cap) == True{} : Bool}:
299	  %Addition.successor_right(i,tail) : {Nat.is_le(_,cap) == True{} : Bool}
300	  h
301	
302	def 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}:
303	  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)))
304	
305	# Order structure shared by padding, allocation and mixed-radix indexing.
306	def lt_succ(+a: Nat,+b: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_lt(a,1n+b) == True{} : Bool}:
307	  match a b:
308	    case 0n 0n:
309	      {==}
310	    case 0n 1n+b:
311	      {==}
312	    case 1n+a 0n:
313	      Empty.absurd({Nat.is_lt(1n+a,1n) == True{} : Bool},WordEncoding.false_true(h))
314	    case 1n+a 1n+b:
315	      lt_succ(a,b,h)
316	
317	# Order structure shared by padding, allocation and mixed-radix indexing.
318	def 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}:
319	  match a b:
320	    case 0n 0n:
321	      reflexive(c)
322	    case 0n 1n+ +b:
323	      successor(c,Nat.add(b,c),
324	        %commutative(c,b) : {Nat.is_le(c,_) == True{} : Bool}
325	        le_add(c,b))
326	    case 1n+a 0n:
327	      Empty.absurd({Nat.is_le(Nat.add(1n+a,c),c) == True{} : Bool},WordEncoding.false_true(h))
328	    case 1n+a 1n+b:
329	      add_le(a,b,c,h)
330	
331	# Order structure shared by padding, allocation and mixed-radix indexing.
332	def 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}:
333	  match a b:
334	    case 0n 0n:
335	      Empty.absurd({Nat.is_lt(c,c) == True{} : Bool},WordEncoding.false_true(h))
336	    case 0n 1n+ +b:
337	      lt_succ(c,Nat.add(b,c),
338	        %commutative(c,b) : {Nat.is_le(c,_) == True{} : Bool}
339	        le_add(c,b))
340	    case 1n+a 0n:
341	      Empty.absurd({Nat.is_lt(Nat.add(1n+a,c),c) == True{} : Bool},WordEncoding.false_true(h))
342	    case 1n+a 1n+b:
343	      add_lt(a,b,c,h)
344	
345	# Order structure shared by padding, allocation and mixed-radix indexing.
346	def strict_follow(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(1n+a,b) == True{} : Bool}:
347	  match a b:
348	    case 0n 0n:
349	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(h))
350	    case 0n 1n+b:
351	      zero_le(b)
352	    case 1n+a 0n:
353	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(h))
354	    case 1n+a 1n+b:
355	      strict_follow(a,b,h)
356	
357	# Translate a comparison against a remaining extent to its absolute position.
358	def below_difference(+offset: Nat,+value: Nat,+end: Nat,ordered: {Nat.is_le(offset,end) == True{} : Bool}) ->
359	  {Nat.is_lt(value,Nat.sub(end,offset)) == Nat.is_lt(Nat.add(offset,value),end) : Bool}:
360	  match offset end:
361	    case 0n end:
362	      %Equal.sym(Nat,Nat.sub(end,0n),end,subtract_zero(end)) : {Nat.is_lt(value,_) == Nat.is_lt(value,end) : Bool}
363	      {==}
364	    case 1n+offset 0n:
365	      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))
366	    case 1n+offset 1n+end: below_difference(offset,value,end,ordered)
367	
368	# Two opposite bounds identify a natural number.
369	def antisymmetric(+left: Nat,+right: Nat,forward: {Nat.is_le(left,right) == True{} : Bool},backward: {Nat.is_le(right,left) == True{} : Bool}) -> {left == right : Nat}:
370	  match left right:
371	    case 0n 0n: {==}
372	    case 0n 1n+right: Empty.absurd({0n == 1n+right : Nat},WordEncoding.false_true(backward))
373	    case 1n+left 0n: Empty.absurd({1n+left == 0n : Nat},WordEncoding.false_true(forward))
374	    case 1n+ +left 1n+ +right:
375	      Equal.cong(Nat,Nat,value => 1n+value,left,right,antisymmetric(left,right,forward,backward))