proofs/u32_comparison.bend
stelliferous@0.0.3.0 · 110 lines · 0 definitions
1import Base
2
3def digit(bit: Bool,n: Nat) -> Nat:
4 match bit:
5 case False{}:
6 Nat.double(n)
7 case True{}:
8 1n+Nat.double(n)
9
10law digits:
11 for +a: Nat
12 for +b: Nat
13 for +ab: Bool
14 for +bb: Bool
15 {Nat.cmp(digit(ab,a),digit(bb,b)) == Word.cmp.fin(ab,bb,Nat.cmp(a,b)) : Cmp}
16def digits(a,b,ab,bb):
17 match a b ab bb:
18 case 0n 0n False{} False{}:
19 {==}
20 case 0n 0n False{} True{}:
21 {==}
22 case 0n 0n True{} False{}:
23 {==}
24 case 0n 0n True{} True{}:
25 {==}
26 case 0n 1n+bp False{} False{}:
27 {==}
28 case 0n 1n+bp False{} True{}:
29 {==}
30 case 0n 1n+bp True{} False{}:
31 {==}
32 case 0n 1n+bp True{} True{}:
33 {==}
34 case 1n+ap 0n False{} False{}:
35 {==}
36 case 1n+ap 0n False{} True{}:
37 {==}
38 case 1n+ap 0n True{} False{}:
39 {==}
40 case 1n+ap 0n True{} True{}:
41 {==}
42 case 1n+ap 1n+bp False{} False{}:
43 digits(ap,bp,False{},False{})
44 case 1n+ap 1n+bp False{} True{}:
45 digits(ap,bp,False{},True{})
46 case 1n+ap 1n+bp True{} False{}:
47 digits(ap,bp,True{},False{})
48 case 1n+ap 1n+bp True{} True{}:
49 digits(ap,bp,True{},True{})
50
51law word:
52 for +n: Nat
53 for +a: Word(n)
54 for +b: Word(n)
55 {Word.cmp(n,a,b) == Nat.cmp(Word.to_nat(n,a),Word.to_nat(n,b)) : Cmp}
56def word(n,a,b):
57 match n:
58 case 0n:
59 {==}
60 case 1n+ +p:
61 match a b:
62 case WCon{False{},+at} WCon{False{},+bt}:
63 %Equal.sym(Cmp,Nat.cmp(digit(False{},Word.to_nat(p,at)),digit(False{},Word.to_nat(p,bt))),Word.cmp.fin(False{},False{},
64 Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),False{},False{})) : {Word.cmp.fin(False{},
65 False{},Word.cmp(p,at,bt)) == _ : Cmp}
66 %word(p,at,bt) : {Word.cmp.fin(False{},False{},Word.cmp(p,at,bt)) == Word.cmp.fin(False{},False{},_) : Cmp}
67 {==}
68 case WCon{False{},+at} WCon{True{},+bt}:
69 %Equal.sym(Cmp,Nat.cmp(digit(False{},Word.to_nat(p,at)),digit(True{},Word.to_nat(p,bt))),Word.cmp.fin(False{},True{},
70 Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),False{},True{})) : {Word.cmp.fin(False{},
71 True{},Word.cmp(p,at,bt)) == _ : Cmp}
72 %word(p,at,bt) : {Word.cmp.fin(False{},True{},Word.cmp(p,at,bt)) == Word.cmp.fin(False{},True{},_) : Cmp}
73 {==}
74 case WCon{True{},+at} WCon{False{},+bt}:
75 %Equal.sym(Cmp,Nat.cmp(digit(True{},Word.to_nat(p,at)),digit(False{},Word.to_nat(p,bt))),Word.cmp.fin(True{},False{},
76 Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),True{},False{})) : {Word.cmp.fin(True{},
77 False{},Word.cmp(p,at,bt)) == _ : Cmp}
78 %word(p,at,bt) : {Word.cmp.fin(True{},False{},Word.cmp(p,at,bt)) == Word.cmp.fin(True{},False{},_) : Cmp}
79 {==}
80 case WCon{True{},+at} WCon{True{},+bt}:
81 %Equal.sym(Cmp,Nat.cmp(digit(True{},Word.to_nat(p,at)),digit(True{},Word.to_nat(p,bt))),Word.cmp.fin(True{},True{},
82 Nat.cmp(Word.to_nat(p,at),Word.to_nat(p,bt))),digits(Word.to_nat(p,at),Word.to_nat(p,bt),True{},True{})) : {Word.cmp.fin(True{},
83 True{},Word.cmp(p,at,bt)) == _ : Cmp}
84 %word(p,at,bt) : {Word.cmp.fin(True{},True{},Word.cmp(p,at,bt)) == Word.cmp.fin(True{},True{},_) : Cmp}
85 {==}
86
87law uint:
88 for +a: U32
89 for +b: U32
90 {U32.cmp(a,b) == Nat.cmp(U32.to_nat(a),U32.to_nat(b)) : Cmp}
91def uint(a,b):
92 match a b:
93 case U32{x} U32{y}:
94 word(32n,x,y)
95
96def lt(+a: U32,+b: U32) -> {U32.is_lt(a,b) == Nat.is_lt(U32.to_nat(a),U32.to_nat(b)) : Bool}:
97 %uint(a,b) : {Cmp.is_lt(U32.cmp(a,b)) == Cmp.is_lt(_) : Bool}
98 {==}
99
100def le(+a: U32,+b: U32) -> {U32.is_le(a,b) == Nat.is_le(U32.to_nat(a),U32.to_nat(b)) : Bool}:
101 %uint(a,b) : {Cmp.is_le(U32.cmp(a,b)) == Cmp.is_le(_) : Bool}
102 {==}
103
104def eq(+a: U32,+b: U32) -> {U32.is_eq(a,b) == Nat.is_eq(U32.to_nat(a),U32.to_nat(b)) : Bool}:
105 %uint(a,b) : {Cmp.is_eq(U32.cmp(a,b)) == Cmp.is_eq(_) : Bool}
106 {==}
107
108def ge(+a: U32,+b: U32) -> {U32.is_ge(a,b) == Nat.is_ge(U32.to_nat(a),U32.to_nat(b)) : Bool}:
109 %uint(a,b) : {Cmp.is_ge(U32.cmp(a,b)) == Cmp.is_ge(_) : Bool}
110 {==}