1	# Natural-number binary long division, proved against the frozen Base.divmod.
2	import Base
3	import ./natural_addition.bend as Addition
4	import ./binary_digit.bend as BinaryDigit
5	import ./u32_comparison.bend as Comparison
6	import ./nat_order.bend as Order
7	import ./nat_division.bend as Division
8	import ./word_multiplication.bend as Multiplication
9	import ./word_subtraction.bend as Subtraction
10	import ./word_encoding.bend as WordEncoding
11	
12	type Quotient is Data:
13	  Quotient{quotient: Nat,remainder: Nat}
14	
15	def total(result: Quotient,b: Nat) -> Nat:
16	  Quotient{q,r} = result
17	  Nat.add(Nat.mul(q,b),r)
18	
19	def remainder(result: Quotient) -> Nat:
20	  Quotient{q,r} = result
21	  r
22	
23	def pair(result: Quotient) -> Nat & Nat:
24	  Quotient{q,r} = result
25	  (q,r)
26	
27	def 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	
34	def 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	
39	def 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	
47	def 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	
51	def 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	
61	def 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	
65	def 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	
70	def 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	
81	def 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	
91	def 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	
98	def 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	
102	def 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	
110	def 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	
115	law 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}
120	def 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	
131	law 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}
137	def 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	
145	def 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	
150	def 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))