1	# Characterize Base.Nat.divmod by quotient/remainder and remainder bounds.
2	import Base
3	import ./natural_addition.bend as Addition
4	import ./word_encoding.bend as WordEncoding
5	
6	def lt_zero(+n: Nat) -> {Nat.is_lt(n,0n) == False{} : Bool}:
7	  match n:
8	    case 0n:
9	      {==}
10	    case 1n+p:
11	      {==}
12	
13	def 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	
25	def 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	
37	def 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	
46	def bump(pair: Nat & Nat) -> Nat & Nat:
47	  (q,r) = pair
48	  (1n+q,r)
49	
50	def bumped_quotient(pair: Nat & Nat) -> {Pair.fst(Nat,Nat,bump(pair)) == 1n+Pair.fst(Nat,Nat,pair) : Nat}:
51	  (quotient,remainder) = pair
52	  {==}
53	
54	law 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}
60	def 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	
71	law 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}
77	def 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	
85	def 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	
95	law 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}
102	def 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	
114	def 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	
119	def 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	  {==}