1	# Natural division by a positive divisor: the quotient/remainder identity and
2	# monotone quotients, plus monotone truncated subtraction.
3	import Base
4	import ./nat_order.bend as Order
5	import ./nat_division.bend as Division
6	import ./natural_addition.bend as Addition
7	import ./row_major_index.bend as RowMajor
8	import ./word_encoding.bend as WordEncoding
9	
10	type Witness<-value: Nat,-divisor: Nat> is Data:
11	  Witness{quotient: Nat,remainder: Nat,exact: {value == Nat.add(Nat.mul(quotient,divisor),remainder) : Nat},
12	    small: {Nat.is_lt(remainder,divisor) == True{} : Bool}}
13	
14	def not_below(+value: Nat,+limit: Nat,+below: {Nat.is_lt(value,limit) == True{} : Bool},+outside: {Nat.is_lt(1n+value,limit) == False{} : Bool}) ->
15	  {1n+value == limit : Nat}:
16	  match value limit:
17	    case 0n 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(below))
18	    case 1n+rest 0n: Empty.absurd({2n+rest == 0n : Nat},WordEncoding.false_true(below))
19	    case 0n 1n+ +rest:
20	      match rest:
21	        case 0n: {==}
22	        case 1n+more: Empty.absurd({1n == 2n+more : Nat},WordEncoding.false_true(Equal.sym(Bool,True{},False{},outside)))
23	    case 1n+ +left 1n+ +right:
24	      Equal.cong(Nat,Nat,n => 1n+n,1n+left,right,not_below(left,right,below,outside))
25	
26	def advanced(+value: Nat,+divisor: Nat,+quotient: Nat,+remainder: Nat,+inside: Bool,
27	  +exact: {value == Nat.add(Nat.mul(quotient,divisor),remainder) : Nat},+small: {Nat.is_lt(remainder,divisor) == True{} : Bool},
28	  +positive: {Nat.is_lt(0n,divisor) == True{} : Bool},+next: {Nat.is_lt(1n+remainder,divisor) == inside : Bool}) -> Witness<1n+value,divisor>:
29	  match inside:
30	    case True{}:
31	      Witness{quotient,1n+remainder,
32	        %Equal.sym(Nat,value,Nat.add(Nat.mul(quotient,divisor),remainder),exact) : {1n+_ == Nat.add(Nat.mul(quotient,divisor),1n+remainder) : Nat}
33	        Equal.sym(Nat,Nat.add(Nat.mul(quotient,divisor),1n+remainder),1n+Nat.add(Nat.mul(quotient,divisor),remainder),
34	          Addition.successor_right(Nat.mul(quotient,divisor),remainder)),
35	        next}
36	    case False{}:
37	      +full = not_below(remainder,divisor,small,next)
38	      Witness{1n+quotient,0n,
39	        %Equal.sym(Nat,value,Nat.add(Nat.mul(quotient,divisor),remainder),exact) : {1n+_ == Nat.add(Nat.add(divisor,Nat.mul(quotient,divisor)),0n) : Nat}
40	        %Equal.sym(Nat,Nat.add(Nat.add(divisor,Nat.mul(quotient,divisor)),0n),Nat.add(divisor,Nat.mul(quotient,divisor)),Addition.zero_right(Nat.add(divisor,Nat.mul(quotient,divisor)))) :
41	          {1n+Nat.add(Nat.mul(quotient,divisor),remainder) == _ : Nat}
42	        %Order.commutative(Nat.mul(quotient,divisor),divisor) : {1n+Nat.add(Nat.mul(quotient,divisor),remainder) == _ : Nat}
43	        %full : {1n+Nat.add(Nat.mul(quotient,divisor),remainder) == Nat.add(Nat.mul(quotient,divisor),_) : Nat}
44	        Equal.sym(Nat,Nat.add(Nat.mul(quotient,divisor),1n+remainder),1n+Nat.add(Nat.mul(quotient,divisor),remainder),
45	          Addition.successor_right(Nat.mul(quotient,divisor),remainder)),
46	        positive}
47	
48	def successor(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool},+previous: Witness<value,divisor>) -> Witness<1n+value,divisor>:
49	  Witness{+quotient,+remainder,+exact,+small} = previous
50	  advanced(value,divisor,quotient,remainder,Nat.is_lt(1n+remainder,divisor),exact,small,positive,{==})
51	
52	def observed_quotient(-value: Nat,-divisor: Nat,found: Witness<value,divisor>) -> Nat:
53	  Witness{quotient,remainder,exact,small} = found
54	  quotient
55	
56	def observed_remainder(-value: Nat,-divisor: Nat,found: Witness<value,divisor>) -> Nat:
57	  Witness{quotient,remainder,exact,small} = found
58	  remainder
59	
60	def observed_pair(+value: Nat,+divisor: Nat,+found: Witness<value,divisor>,positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
61	  {Nat.divmod(value,divisor) == (observed_quotient(value,divisor,found),observed_remainder(value,divisor,found)) : Nat & Nat}:
62	  Witness{+quotient,+remainder,+exact,+small} = found
63	  Division.unique(value,divisor,quotient,remainder,exact,positive,small)
64	
65	def advanced_pair(+value: Nat,+divisor: Nat,+quotient: Nat,+remainder: Nat,inside: Bool,
66	  +exact: {value == Nat.add(Nat.mul(quotient,divisor),remainder) : Nat},+small: {Nat.is_lt(remainder,divisor) == True{} : Bool},
67	  +positive: {Nat.is_lt(0n,divisor) == True{} : Bool},+next: {Nat.is_lt(1n+remainder,divisor) == inside : Bool}) ->
68	  {Nat.divmod(1n+value,divisor) == Bool.pick(Nat & Nat,inside,(quotient,1n+remainder),(1n+quotient,0n)) : Nat & Nat}:
69	  match inside:
70	    case True{}: observed_pair(1n+value,divisor,advanced(value,divisor,quotient,remainder,True{},exact,small,positive,next),positive)
71	    case False{}: observed_pair(1n+value,divisor,advanced(value,divisor,quotient,remainder,False{},exact,small,positive,next),positive)
72	
73	def increment_case(+value: Nat,+divisor: Nat,+quotient: Nat,+remainder: Nat,
74	  +exact: {value == Nat.add(Nat.mul(quotient,divisor),remainder) : Nat},+small: {Nat.is_lt(remainder,divisor) == True{} : Bool},
75	  +positive: {Nat.is_lt(0n,divisor) == True{} : Bool},which: Order.UpperBound<1n+remainder,divisor>) ->
76	  {Nat.divmod(1n+value,divisor) == Bool.pick(Nat & Nat,Nat.is_eq(1n+remainder,divisor),(1n+quotient,0n),(quotient,1n+remainder)) : Nat & Nat}:
77	  match which:
78	    case Order.Before{+below}:
79	      %Equal.sym(Bool,Nat.is_eq(1n+remainder,divisor),False{},Order.less_not_equal(1n+remainder,divisor,below)) :
80	        {Nat.divmod(1n+value,divisor) == Bool.pick(Nat & Nat,_,(1n+quotient,0n),(quotient,1n+remainder)) : Nat & Nat}
81	      advanced_pair(value,divisor,quotient,remainder,True{},exact,small,positive,below)
82	    case Order.At{+same}:
83	      %Equal.sym(Bool,Nat.is_eq(1n+remainder,divisor),True{},
84	        %same : {Nat.is_eq(1n+remainder,_) == True{} : Bool} Order.equal_reflexive(1n+remainder)) :
85	        {Nat.divmod(1n+value,divisor) == Bool.pick(Nat & Nat,_,(1n+quotient,0n),(quotient,1n+remainder)) : Nat & Nat}
86	      advanced_pair(value,divisor,quotient,remainder,False{},exact,small,positive,
87	        %same : {Nat.is_lt(1n+remainder,_) == False{} : Bool} Order.not_below(1n+remainder,1n+remainder,Order.reflexive(1n+remainder)))
88	
89	def witness(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) -> Witness<value,divisor>:
90	  match value:
91	    case 0n: Witness{0n,0n,{==},positive}
92	    case 1n+ +rest: successor(rest,divisor,positive,witness(rest,divisor,positive))
93	
94	def quotient_exact_of(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool},+found: Witness<value,divisor>) ->
95	  {value == Nat.add(Nat.mul(Nat.div(value,divisor),divisor),Nat.mod(value,divisor)) : Nat}:
96	  Witness{+quotient,+remainder,+exact,+small} = found
97	  %Equal.sym(Nat & Nat,Nat.divmod(value,divisor),(quotient,remainder),Division.unique(value,divisor,quotient,remainder,exact,positive,small)) :
98	    {value == Nat.add(Nat.mul(Pair.fst(Nat,Nat,_),divisor),Pair.snd(Nat,Nat,_)) : Nat}
99	  exact
100	
101	def quotient_exact(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
102	  {value == Nat.add(Nat.mul(Nat.div(value,divisor),divisor),Nat.mod(value,divisor)) : Nat}:
103	  quotient_exact_of(value,divisor,positive,witness(value,divisor,positive))
104	
105	def remainder_small_of(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool},+found: Witness<value,divisor>) ->
106	  {Nat.is_lt(Nat.mod(value,divisor),divisor) == True{} : Bool}:
107	  Witness{+quotient,+remainder,+exact,+small} = found
108	  %Equal.sym(Nat & Nat,Nat.divmod(value,divisor),(quotient,remainder),Division.unique(value,divisor,quotient,remainder,exact,positive,small)) :
109	    {Nat.is_lt(Pair.snd(Nat,Nat,_),divisor) == True{} : Bool}
110	  small
111	
112	def remainder_small(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
113	  {Nat.is_lt(Nat.mod(value,divisor),divisor) == True{} : Bool}:
114	  remainder_small_of(value,divisor,positive,witness(value,divisor,positive))
115	
116	def remainder_le(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) -> {Nat.is_le(Nat.mod(value,divisor),value) == True{} : Bool}:
117	  +quotient = Nat.mul(Nat.div(value,divisor),divisor)
118	  %Equal.sym(Nat,value,Nat.add(quotient,Nat.mod(value,divisor)),quotient_exact(value,divisor,positive)) : {Nat.is_le(Nat.mod(value,divisor),_) == True{} : Bool}
119	  %Order.commutative(Nat.mod(value,divisor),quotient) : {Nat.is_le(Nat.mod(value,divisor),_) == True{} : Bool}
120	  Order.le_add(Nat.mod(value,divisor),quotient)
121	
122	def product_below(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
123	  {Nat.is_le(Nat.mul(Nat.div(value,divisor),divisor),value) == True{} : Bool}:
124	  %Equal.sym(Nat,value,Nat.add(Nat.mul(Nat.div(value,divisor),divisor),Nat.mod(value,divisor)),quotient_exact(value,divisor,positive)) :
125	    {Nat.is_le(Nat.mul(Nat.div(value,divisor),divisor),_) == True{} : Bool}
126	  Order.le_add(Nat.mul(Nat.div(value,divisor),divisor),Nat.mod(value,divisor))
127	
128	def next_above(+value: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
129	  {Nat.is_lt(value,Nat.mul(1n+Nat.div(value,divisor),divisor)) == True{} : Bool}:
130	  +quotient = Nat.div(value,divisor)
131	  +remainder = Nat.mod(value,divisor)
132	  %Equal.sym(Nat,value,Nat.add(Nat.mul(quotient,divisor),remainder),quotient_exact(value,divisor,positive)) :
133	    {Nat.is_lt(_,Nat.add(divisor,Nat.mul(quotient,divisor))) == True{} : Bool}
134	  %Order.commutative(Nat.mul(quotient,divisor),divisor) :
135	    {Nat.is_lt(Nat.add(Nat.mul(quotient,divisor),remainder),_) == True{} : Bool}
136	  %Order.commutative(remainder,Nat.mul(quotient,divisor)) : {Nat.is_lt(_,Nat.add(Nat.mul(quotient,divisor),divisor)) == True{} : Bool}
137	  %Order.commutative(divisor,Nat.mul(quotient,divisor)) : {Nat.is_lt(Nat.add(remainder,Nat.mul(quotient,divisor)),_) == True{} : Bool}
138	  Order.add_lt(remainder,divisor,Nat.mul(quotient,divisor),remainder_small(value,divisor,positive))
139	
140	def quotient_below(+value: Nat,+limit: Nat,+divisor: Nat,positive: {Nat.is_lt(0n,divisor) == True{} : Bool},
141	  inside: {Nat.is_lt(value,Nat.mul(limit,divisor)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(value,divisor),limit) == True{} : Bool}:
142	  RowMajor.cancel_multiply_lt(Nat.div(value,divisor),limit,divisor,
143	    Order.le_lt_trans(Nat.mul(Nat.div(value,divisor),divisor),value,Nat.mul(limit,divisor),product_below(value,divisor,positive),inside))
144	
145	def quotient_le(+smaller: Nat,+larger: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool},
146	  +ordered: {Nat.is_le(smaller,larger) == True{} : Bool}) -> {Nat.is_le(Nat.div(smaller,divisor),Nat.div(larger,divisor)) == True{} : Bool}:
147	  Division.lt_succ_le(Nat.div(smaller,divisor),Nat.div(larger,divisor),
148	    RowMajor.cancel_multiply_lt(Nat.div(smaller,divisor),1n+Nat.div(larger,divisor),divisor,
149	      Order.le_lt_trans(Nat.mul(Nat.div(smaller,divisor),divisor),larger,Nat.mul(1n+Nat.div(larger,divisor),divisor),
150	        Order.transitive(Nat.mul(Nat.div(smaller,divisor),divisor),smaller,larger,product_below(smaller,divisor,positive),ordered),
151	        next_above(larger,divisor,positive))))
152	
153	def subtract_le(+smaller: Nat,+larger: Nat,+amount: Nat,+ordered: {Nat.is_le(smaller,larger) == True{} : Bool}) ->
154	  {Nat.is_le(Nat.sub(smaller,amount),Nat.sub(larger,amount)) == True{} : Bool}:
155	  match smaller larger amount:
156	    case 0n 0n 0n: {==}
157	    case 0n 0n 1n+rest: {==}
158	    case 0n 1n+above 0n: {==}
159	    case 0n 1n+ +above 1n+ +rest: Order.zero_le(Nat.sub(above,rest))
160	    case 1n+left 0n 0n: Empty.absurd({Nat.is_le(1n+left,0n) == True{} : Bool},WordEncoding.false_true(ordered))
161	    case 1n+left 0n 1n+rest: Empty.absurd({Nat.is_le(Nat.sub(left,rest),0n) == True{} : Bool},WordEncoding.false_true(ordered))
162	    case 1n+left 1n+right 0n: ordered
163	    case 1n+ +left 1n+ +right 1n+ +rest: subtract_le(left,right,rest,ordered)
164	
165	# Adding whole rows changes the quotient and preserves the remainder.
166	def shifted_exact(+value: Nat,+divisor: Nat,+rows: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
167	  {Nat.add(Nat.mul(rows,divisor),value) == Nat.add(Nat.mul(Nat.add(rows,Nat.div(value,divisor)),divisor),Nat.mod(value,divisor)) : Nat}:
168	  +q = Nat.div(value,divisor)
169	  +r = Nat.mod(value,divisor)
170	  %Equal.sym(Nat,value,Nat.add(Nat.mul(q,divisor),r),quotient_exact(value,divisor,positive)) :
171	    {Nat.add(Nat.mul(rows,divisor),_) == Nat.add(Nat.mul(Nat.add(rows,q),divisor),r) : Nat}
172	  %Equal.sym(Nat,Nat.mul(Nat.add(rows,q),divisor),Nat.add(Nat.mul(rows,divisor),Nat.mul(q,divisor)),RowMajor.distrib(rows,q,divisor)) :
173	    {Nat.add(Nat.mul(rows,divisor),Nat.add(Nat.mul(q,divisor),r)) == Nat.add(_,r) : Nat}
174	  Equal.sym(Nat,Nat.add(Nat.add(Nat.mul(rows,divisor),Nat.mul(q,divisor)),r),Nat.add(Nat.mul(rows,divisor),Nat.add(Nat.mul(q,divisor),r)),Addition.associative(Nat.mul(rows,divisor),Nat.mul(q,divisor),r))
175	
176	def shifted_pair(+value: Nat,+divisor: Nat,+rows: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
177	  {Nat.divmod(Nat.add(Nat.mul(rows,divisor),value),divisor) == (Nat.add(rows,Nat.div(value,divisor)),Nat.mod(value,divisor)) : Nat & Nat}:
178	  Division.unique(Nat.add(Nat.mul(rows,divisor),value),divisor,Nat.add(rows,Nat.div(value,divisor)),Nat.mod(value,divisor),shifted_exact(value,divisor,rows,positive),positive,remainder_small(value,divisor,positive))
179	
180	def quotient_shift(+value: Nat,+divisor: Nat,+rows: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
181	  {Nat.div(Nat.add(Nat.mul(rows,divisor),value),divisor) == Nat.add(rows,Nat.div(value,divisor)) : Nat}:
182	  Equal.cong(Nat & Nat,Nat,pair => Pair.fst(Nat,Nat,pair),Nat.divmod(Nat.add(Nat.mul(rows,divisor),value),divisor),(Nat.add(rows,Nat.div(value,divisor)),Nat.mod(value,divisor)),shifted_pair(value,divisor,rows,positive))
183	
184	def remainder_shift(+value: Nat,+divisor: Nat,+rows: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
185	  {Nat.mod(Nat.add(Nat.mul(rows,divisor),value),divisor) == Nat.mod(value,divisor) : Nat}:
186	  Equal.cong(Nat & Nat,Nat,pair => Pair.snd(Nat,Nat,pair),Nat.divmod(Nat.add(Nat.mul(rows,divisor),value),divisor),(Nat.add(rows,Nat.div(value,divisor)),Nat.mod(value,divisor)),shifted_pair(value,divisor,rows,positive))
187	
188	def multiply_left_le(+factor: Nat,+smaller: Nat,+larger: Nat,+ordered: {Nat.is_le(smaller,larger) == True{} : Bool}) ->
189	  {Nat.is_le(Nat.mul(factor,smaller),Nat.mul(factor,larger)) == True{} : Bool}:
190	  %RowMajor.multiply_commutative(smaller,factor) : {Nat.is_le(_,Nat.mul(factor,larger)) == True{} : Bool}
191	  %RowMajor.multiply_commutative(larger,factor) : {Nat.is_le(Nat.mul(smaller,factor),_) == True{} : Bool}
192	  RowMajor.mul_le(smaller,larger,factor,ordered)
193	
194	def right_factor_positive(+head: Nat,+tail: Nat,positive: {Nat.is_lt(0n,Nat.mul(head,tail)) == True{} : Bool}) -> {Nat.is_lt(0n,tail) == True{} : Bool}:
195	  RowMajor.left_factor_positive(tail,head,%RowMajor.multiply_commutative(head,tail) : {Nat.is_lt(0n,_) == True{} : Bool} positive)
196	
197	def le_multiple(+images: Nat,+elements: Nat,positive: {Nat.is_lt(0n,images) == True{} : Bool}) ->
198	  {Nat.is_le(elements,Nat.mul(images,elements)) == True{} : Bool}:
199	  %Equal.sym(Nat,Nat.mul(images,elements),Nat.mul(elements,images),RowMajor.multiply_commutative(images,elements)) : {Nat.is_le(elements,_) == True{} : Bool}
200	  RowMajor.product_covers(elements,images,positive)
201	
202	def subtract_sum(+a: Nat,+b: Nat) -> {Nat.sub(Nat.add(a,b),b) == a : Nat}:
203	  match b:
204	    case 0n:
205	      %Equal.sym(Nat,Nat.add(a,0n),a,Addition.zero_right(a)) : {Nat.sub(_,0n) == a : Nat}
206	      Order.subtract_zero(a)
207	    case 1n+ +p:
208	      %Equal.sym(Nat,Nat.add(a,1n+p),1n+Nat.add(a,p),Addition.successor_right(a,p)) : {Nat.sub(_,1n+p) == a : Nat}
209	      subtract_sum(a,p)