proofs/math/typed/natcmp.bend

bend-collections-laws-math@1.0.0.0 · 145 lines · 21 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
7import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
8import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
9
10# Comparisons of naturals (Nat.cmp), lexicographic pairs and common scales:
11# the order facts behind the f64 comparison and rounding proofs.
12
13def absurd_tf(-T: Type, +h: {False{} == True{} : Bool}) -> T:
14  Empty.absurd(T, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
15
16def lex(c: Cmp, d: Cmp) -> Cmp:
17  match c:
18    case LT{}:
19      LT{}
20    case EQ{}:
21      d
22    case GT{}:
23      GT{}
24
25def cmp_dbl(+a: Nat, +b: Nat) -> {Nat.cmp(Nat.double(a), Nat.double(b)) == Nat.cmp(a, b) : Cmp}:
26  match a b:
27    case 0n 0n:
28      {==}
29    case 0n 1n+ +bp:
30      {==}
31    case 1n+ +ap 0n:
32      {==}
33    case 1n+ +ap 1n+ +bp:
34      cmp_dbl(ap, bp)
35
36def cmp_shift(+k: Nat, +a: Nat, +b: Nat) -> {Nat.cmp(C.shift(k, a), C.shift(k, b)) == Nat.cmp(a, b) : Cmp}:
37  match k:
38    case 0n:
39      {==}
40    case 1n+ +p:
41      Equal.trans(Cmp, Nat.cmp(Nat.double(C.shift(p, a)), Nat.double(C.shift(p, b))), Nat.cmp(C.shift(p, a), C.shift(p, b)), Nat.cmp(a, b), cmp_dbl(C.shift(p, a), C.shift(p, b)), cmp_shift(p, a, b))
42
43def cmp_add(+d: Nat, +a: Nat, +b: Nat) -> {Nat.cmp(Nat.add(d, a), Nat.add(d, b)) == Nat.cmp(a, b) : Cmp}:
44  match d:
45    case 0n:
46      {==}
47    case 1n+ +dp:
48      cmp_add(dp, a, b)
49
50def cmp_addr(+a: Nat, +b: Nat, +s: Nat) -> {Nat.cmp(Nat.add(a, s), Nat.add(b, s)) == Nat.cmp(a, b) : Cmp}:
51  +e1 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, Nat.add(b, s)), Nat.add(a, s), Nat.add(s, a), NA.add_comm(a, s))
52  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(Nat.add(s, a), z), Nat.add(b, s), Nat.add(s, b), NA.add_comm(b, s))
53  Equal.trans(Cmp, Nat.cmp(Nat.add(a, s), Nat.add(b, s)), Nat.cmp(Nat.add(s, a), Nat.add(b, s)), Nat.cmp(a, b), e1, Equal.trans(Cmp, Nat.cmp(Nat.add(s, a), Nat.add(b, s)), Nat.cmp(Nat.add(s, a), Nat.add(s, b)), Nat.cmp(a, b), e2, cmp_add(s, a, b)))
54
55def lt_c(+c: Cmp, +h: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
56  match c:
57    case LT{}:
58      {==}
59    case EQ{}:
60      absurd_tf({EQ{} == LT{} : Cmp}, h)
61    case GT{}:
62      absurd_tf({GT{} == LT{} : Cmp}, h)
63
64def eq_c(+c: Cmp, +h: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
65  match c:
66    case LT{}:
67      absurd_tf({LT{} == EQ{} : Cmp}, h)
68    case EQ{}:
69      {==}
70    case GT{}:
71      absurd_tf({GT{} == EQ{} : Cmp}, h)
72
73def cmp_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.cmp(a, b) == LT{} : Cmp}:
74  lt_c(Nat.cmp(a, b), h)
75
76def cmp_flip(+a: Nat, +b: Nat) -> {SF.flip(Nat.cmp(a, b)) == Nat.cmp(b, a) : Cmp}:
77  match a b:
78    case 0n 0n:
79      {==}
80    case 0n 1n+ +bp:
81      {==}
82    case 1n+ +ap 0n:
83      {==}
84    case 1n+ +ap 1n+ +bp:
85      cmp_flip(ap, bp)
86
87def cmp_gt(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.cmp(a, b) == GT{} : Cmp}:
88  Equal.trans(Cmp, Nat.cmp(a, b), SF.flip(Nat.cmp(b, a)), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(b, a)), Nat.cmp(a, b), cmp_flip(b, a)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(b, a), LT{}, cmp_lt(b, a, h)))
89
90def cmp_refl(+a: Nat) -> {Nat.cmp(a, a) == EQ{} : Cmp}:
91  eq_c(Nat.cmp(a, a), N.is_eq_refl(a))
92
93def eq_of_cmp(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
94  N.eq_from_is_eq(a, b, Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(a, b), EQ{}, h))
95
96def lt_of_cmp(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == LT{} : Cmp}) -> {Nat.is_lt(a, b) == True{} : Bool}:
97  Equal.cong(Cmp, Bool, t => Cmp.is_lt(t), Nat.cmp(a, b), LT{}, h)
98
99def lt_of_gt(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == GT{} : Cmp}) -> {Nat.is_lt(b, a) == True{} : Bool}:
100  lt_of_cmp(b, a, Equal.trans(Cmp, Nat.cmp(b, a), SF.flip(Nat.cmp(a, b)), LT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(a, b)), Nat.cmp(b, a), cmp_flip(a, b)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(a, b), GT{}, h)))
101
102# two limbs compare lexicographically
103def cl_c(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(y1, y2) == c : Cmp}) -> {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == lex(c, Nat.cmp(x1, x2)) : Cmp}:
104  match c:
105    case LT{}:
106      cmp_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), WW.lt_hi(k, x1, y1, x2, y2, hx1, lt_of_cmp(y1, y2, hc)))
107    case GT{}:
108      cmp_gt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), WW.lt_hi(k, x2, y2, x1, y1, hx2, lt_of_gt(y1, y2, hc)))
109    case EQ{}:
110      L.subst(Nat, z => {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == Nat.cmp(x1, x2) : Cmp}, y1, y2, eq_of_cmp(y1, y2, hc), cmp_addr(x1, x2, C.shift(k, y1)))
111
112def cmp_limbs(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}) -> {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == lex(Nat.cmp(y1, y2), Nat.cmp(x1, x2)) : Cmp}:
113  cl_c(k, x1, y1, x2, y2, hx1, hx2, Nat.cmp(y1, y2), {==})
114
115def min_le_l(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}:
116  match a b:
117    case 0n _:
118      {==}
119    case 1n+ +ap 0n:
120      {==}
121    case 1n+ +ap 1n+ +bp:
122      min_le_l(ap, bp)
123
124def min_le_r(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}:
125  match a b:
126    case 0n _:
127      N.zero_le(b)
128    case 1n+ +ap 0n:
129      {==}
130    case 1n+ +ap 1n+ +bp:
131      min_le_r(ap, bp)
132
133# shift(a, p) = shift(m, shift(a - m, p)) for m <= a
134def sh_split(+a: Nat, +m: Nat, +p: Nat, +h: {Nat.is_le(m, a) == True{} : Bool}) -> {C.shift(a, p) == C.shift(m, C.shift(Nat.sub(a, m), p)) : Nat}:
135  Equal.trans(Nat, C.shift(a, p), C.shift(Nat.add(m, Nat.sub(a, m)), p), C.shift(m, C.shift(Nat.sub(a, m), p)), Equal.cong(Nat, Nat, z => C.shift(z, p), a, Nat.add(m, Nat.sub(a, m)), Equal.sym(Nat, Nat.add(m, Nat.sub(a, m)), a, N.sub_add(a, m, h))), WW.shift_comp(m, Nat.sub(a, m), p))
136
137# a common scale 2^min cancels
138def cmp_min(+a: Nat, +b: Nat, +p: Nat, +q: Nat) -> {Nat.cmp(C.shift(Nat.sub(a, Nat.min(a, b)), p), C.shift(Nat.sub(b, Nat.min(a, b)), q)) == Nat.cmp(C.shift(a, p), C.shift(b, q)) : Cmp}:
139  +m = Nat.min(a, b)
140  +X0 = C.shift(Nat.sub(a, m), p)
141  +Y0 = C.shift(Nat.sub(b, m), q)
142  +e1 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(b, q)), C.shift(a, p), C.shift(m, X0), sh_split(a, m, p, min_le_l(a, b)))
143  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(C.shift(m, X0), z), C.shift(b, q), C.shift(m, Y0), sh_split(b, m, q, min_le_r(a, b)))
144  Equal.sym(Cmp, Nat.cmp(C.shift(a, p), C.shift(b, q)), Nat.cmp(X0, Y0), Equal.trans(Cmp, Nat.cmp(C.shift(a, p), C.shift(b, q)), Nat.cmp(C.shift(m, X0), C.shift(b, q)), Nat.cmp(X0, Y0), e1, Equal.trans(Cmp, Nat.cmp(C.shift(m, X0), C.shift(b, q)), Nat.cmp(C.shift(m, X0), C.shift(m, Y0)), Nat.cmp(X0, Y0), e2, cmp_shift(m, X0, Y0))))
145