proofs/nat_division_order.bend
stelliferous@0.0.3.0 · 209 lines · 0 definitions
1# Natural division by a positive divisor: the quotient/remainder identity and
2# monotone quotients, plus monotone truncated subtraction.
3import Base
4import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
5import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
6import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
7import stelliferous@0.0.3.0/proofs/row_major_index.bend as RowMajor
8import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
9
10type 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
14def 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
26def 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
48def 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
52def observed_quotient(-value: Nat,-divisor: Nat,found: Witness<value,divisor>) -> Nat:
53 Witness{quotient,remainder,exact,small} = found
54 quotient
55
56def observed_remainder(-value: Nat,-divisor: Nat,found: Witness<value,divisor>) -> Nat:
57 Witness{quotient,remainder,exact,small} = found
58 remainder
59
60def 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
65def 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
73def 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
89def 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
94def 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
101def 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
105def 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
112def 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
116def 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
122def 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
128def 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
140def 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
145def 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
153def 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.
166def 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
176def 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
180def 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
184def 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
188def 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
194def 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
197def 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
202def 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)