PROOF_order.bend

bend-osdev-u32@0.1.0.0 · 537 lines · 58 definitions

1# Proofs of LAWS_order.bend: the order of Nat by induction on Base's unary
2# Nat, and that of Word(n) by induction over the bits, compared from the top
3# bit down (Word.cmp.fin); U32's is Word(32)'s. The lemmas on Bool, Cmp and
4# words are those bend-osdev-maple, -timerqueue and -itree proved for their
5# own use (proof_order.bend), now proved here once.
6import Base
7import bend-osdev-u32@0.1.0.0/LAWS_order.bend as Laws
8
9# Contradictions
10
11def ab.bool(b: Bool) -> Type:
12  match b:
13    case True{}:
14      Unit
15    case False{}:
16      Empty
17
18def ab.tf(+e: {True{} == False{} : Bool}) -> Empty:
19  %e : ab.bool(_)
20  Unit{}
21
22def ab.ft(+e: {False{} == True{} : Bool}) -> Empty:
23  %Equal.sym(Bool, False{}, True{}, e) : ab.bool(_)
24  Unit{}
25
26def ab.is_lt(c: Cmp) -> Type:
27  match c:
28    case LT{}:
29      Unit
30    case o:
31      Empty
32
33def ab.is_eq(c: Cmp) -> Type:
34  match c:
35    case EQ{}:
36      Unit
37    case o:
38      Empty
39
40def ab.is_gt(c: Cmp) -> Type:
41  match c:
42    case GT{}:
43      Unit
44    case o:
45      Empty
46
47def ab.eq_lt(+e: {EQ{} == LT{} : Cmp}) -> Empty:
48  %e : ab.is_eq(_)
49  Unit{}
50
51def ab.gt_lt(+e: {GT{} == LT{} : Cmp}) -> Empty:
52  %e : ab.is_gt(_)
53  Unit{}
54
55def ab.lt_eq(+e: {LT{} == EQ{} : Cmp}) -> Empty:
56  %e : ab.is_lt(_)
57  Unit{}
58
59def ab.gt_eq(+e: {GT{} == EQ{} : Cmp}) -> Empty:
60  %e : ab.is_gt(_)
61  Unit{}
62
63# Cmp
64
65def cm.flip(c: Cmp) -> Cmp:
66  match c:
67    case LT{}:
68      GT{}
69    case EQ{}:
70      EQ{}
71    case GT{}:
72      LT{}
73
74def cm.lt_of(c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
75  match c:
76    case LT{}:
77      {==}
78    case EQ{}:
79      Empty.absurd({EQ{} == LT{} : Cmp}, ab.ft(e))
80    case GT{}:
81      Empty.absurd({GT{} == LT{} : Cmp}, ab.ft(e))
82
83def cm.is_lt_of(-c: Cmp, +e: {c == LT{} : Cmp}) -> {Cmp.is_lt(c) == True{} : Bool}:
84  %Equal.sym(Cmp, c, LT{}, e) : {Cmp.is_lt(_) == True{} : Bool}
85  {==}
86
87def cm.le_of_lt(c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}:
88  match c:
89    case LT{}:
90      {==}
91    case EQ{}:
92      Empty.absurd({True{} == True{} : Bool}, ab.ft(e))
93    case GT{}:
94      Empty.absurd({False{} == True{} : Bool}, ab.ft(e))
95
96# is_le(c) and not is_lt(c): c is EQ
97def cm.eq_of_le(c: Cmp, +e: {Cmp.is_le(c) == True{} : Bool}, +f: {Cmp.is_lt(c) == False{} : Bool}) -> {c == EQ{} : Cmp}:
98  match c:
99    case LT{}:
100      Empty.absurd({LT{} == EQ{} : Cmp}, ab.tf(f))
101    case EQ{}:
102      {==}
103    case GT{}:
104      Empty.absurd({GT{} == EQ{} : Cmp}, ab.ft(e))
105
106# flipping turns not-less into at-most and the other way
107def cm.le_flip(c: Cmp, +e: {Cmp.is_lt(c) == False{} : Bool}) -> {Cmp.is_le(cm.flip(c)) == True{} : Bool}:
108  match c:
109    case LT{}:
110      Empty.absurd({False{} == True{} : Bool}, ab.tf(e))
111    case EQ{}:
112      {==}
113    case GT{}:
114      {==}
115
116def cm.lt_flip(c: Cmp, +e: {Cmp.is_le(c) == False{} : Bool}) -> {Cmp.is_lt(cm.flip(c)) == True{} : Bool}:
117  match c:
118    case LT{}:
119      Empty.absurd({False{} == True{} : Bool}, ab.tf(e))
120    case EQ{}:
121      Empty.absurd({False{} == True{} : Bool}, ab.tf(e))
122    case GT{}:
123      {==}
124
125def cm.not_le_flip(c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(cm.flip(c)) == False{} : Bool}:
126  match c:
127    case LT{}:
128      {==}
129    case EQ{}:
130      Empty.absurd({True{} == False{} : Bool}, ab.ft(e))
131    case GT{}:
132      Empty.absurd({True{} == False{} : Bool}, ab.ft(e))
133
134def cm.not_lt_flip(c: Cmp, +e: {Cmp.is_le(c) == True{} : Bool}) -> {Cmp.is_lt(cm.flip(c)) == False{} : Bool}:
135  match c:
136    case LT{}:
137      {==}
138    case EQ{}:
139      {==}
140    case GT{}:
141      Empty.absurd({True{} == False{} : Bool}, ab.ft(e))
142
143# Words: Base's order on Word(n), compared from the top bit down
144
145def wd.fin_refl(x: Bool) -> {Word.cmp.fin(x, x, EQ{}) == EQ{} : Cmp}:
146  match x:
147    case True{}:
148      {==}
149    case False{}:
150      {==}
151
152def wd.refl(n: Nat, a: Word(n)) -> {Word.cmp(n, a, a) == EQ{} : Cmp}:
153  match n:
154    case 0n:
155      {==}
156    case 1n+ +p:
157      match a:
158        case WCon{+x, +at}:
159          %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, wd.refl(p, at)) : {Word.cmp.fin(x, x, _) == EQ{} : Cmp}
160          wd.fin_refl(x)
161
162def wd.fin_eq_tail(c: Cmp, -x: Bool, -y: Bool, +e: {Word.cmp.fin(x, y, c) == EQ{} : Cmp}) -> {c == EQ{} : Cmp}:
163  match c:
164    case LT{}:
165      Empty.absurd({LT{} == EQ{} : Cmp}, ab.lt_eq(e))
166    case EQ{}:
167      {==}
168    case GT{}:
169      Empty.absurd({GT{} == EQ{} : Cmp}, ab.gt_eq(e))
170
171def wd.bool_eq(x: Bool, y: Bool, +e: {Bool.cmp(x, y) == EQ{} : Cmp}) -> {x == y : Bool}:
172  match x y:
173    case False{} False{}:
174      {==}
175    case False{} True{}:
176      Empty.absurd({False{} == True{} : Bool}, ab.lt_eq(e))
177    case True{} False{}:
178      Empty.absurd({True{} == False{} : Bool}, ab.gt_eq(e))
179    case True{} True{}:
180      {==}
181
182def wd.fin_eq_head(c: Cmp, x: Bool, y: Bool, +e: {Word.cmp.fin(x, y, c) == EQ{} : Cmp}) -> {x == y : Bool}:
183  match c:
184    case LT{}:
185      Empty.absurd({x == y : Bool}, ab.lt_eq(e))
186    case EQ{}:
187      wd.bool_eq(x, y, e)
188    case GT{}:
189      Empty.absurd({x == y : Bool}, ab.gt_eq(e))
190
191def wd.eq(n: Nat, a: Word(n), b: Word(n), +e: {Word.cmp(n, a, b) == EQ{} : Cmp}) -> {a == b : Word(n)}:
192  match n:
193    case 0n:
194      match a b:
195        case WNil{} WNil{}:
196          {==}
197    case 1n+ +p:
198      match a b:
199        case WCon{+x, +at} WCon{+y, +bt}:
200          %wd.eq(p, at, bt, wd.fin_eq_tail(Word.cmp(p, at, bt), x, y, e)) : {WCon{x, at} == WCon{y, _} : Word(1n+p)}
201          %wd.fin_eq_head(Word.cmp(p, at, bt), x, y, e) : {WCon{x, at} == WCon{_, at} : Word(1n+p)}
202          {==}
203
204def wd.bool_flip(x: Bool, y: Bool) -> {Bool.cmp(y, x) == cm.flip(Bool.cmp(x, y)) : Cmp}:
205  match x y:
206    case False{} False{}:
207      {==}
208    case False{} True{}:
209      {==}
210    case True{} False{}:
211      {==}
212    case True{} True{}:
213      {==}
214
215def wd.fin_flip(c: Cmp, x: Bool, y: Bool) -> {Word.cmp.fin(y, x, cm.flip(c)) == cm.flip(Word.cmp.fin(x, y, c)) : Cmp}:
216  match c:
217    case LT{}:
218      {==}
219    case EQ{}:
220      wd.bool_flip(x, y)
221    case GT{}:
222      {==}
223
224def wd.flip(n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, b, a) == cm.flip(Word.cmp(n, a, b)) : Cmp}:
225  match n:
226    case 0n:
227      {==}
228    case 1n+ +p:
229      match a b:
230        case WCon{+x, +at} WCon{+y, +bt}:
231          %Equal.sym(Cmp, Word.cmp(p, bt, at), cm.flip(Word.cmp(p, at, bt)), wd.flip(p, at, bt)) : {Word.cmp.fin(y, x, _) == cm.flip(Word.cmp.fin(x, y, Word.cmp(p, at, bt))) : Cmp}
232          wd.fin_flip(Word.cmp(p, at, bt), x, y)
233
234def wd.bool_trans(x: Bool, y: Bool, z: Bool, +h1: {Bool.cmp(x, y) == LT{} : Cmp}, +h2: {Bool.cmp(y, z) == LT{} : Cmp}) -> {Bool.cmp(x, z) == LT{} : Cmp}:
235  match x y z:
236    case False{} False{} z:
237      Empty.absurd({Bool.cmp(False{}, z) == LT{} : Cmp}, ab.eq_lt(h1))
238    case False{} True{} False{}:
239      Empty.absurd({EQ{} == LT{} : Cmp}, ab.gt_lt(h2))
240    case False{} True{} True{}:
241      Empty.absurd({LT{} == LT{} : Cmp}, ab.eq_lt(h2))
242    case True{} False{} z:
243      Empty.absurd({Bool.cmp(True{}, z) == LT{} : Cmp}, ab.gt_lt(h1))
244    case True{} True{} z:
245      Empty.absurd({Bool.cmp(True{}, z) == LT{} : Cmp}, ab.eq_lt(h1))
246
247def wd.fin_trans(c1: Cmp, c2: Cmp, +p: Nat, +x: Bool, +y: Bool, +z: Bool, +at: Word(p), +bt: Word(p), +ct: Word(p), +e1: {Word.cmp(p, at, bt) == c1 : Cmp}, +e2: {Word.cmp(p, bt, ct) == c2 : Cmp}, +h1: {Word.cmp.fin(x, y, c1) == LT{} : Cmp}, +h2: {Word.cmp.fin(y, z, c2) == LT{} : Cmp}, ih: {Word.cmp(p, at, bt) == LT{} : Cmp} -> {Word.cmp(p, bt, ct) == LT{} : Cmp} -> {Word.cmp(p, at, ct) == LT{} : Cmp}) -> {Word.cmp.fin(x, z, Word.cmp(p, at, ct)) == LT{} : Cmp}:
248  match c1 c2:
249    case LT{} LT{}:
250      %Equal.sym(Cmp, Word.cmp(p, at, ct), LT{}, ih(e1, e2)) : {Word.cmp.fin(x, z, _) == LT{} : Cmp}
251      {==}
252    case LT{} EQ{}:
253      %wd.eq(p, bt, ct, e2) : {Word.cmp.fin(x, z, Word.cmp(p, at, _)) == LT{} : Cmp}
254      %Equal.sym(Cmp, Word.cmp(p, at, bt), LT{}, e1) : {Word.cmp.fin(x, z, _) == LT{} : Cmp}
255      {==}
256    case EQ{} LT{}:
257      %Equal.sym(Word(p), at, bt, wd.eq(p, at, bt, e1)) : {Word.cmp.fin(x, z, Word.cmp(p, _, ct)) == LT{} : Cmp}
258      %Equal.sym(Cmp, Word.cmp(p, bt, ct), LT{}, e2) : {Word.cmp.fin(x, z, _) == LT{} : Cmp}
259      {==}
260    case EQ{} EQ{}:
261      %Equal.trans(Word(p), at, bt, ct, wd.eq(p, at, bt, e1), wd.eq(p, bt, ct, e2)) : {Word.cmp.fin(x, z, Word.cmp(p, at, _)) == LT{} : Cmp}
262      %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, wd.refl(p, at)) : {Word.cmp.fin(x, z, _) == LT{} : Cmp}
263      wd.bool_trans(x, y, z, h1, h2)
264    case GT{} c2:
265      Empty.absurd({Word.cmp.fin(x, z, Word.cmp(p, at, ct)) == LT{} : Cmp}, ab.gt_lt(h1))
266    case c1 GT{}:
267      Empty.absurd({Word.cmp.fin(x, z, Word.cmp(p, at, ct)) == LT{} : Cmp}, ab.gt_lt(h2))
268
269def wd.lt_trans(n: Nat, a: Word(n), b: Word(n), c: Word(n), +h1: {Word.cmp(n, a, b) == LT{} : Cmp}, +h2: {Word.cmp(n, b, c) == LT{} : Cmp}) -> {Word.cmp(n, a, c) == LT{} : Cmp}:
270  match n:
271    case 0n:
272      Empty.absurd({Word.cmp(0n, a, c) == LT{} : Cmp}, ab.eq_lt(h1))
273    case 1n+ +p:
274      match a b c:
275        case WCon{+x, +at} WCon{+y, +bt} WCon{+z, +ct}:
276          wd.fin_trans(Word.cmp(p, at, bt), Word.cmp(p, bt, ct), p, x, y, z, at, bt, ct, {==}, {==}, h1, h2, u => w => wd.lt_trans(p, at, bt, ct, u, w))
277
278# U32's order, as Bools
279
280def ult(+a: U32, +b: U32) -> Bool:
281  Cmp.is_lt(U32.cmp(a, b))
282
283def ule(+a: U32, +b: U32) -> Bool:
284  Cmp.is_le(U32.cmp(a, b))
285
286def u.refl(a: U32) -> {U32.cmp(a, a) == EQ{} : Cmp}:
287  match a:
288    case U32{+w}:
289      wd.refl(32n, w)
290
291def u.eq(a: U32, b: U32, +e: {U32.cmp(a, b) == EQ{} : Cmp}) -> {a == b : U32}:
292  match a b:
293    case U32{+x} U32{+y}:
294      %wd.eq(32n, x, y, e) : {U32{x} == U32{_} : U32}
295      {==}
296
297def u.flip(a: U32, b: U32) -> {U32.cmp(b, a) == cm.flip(U32.cmp(a, b)) : Cmp}:
298  match a b:
299    case U32{+x} U32{+y}:
300      wd.flip(32n, x, y)
301
302def u.cmp_lt_trans(a: U32, b: U32, c: U32, +h1: {U32.cmp(a, b) == LT{} : Cmp}, +h2: {U32.cmp(b, c) == LT{} : Cmp}) -> {U32.cmp(a, c) == LT{} : Cmp}:
303  match a b c:
304    case U32{+x} U32{+y} U32{+z}:
305      wd.lt_trans(32n, x, y, z, h1, h2)
306
307def u.le_refl(+a: U32) -> {ule(a, a) == True{} : Bool}:
308  %Equal.sym(Cmp, U32.cmp(a, a), EQ{}, u.refl(a)) : {Cmp.is_le(_) == True{} : Bool}
309  {==}
310
311def ab.lt_eqc(c: Cmp, +h: {c == EQ{} : Cmp}, +e: {Cmp.is_lt(c) == True{} : Bool}) -> Empty:
312  match c:
313    case LT{}:
314      ab.lt_eq(h)
315    case EQ{}:
316      ab.ft(e)
317    case GT{}:
318      ab.gt_eq(h)
319
320def u.lt_irrefl(+a: U32, +e: {ult(a, a) == True{} : Bool}) -> Empty:
321  ab.lt_eqc(U32.cmp(a, a), u.refl(a), e)
322
323def u.le_of_lt(+a: U32, +b: U32, +e: {ult(a, b) == True{} : Bool}) -> {ule(a, b) == True{} : Bool}:
324  cm.le_of_lt(U32.cmp(a, b), e)
325
326def u.lt_trans(+a: U32, +b: U32, +c: U32, +h1: {ult(a, b) == True{} : Bool}, +h2: {ult(b, c) == True{} : Bool}) -> {ult(a, c) == True{} : Bool}:
327  cm.is_lt_of(U32.cmp(a, c), u.cmp_lt_trans(a, b, c, cm.lt_of(U32.cmp(a, b), h1), cm.lt_of(U32.cmp(b, c), h2)))
328
329def u.not_lt(+a: U32, +b: U32, +e: {ult(a, b) == False{} : Bool}) -> {ule(b, a) == True{} : Bool}:
330  %Equal.sym(Cmp, U32.cmp(b, a), cm.flip(U32.cmp(a, b)), u.flip(a, b)) : {Cmp.is_le(_) == True{} : Bool}
331  cm.le_flip(U32.cmp(a, b), e)
332
333def u.not_le(+a: U32, +b: U32, +e: {ule(a, b) == False{} : Bool}) -> {ult(b, a) == True{} : Bool}:
334  %Equal.sym(Cmp, U32.cmp(b, a), cm.flip(U32.cmp(a, b)), u.flip(a, b)) : {Cmp.is_lt(_) == True{} : Bool}
335  cm.lt_flip(U32.cmp(a, b), e)
336
337# a < b: not b <= a
338def u.lt_not_le(+a: U32, +b: U32, +e: {ult(a, b) == True{} : Bool}) -> {ule(b, a) == False{} : Bool}:
339  %Equal.sym(Cmp, U32.cmp(b, a), cm.flip(U32.cmp(a, b)), u.flip(a, b)) : {Cmp.is_le(_) == False{} : Bool}
340  cm.not_le_flip(U32.cmp(a, b), e)
341
342# a <= b: not b < a
343def u.le_not_lt(+a: U32, +b: U32, +e: {ule(a, b) == True{} : Bool}) -> {ult(b, a) == False{} : Bool}:
344  %Equal.sym(Cmp, U32.cmp(b, a), cm.flip(U32.cmp(a, b)), u.flip(a, b)) : {Cmp.is_lt(_) == False{} : Bool}
345  cm.not_lt_flip(U32.cmp(a, b), e)
346
347def u.le_lt.go(c1: Cmp, +a: U32, +b: U32, +c: U32, +e1: {U32.cmp(a, b) == c1 : Cmp}, +h1: {Cmp.is_le(c1) == True{} : Bool}, +h2: {U32.cmp(b, c) == LT{} : Cmp}) -> {U32.cmp(a, c) == LT{} : Cmp}:
348  match c1:
349    case LT{}:
350      u.cmp_lt_trans(a, b, c, e1, h2)
351    case EQ{}:
352      %Equal.sym(U32, a, b, u.eq(a, b, e1)) : {U32.cmp(_, c) == LT{} : Cmp}
353      h2
354    case GT{}:
355      Empty.absurd({U32.cmp(a, c) == LT{} : Cmp}, ab.ft(h1))
356
357# a <= b < c
358def u.le_lt(+a: U32, +b: U32, +c: U32, +h1: {ule(a, b) == True{} : Bool}, +h2: {ult(b, c) == True{} : Bool}) -> {ult(a, c) == True{} : Bool}:
359  cm.is_lt_of(U32.cmp(a, c), u.le_lt.go(U32.cmp(a, b), a, b, c, {==}, h1, cm.lt_of(U32.cmp(b, c), h2)))
360
361def u.lt_le.go(c2: Cmp, +a: U32, +b: U32, +c: U32, +e2: {U32.cmp(b, c) == c2 : Cmp}, +h1: {U32.cmp(a, b) == LT{} : Cmp}, +h2: {Cmp.is_le(c2) == True{} : Bool}) -> {U32.cmp(a, c) == LT{} : Cmp}:
362  match c2:
363    case LT{}:
364      u.cmp_lt_trans(a, b, c, h1, e2)
365    case EQ{}:
366      %u.eq(b, c, e2) : {U32.cmp(a, _) == LT{} : Cmp}
367      h1
368    case GT{}:
369      Empty.absurd({U32.cmp(a, c) == LT{} : Cmp}, ab.ft(h2))
370
371# a < b <= c
372def u.lt_le(+a: U32, +b: U32, +c: U32, +h1: {ult(a, b) == True{} : Bool}, +h2: {ule(b, c) == True{} : Bool}) -> {ult(a, c) == True{} : Bool}:
373  cm.is_lt_of(U32.cmp(a, c), u.lt_le.go(U32.cmp(b, c), a, b, c, {==}, cm.lt_of(U32.cmp(a, b), h1), h2))
374
375def u.le_le.go(c1: Cmp, +a: U32, +b: U32, +c: U32, +e1: {U32.cmp(a, b) == c1 : Cmp}, +h1: {Cmp.is_le(c1) == True{} : Bool}, +h2: {ule(b, c) == True{} : Bool}) -> {ule(a, c) == True{} : Bool}:
376  match c1:
377    case LT{}:
378      u.le_of_lt(a, c, u.lt_le(a, b, c, cm.is_lt_of(U32.cmp(a, b), e1), h2))
379    case EQ{}:
380      %Equal.sym(U32, a, b, u.eq(a, b, e1)) : {Cmp.is_le(U32.cmp(_, c)) == True{} : Bool}
381      h2
382    case GT{}:
383      Empty.absurd({ule(a, c) == True{} : Bool}, ab.ft(h1))
384
385# a <= b <= c
386def u.le_trans(+a: U32, +b: U32, +c: U32, +h1: {ule(a, b) == True{} : Bool}, +h2: {ule(b, c) == True{} : Bool}) -> {ule(a, c) == True{} : Bool}:
387  u.le_le.go(U32.cmp(a, b), a, b, c, {==}, h1, h2)
388
389# a <= b and b <= a: a == b
390def u.antisym(+a: U32, +b: U32, +h1: {ule(a, b) == True{} : Bool}, +h2: {ule(b, a) == True{} : Bool}) -> {a == b : U32}:
391  u.eq(a, b, cm.eq_of_le(U32.cmp(a, b), h1, u.le_not_lt(b, a, h2)))
392
393# Nat
394
395def nt.le_trans(x: Nat, y: Nat, z: Nat, h1: {Nat.is_le(x, y) == True{} : Bool}, h2: {Nat.is_le(y, z) == True{} : Bool}) -> {Nat.is_le(x, z) == True{} : Bool}:
396  match x y z:
397    case 0n _ _:
398      match z:
399        case 0n:
400          {==}
401        case 1n+zp:
402          {==}
403    case 1n+xp 0n _:
404      Empty.absurd({Nat.is_le(1n+xp, z) == True{} : Bool}, ab.ft(h1))
405    case 1n+xp 1n+yp 0n:
406      Empty.absurd({Nat.is_le(1n+xp, 0n) == True{} : Bool}, ab.ft(h2))
407    case 1n+xp 1n+yp 1n+zp:
408      nt.le_trans(xp, yp, zp, h1, h2)
409
410def nt.lt_trans(x: Nat, y: Nat, z: Nat, h1: {Nat.is_lt(x, y) == True{} : Bool}, h2: {Nat.is_lt(y, z) == True{} : Bool}) -> {Nat.is_lt(x, z) == True{} : Bool}:
411  match x y z:
412    case 0n 0n _:
413      Empty.absurd({Nat.is_lt(0n, z) == True{} : Bool}, ab.ft(h1))
414    case 0n 1n+yp 0n:
415      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, ab.ft(h2))
416    case 0n 1n+yp 1n+zp:
417      {==}
418    case 1n+xp 0n _:
419      Empty.absurd({Nat.is_lt(1n+xp, z) == True{} : Bool}, ab.ft(h1))
420    case 1n+xp 1n+yp 0n:
421      Empty.absurd({Nat.is_lt(1n+xp, 0n) == True{} : Bool}, ab.ft(h2))
422    case 1n+xp 1n+yp 1n+zp:
423      nt.lt_trans(xp, yp, zp, h1, h2)
424
425def nt.lt_le_trans(x: Nat, y: Nat, z: Nat, h1: {Nat.is_lt(x, y) == True{} : Bool}, h2: {Nat.is_le(y, z) == True{} : Bool}) -> {Nat.is_lt(x, z) == True{} : Bool}:
426  match x y z:
427    case 0n 0n _:
428      Empty.absurd({Nat.is_lt(0n, z) == True{} : Bool}, ab.ft(h1))
429    case 0n 1n+yp 0n:
430      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, ab.ft(h2))
431    case 0n 1n+yp 1n+zp:
432      {==}
433    case 1n+xp 0n _:
434      Empty.absurd({Nat.is_lt(1n+xp, z) == True{} : Bool}, ab.ft(h1))
435    case 1n+xp 1n+yp 0n:
436      Empty.absurd({Nat.is_lt(1n+xp, 0n) == True{} : Bool}, ab.ft(h2))
437    case 1n+xp 1n+yp 1n+zp:
438      nt.lt_le_trans(xp, yp, zp, h1, h2)
439
440def nt.le_lt_trans(x: Nat, y: Nat, z: Nat, h1: {Nat.is_le(x, y) == True{} : Bool}, h2: {Nat.is_lt(y, z) == True{} : Bool}) -> {Nat.is_lt(x, z) == True{} : Bool}:
441  match x y z:
442    case 0n 0n 0n:
443      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, ab.ft(h2))
444    case 0n 0n 1n+zp:
445      {==}
446    case 0n 1n+yp 0n:
447      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, ab.ft(h2))
448    case 0n 1n+yp 1n+zp:
449      {==}
450    case 1n+xp 0n _:
451      Empty.absurd({Nat.is_lt(1n+xp, z) == True{} : Bool}, ab.ft(h1))
452    case 1n+xp 1n+yp 0n:
453      Empty.absurd({Nat.is_lt(1n+xp, 0n) == True{} : Bool}, ab.ft(h2))
454    case 1n+xp 1n+yp 1n+zp:
455      nt.le_lt_trans(xp, yp, zp, h1, h2)
456
457def nt.le_add_r(x: Nat, +w: Nat) -> {Nat.is_le(x, Nat.add(x, w)) == True{} : Bool}:
458  match x:
459    case 0n:
460      match w:
461        case 0n:
462          {==}
463        case 1n+wp:
464          {==}
465    case 1n+xp:
466      nt.le_add_r(xp, w)
467
468# The laws
469
470def Laws.nat_le_trans(x, y, z, h1, h2):
471  nt.le_trans(x, y, z, h1, h2)
472
473def Laws.nat_lt_trans(x, y, z, h1, h2):
474  nt.lt_trans(x, y, z, h1, h2)
475
476def Laws.nat_lt_le_trans(x, y, z, h1, h2):
477  nt.lt_le_trans(x, y, z, h1, h2)
478
479def Laws.nat_le_lt_trans(x, y, z, h1, h2):
480  nt.le_lt_trans(x, y, z, h1, h2)
481
482def Laws.nat_le_add_r(x, w):
483  nt.le_add_r(x, w)
484
485def Laws.word_cmp_refl(n, a):
486  wd.refl(n, a)
487
488def Laws.word_cmp_eq(n, a, b, e):
489  wd.eq(n, a, b, e)
490
491def Laws.word_cmp_lt_trans(n, a, b, c, h1, h2):
492  wd.lt_trans(n, a, b, c, h1, h2)
493
494def Laws.u32_cmp_refl(a):
495  u.refl(a)
496
497def Laws.u32_cmp_eq(a, b, e):
498  u.eq(a, b, e)
499
500def Laws.u32_cmp_lt_trans(a, b, c, h1, h2):
501  u.cmp_lt_trans(a, b, c, h1, h2)
502
503def Laws.u32_le_refl(a):
504  u.le_refl(a)
505
506def Laws.u32_lt_irrefl(a, e):
507  u.lt_irrefl(a, e)
508
509def Laws.u32_lt_le(a, b, e):
510  u.le_of_lt(a, b, e)
511
512def Laws.u32_lt_trans(a, b, c, h1, h2):
513  u.lt_trans(a, b, c, h1, h2)
514
515def Laws.u32_le_trans(a, b, c, h1, h2):
516  u.le_trans(a, b, c, h1, h2)
517
518def Laws.u32_lt_le_trans(a, b, c, h1, h2):
519  u.lt_le(a, b, c, h1, h2)
520
521def Laws.u32_le_lt_trans(a, b, c, h1, h2):
522  u.le_lt(a, b, c, h1, h2)
523
524def Laws.u32_le_antisym(a, b, h1, h2):
525  u.antisym(a, b, h1, h2)
526
527def Laws.u32_not_lt(a, b, e):
528  u.not_lt(a, b, e)
529
530def Laws.u32_not_le(a, b, e):
531  u.not_le(a, b, e)
532
533def Laws.u32_lt_not_le(a, b, e):
534  u.lt_not_le(a, b, e)
535
536def Laws.u32_le_not_lt(a, b, e):
537  u.le_not_lt(a, b, e)