proofs/binary_division.bend
stelliferous@0.0.3.0 · 152 lines · 0 definitions
1# Natural-number binary long division, proved against the frozen Base.divmod.
2import Base
3import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
4import stelliferous@0.0.3.0/proofs/binary_digit.bend as BinaryDigit
5import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
6import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
7import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
8import stelliferous@0.0.3.0/proofs/word_multiplication.bend as Multiplication
9import stelliferous@0.0.3.0/proofs/word_subtraction.bend as Subtraction
10import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
11
12type Quotient is Data:
13 Quotient{quotient: Nat,remainder: Nat}
14
15def total(result: Quotient,b: Nat) -> Nat:
16 Quotient{q,r} = result
17 Nat.add(Nat.mul(q,b),r)
18
19def remainder(result: Quotient) -> Nat:
20 Quotient{q,r} = result
21 r
22
23def pair(result: Quotient) -> Nat & Nat:
24 Quotient{q,r} = result
25 (q,r)
26
27def branch(g: Bool,+q: Nat,s: Nat,b: Nat) -> Quotient:
28 match g:
29 case False{}:
30 Quotient{q,s}
31 case True{}:
32 Quotient{1n+q,Nat.sub(s,b)}
33
34def step(bit: Bool,+b: Nat,prev: Quotient) -> Quotient:
35 Quotient{q,r} = prev
36 +s = Comparison.digit(bit,r)
37 branch(Nat.is_ge(s,b),Nat.double(q),s,b)
38
39def go(n: Nat,w: Word(n),+b: Nat) -> Quotient:
40 match n:
41 case 0n:
42 Quotient{0n,0n}
43 case 1n+p:
44 WCon{bit,tail} = w
45 step(bit,b,go(p,tail,b))
46
47def rotate(+a: Nat,+b: Nat,+c: Nat) -> {Nat.add(Nat.add(a,b),c) == Nat.add(b,Nat.add(c,a)) : Nat}:
48 Equal.trans(Nat,Nat.add(Nat.add(a,b),c),Nat.add(a,Nat.add(b,c)),Nat.add(b,Nat.add(c,a)),Addition.associative(a,b,c),Equal.trans(Nat,
49 Nat.add(a,Nat.add(b,c)),Nat.add(Nat.add(b,c),a),Nat.add(b,Nat.add(c,a)),Order.commutative(a,Nat.add(b,c)),Addition.associative(b,c,a)))
50
51def product_right(+a: Nat,+b: Nat) -> {Nat.mul(a,Nat.double(b)) == Nat.double(Nat.mul(a,b)) : Nat}:
52 match a:
53 case 0n:
54 {==}
55 case 1n+ +p:
56 %Equal.sym(Nat,Nat.double(Nat.add(b,Nat.mul(p,b))),Nat.add(Nat.double(b),Nat.double(Nat.mul(p,b))),WordEncoding.double_add(b,Nat.mul(p,
57 b))) : {Nat.add(Nat.double(b),Nat.mul(p,Nat.double(b))) == _ : Nat}
58 %product_right(p,b) : {Nat.add(Nat.double(b),Nat.mul(p,Nat.double(b))) == Nat.add(Nat.double(b),_) : Nat}
59 {==}
60
61def product_double(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.double(Nat.mul(a,b)) : Nat}:
62 %Equal.sym(Nat,Nat.mul(Nat.double(a),b),Nat.mul(a,Nat.double(b)),Multiplication.double_mul(a,b)) : {_ == Nat.double(Nat.mul(a,b)) : Nat}
63 product_right(a,b)
64
65def even_total(+q: Nat,+r: Nat,+b: Nat) -> {Nat.add(Nat.mul(Nat.double(q),b),Nat.double(r)) == Nat.double(Nat.add(Nat.mul(q,b),r)) : Nat}:
66 %Equal.sym(Nat,Nat.mul(Nat.double(q),b),Nat.double(Nat.mul(q,b)),product_double(q,b)) : {Nat.add(_,
67 Nat.double(r)) == Nat.double(Nat.add(Nat.mul(q,b),r)) : Nat}
68 Equal.sym(Nat,Nat.double(Nat.add(Nat.mul(q,b),r)),Nat.add(Nat.double(Nat.mul(q,b)),Nat.double(r)),WordEncoding.double_add(Nat.mul(q,b),r))
69
70def digit_total(+bit: Bool,+q: Nat,+r: Nat,+b: Nat) -> {Nat.add(Nat.mul(Nat.double(q),b),Comparison.digit(bit,r)) == Comparison.digit(bit,
71 Nat.add(Nat.mul(q,b),r)) : Nat}:
72 match bit:
73 case False{}:
74 even_total(q,r,b)
75 case True{}:
76 %Equal.sym(Nat,Nat.add(Nat.mul(Nat.double(q),b),1n+Nat.double(r)),1n+Nat.add(Nat.mul(Nat.double(q),b),Nat.double(r)),
77 Addition.successor_right(Nat.mul(Nat.double(q),b),Nat.double(r))) : {_ == 1n+Nat.double(Nat.add(Nat.mul(q,b),r)) : Nat}
78 %even_total(q,r,b) : {1n+Nat.add(Nat.mul(Nat.double(q),b),Nat.double(r)) == 1n+_ : Nat}
79 {==}
80
81def branch_total(+g: Bool,+q: Nat,+s: Nat,+b: Nat,guard: {Nat.is_ge(s,b) == g : Bool}) -> {total(branch(g,q,s,b),b) == Nat.add(Nat.mul(q,b),s) : Nat}:
82 match g:
83 case False{}:
84 {==}
85 case True{}:
86 %Equal.sym(Nat,Nat.add(Nat.add(b,Nat.mul(q,b)),Nat.sub(s,b)),Nat.add(Nat.mul(q,b),Nat.add(Nat.sub(s,b),b)),rotate(b,Nat.mul(q,b),Nat.sub(s,
87 b))) : {_ == Nat.add(Nat.mul(q,b),s) : Nat}
88 %Subtraction.restore(s,b,Order.ge_true(s,b,guard)) : {Nat.add(Nat.mul(q,b),Nat.add(Nat.sub(s,b),b)) == Nat.add(Nat.mul(q,b),_) : Nat}
89 {==}
90
91def step_total(+bit: Bool,+b: Nat,+prev: Quotient) -> {total(step(bit,b,prev),b) == Comparison.digit(bit,total(prev,b)) : Nat}:
92 Quotient{+q,+r} = prev
93 %Equal.sym(Nat,total(branch(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),Comparison.digit(bit,r),b),b),
94 Nat.add(Nat.mul(Nat.double(q),b),Comparison.digit(bit,r)),branch_total(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),
95 Comparison.digit(bit,r),b,{==})) : {_ == Comparison.digit(bit,Nat.add(Nat.mul(q,b),r)) : Nat}
96 digit_total(bit,q,r,b)
97
98def sum_bound(+s: Nat,+b: Nat,h: {Nat.is_lt(s,Nat.double(b)) == True{} : Bool}) -> {Nat.is_lt(s,Nat.add(b,b)) == True{} : Bool}:
99 %Equal.sym(Nat,Nat.add(b,b),Nat.double(b),Addition.double(b)) : {Nat.is_lt(s,_) == True{} : Bool}
100 h
101
102def branch_bound(+g: Bool,+q: Nat,+s: Nat,+b: Nat,guard: {Nat.is_ge(s,b) == g : Bool},bound: {Nat.is_lt(s,
103 Nat.double(b)) == True{} : Bool}) -> {Nat.is_lt(remainder(branch(g,q,s,b)),b) == True{} : Bool}:
104 match g:
105 case False{}:
106 Order.ge_false(s,b,guard)
107 case True{}:
108 Order.sub_lt(s,b,b,Order.ge_true(s,b,guard),sum_bound(s,b,bound))
109
110def step_bound(+bit: Bool,+b: Nat,+prev: Quotient,h: {Nat.is_lt(remainder(prev),b) == True{} : Bool}) -> {Nat.is_lt(remainder(step(bit,b,prev)),
111 b) == True{} : Bool}:
112 Quotient{+q,+r} = prev
113 branch_bound(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),Comparison.digit(bit,r),b,{==},Order.digit_lt(r,b,bit,h))
114
115law go_total:
116 for +n: Nat
117 for +w: Word(n)
118 for +b: Nat
119 {total(go(n,w,b),b) == Word.to_nat(n,w) : Nat}
120def go_total(n,w,b):
121 match n:
122 case 0n:
123 {==}
124 case 1n+ +p:
125 WCon{+bit,+tail} = w
126 %Equal.sym(Nat,Word.to_nat(1n+p,WCon{bit,tail}),Comparison.digit(bit,Word.to_nat(p,tail)),BinaryDigit.word_digit(p,bit,
127 tail)) : {total(step(bit,b,go(p,tail,b)),b) == _ : Nat}
128 %go_total(p,tail,b) : {total(step(bit,b,go(p,tail,b)),b) == Comparison.digit(bit,_) : Nat}
129 step_total(bit,b,go(p,tail,b))
130
131law go_bound:
132 for +n: Nat
133 for +w: Word(n)
134 for +b: Nat
135 for positive: {Nat.is_lt(0n,b) == True{} : Bool}
136 {Nat.is_lt(remainder(go(n,w,b)),b) == True{} : Bool}
137def go_bound(n,w,b,positive):
138 match n:
139 case 0n:
140 positive
141 case 1n+ +p:
142 WCon{+bit,+tail} = w
143 step_bound(bit,b,go(p,tail,b),go_bound(p,tail,b,positive))
144
145def finish(+a: Nat,+b: Nat,+result: Quotient,e: {total(result,b) == a : Nat},positive: {Nat.is_lt(0n,b) == True{} : Bool},
146 bounded: {Nat.is_lt(remainder(result),b) == True{} : Bool}) -> {Nat.divmod(a,b) == pair(result) : Nat & Nat}:
147 Quotient{+q,+r} = result
148 Division.unique(a,b,q,r,Equal.sym(Nat,Nat.add(Nat.mul(q,b),r),a,e),positive,bounded)
149
150def natural(+n: Nat,+w: Word(n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.divmod(Word.to_nat(n,w),b) == pair(go(n,w,
151 b)) : Nat & Nat}:
152 finish(Word.to_nat(n,w),b,go(n,w,b),go_total(n,w,b),positive,go_bound(n,w,b,positive))