proofs/nat_division.bend
stelliferous@0.0.3.0 · 125 lines · 0 definitions
1# Characterize Base.Nat.divmod by quotient/remainder and remainder bounds.
2import Base
3import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
4import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
5
6def lt_zero(+n: Nat) -> {Nat.is_lt(n,0n) == False{} : Bool}:
7 match n:
8 case 0n:
9 {==}
10 case 1n+p:
11 {==}
12
13def lt_succ_le(+n: Nat,+m: Nat,h: {Nat.is_lt(n,1n+m) == True{} : Bool}) -> {Nat.is_le(n,m) == True{} : Bool}:
14 match n m:
15 case 0n 0n:
16 {==}
17 case 0n 1n+m:
18 {==}
19 case 1n+ +n 0n:
20 Empty.absurd({Nat.is_le(1n+n,0n) == True{} : Bool},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(n,0n),True{},Equal.sym(Bool,
21 Nat.is_lt(n,0n),False{},lt_zero(n)),h)))
22 case 1n+n 1n+m:
23 lt_succ_le(n,m,h)
24
25def go_small(+n: Nat,+m: Nat,+d: Nat,+r: Nat,h: {Nat.is_le(n,m) == True{} : Bool}) -> {Nat.divmod.go(n,m,d,r) == (d,Nat.add(n,r)) : Nat & Nat}:
26 match n:
27 case 0n:
28 {==}
29 case 1n+ +p:
30 match m:
31 case 0n:
32 Empty.absurd({Nat.divmod.go(1n+p,0n,d,r) == (d,Nat.add(1n+p,r)) : Nat & Nat},WordEncoding.false_true(h))
33 case 1n+ +q:
34 %Addition.successor_right(p,r) : {Nat.divmod.go(p,q,d,1n+r) == (d,_) : Nat & Nat}
35 go_small(p,q,d,1n+r,h)
36
37def small(+r: Nat,+b: Nat,h: {Nat.is_lt(r,b) == True{} : Bool}) -> {Nat.divmod(r,b) == (0n,r) : Nat & Nat}:
38 match b:
39 case 0n:
40 Empty.absurd({Nat.divmod(r,0n) == (0n,r) : Nat & Nat},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(r,0n),True{},
41 Equal.sym(Bool,Nat.is_lt(r,0n),False{},lt_zero(r)),h)))
42 case 1n+ +p:
43 %Addition.zero_right(r) : {Nat.divmod.go(r,p,0n,0n) == (0n,_) : Nat & Nat}
44 go_small(r,p,0n,0n,lt_succ_le(r,p,h))
45
46def bump(pair: Nat & Nat) -> Nat & Nat:
47 (q,r) = pair
48 (1n+q,r)
49
50def bumped_quotient(pair: Nat & Nat) -> {Pair.fst(Nat,Nat,bump(pair)) == 1n+Pair.fst(Nat,Nat,pair) : Nat}:
51 (quotient,remainder) = pair
52 {==}
53
54law bump_go:
55 for +n: Nat
56 for +m: Nat
57 for +d: Nat
58 for +r: Nat
59 {Nat.divmod.go(n,m,1n+d,r) == bump(Nat.divmod.go(n,m,d,r)) : Nat & Nat}
60def bump_go(n,m,d,r):
61 match n:
62 case 0n:
63 {==}
64 case 1n+ +p:
65 match m:
66 case 0n:
67 bump_go(p,r,1n+d,0n)
68 case 1n+q:
69 bump_go(p,q,d,1n+r)
70
71law cycle:
72 for +m: Nat
73 for +tail: Nat
74 for +d: Nat
75 for +r: Nat
76 {Nat.divmod.go(Nat.add(1n+m,tail),m,d,r) == Nat.divmod.go(tail,Nat.add(m,r),1n+d,0n) : Nat & Nat}
77def cycle(m,tail,d,r):
78 match m:
79 case 0n:
80 {==}
81 case 1n+ +p:
82 %Addition.successor_right(p,r) : {Nat.divmod.go(Nat.add(1n+p,tail),p,d,1n+r) == Nat.divmod.go(tail,_,1n+d,0n) : Nat & Nat}
83 cycle(p,tail,d,1n+r)
84
85def add_divisor(+a: Nat,+b: Nat,h: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.divmod(Nat.add(b,a),b) == bump(Nat.divmod(a,b)) : Nat & Nat}:
86 match b:
87 case 0n:
88 Empty.absurd({Nat.divmod(a,0n) == bump(Nat.divmod(a,0n)) : Nat & Nat},WordEncoding.false_true(h))
89 case 1n+ +p:
90 %Equal.sym(Nat & Nat,Nat.divmod.go(Nat.add(1n+p,a),p,0n,0n),Nat.divmod.go(a,Nat.add(p,0n),1n,0n),cycle(p,a,0n,
91 0n)) : {_ == bump(Nat.divmod.go(a,p,0n,0n)) : Nat & Nat}
92 %Equal.sym(Nat,Nat.add(p,0n),p,Addition.zero_right(p)) : {Nat.divmod.go(a,_,1n,0n) == bump(Nat.divmod.go(a,p,0n,0n)) : Nat & Nat}
93 bump_go(a,p,0n,0n)
94
95law quotient_remainder:
96 for +q: Nat
97 for +r: Nat
98 for +b: Nat
99 for +positive: {Nat.is_lt(0n,b) == True{} : Bool}
100 for +bounded: {Nat.is_lt(r,b) == True{} : Bool}
101 {Nat.divmod(Nat.add(Nat.mul(q,b),r),b) == (q,r) : Nat & Nat}
102def quotient_remainder(q,r,b,positive,bounded):
103 match q:
104 case 0n:
105 small(r,b,bounded)
106 case 1n+ +p:
107 %Equal.sym(Nat,Nat.add(Nat.add(b,Nat.mul(p,b)),r),Nat.add(b,Nat.add(Nat.mul(p,b),r)),Addition.associative(b,Nat.mul(p,b),
108 r)) : {Nat.divmod(_,b) == (1n+p,r) : Nat & Nat}
109 %Equal.sym(Nat & Nat,Nat.divmod(Nat.add(b,Nat.add(Nat.mul(p,b),r)),b),bump(Nat.divmod(Nat.add(Nat.mul(p,b),r),b)),
110 add_divisor(Nat.add(Nat.mul(p,b),r),b,positive)) : {_ == (1n+p,r) : Nat & Nat}
111 %Equal.sym(Nat & Nat,Nat.divmod(Nat.add(Nat.mul(p,b),r),b),(p,r),quotient_remainder(p,r,b,positive,bounded)) : {bump(_) == (1n+p,r) : Nat & Nat}
112 {==}
113
114def unique(+a: Nat,+b: Nat,+q: Nat,+r: Nat,e: {a == Nat.add(Nat.mul(q,b),r) : Nat},positive: {Nat.is_lt(0n,b) == True{} : Bool},
115 bounded: {Nat.is_lt(r,b) == True{} : Bool}) -> {Nat.divmod(a,b) == (q,r) : Nat & Nat}:
116 %Equal.sym(Nat,a,Nat.add(Nat.mul(q,b),r),e) : {Nat.divmod(_,b) == (q,r) : Nat & Nat}
117 quotient_remainder(q,r,b,positive,bounded)
118
119def exact_quotient(+quotient: Nat,+divisor: Nat,+positive: {Nat.is_lt(0n,divisor) == True{} : Bool}) ->
120 {Nat.div(Nat.mul(quotient,divisor),divisor) == quotient : Nat}:
121 %Addition.zero_right(Nat.mul(quotient,divisor)) :
122 {Nat.div(_,divisor) == quotient : Nat}
123 %Equal.sym(Nat & Nat,Nat.divmod(Nat.add(Nat.mul(quotient,divisor),0n),divisor),(quotient,0n),
124 quotient_remainder(quotient,0n,divisor,positive,positive)) : {Pair.fst(Nat,Nat,_) == quotient : Nat}
125 {==}