proofs/nat_order.bend

stelliferous@0.0.2.0 · 375 lines · 46 definitions

1import Base
2import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
3
4import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
5import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
6import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
7
8def 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
15def 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
21def 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
30def subtract_zero(+value: Nat) -> {Nat.sub(value,0n) == value : Nat}:
31  match value:
32    case 0n: {==}
33    case 1n+rest: {==}
34
35def zero_subtract(value: Nat) -> {Nat.sub(0n,value) == 0n : Nat}:
36  match value:
37    case 0n: {==}
38    case 1n+rest: {==}
39
40def 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
45def 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
52def 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
57def 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
64def 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
71def 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
82type UpperBound<-value: Nat,-limit: Nat> is Data:
83  Before{inside: {Nat.is_lt(value,limit) == True{} : Bool}}
84  At{equal: {value == limit : Nat}}
85
86def 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
91def 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
98def 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
105def 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
111def 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
114def 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
119def 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
126def zero_le(+a: Nat) -> {Nat.is_le(0n,a) == True{} : Bool}:
127  match a:
128    case 0n:
129      {==}
130    case 1n+p:
131      {==}
132
133def 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
140def 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
146def 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
152def 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
158def 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
169def 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
185def 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
192def 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
196def 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
202def 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
213def 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
225def 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
236def 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
240def 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
251def 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
267def 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
272def 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
281def 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
297def 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
302def 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.
306def 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.
318def 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.
332def 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.
346def 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.
358def 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.
369def 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))