1	# Proofs of LAWS_div.bend, from Base's definition of Nat.divmod: with a
2	# divisor 1 + bp, Nat.divmod(a, 1 + bp) runs go(a, bp, 0, 0), which counts m
3	# down and r up (m + r == bp throughout) and d once per full round. The
4	# lemmas are those bend-osdev-ext2, -iodev and -blockdev proved for their
5	# own use (PROOF.bend, PROOF_range.bend), now proved here once.
6	import Base
7	import ./LAWS.bend as UL
8	import ./PROOF.bend as UP
9	import ./LAWS_div.bend as Laws
10	
11	def ud.sub_zero(a: Nat) -> {Nat.sub(a, 0n) == a : Nat}:
12	  match a:
13	    case 0n:
14	      {==}
15	    case 1n+p:
16	      {==}
17	
18	def ud.pred(n: Nat) -> Nat:
19	  match n:
20	    case 0n:
21	      0n
22	    case 1n+p:
23	      p
24	
25	def ud.succ_inj(+x: Nat, +y: Nat, e: {1n+x == 1n+y : Nat}) -> {x == y : Nat}:
26	  Equal.cong(Nat, Nat, ud.pred, 1n+x, 1n+y, e)
27	
28	# a + r == b + r gives a == b
29	def ud.add_cancel(+r: Nat, +a: Nat, +b: Nat, e: {Nat.add(a, r) == Nat.add(b, r) : Nat}) -> {a == b : Nat}:
30	  match r:
31	    case 0n:
32	      Equal.trans(Nat, a, Nat.add(b, 0n), b, Equal.trans(Nat, a, Nat.add(a, 0n), Nat.add(b, 0n), Equal.sym(Nat, Nat.add(a, 0n), a, UL.nat_add_zero(a)), e), UL.nat_add_zero(b))
33	    case 1n+q:
34	      ud.add_cancel(q, a, b, ud.succ_inj(Nat.add(a, q), Nat.add(b, q), Equal.trans(Nat, 1n+Nat.add(a, q), Nat.add(a, 1n+q), 1n+Nat.add(b, q), Equal.sym(Nat, Nat.add(a, 1n+q), 1n+Nat.add(a, q), UL.nat_add_succ(a, q)), Equal.trans(Nat, Nat.add(a, 1n+q), Nat.add(b, 1n+q), 1n+Nat.add(b, q), e, UL.nat_add_succ(b, q)))))
35	
36	def ud.bool_disc(b: Bool) -> Type:
37	  match b:
38	    case True{}:
39	      Unit
40	    case False{}:
41	      Empty
42	
43	def ud.bool_clash(h: {False{} == True{} : Bool}) -> Empty:
44	  %Equal.sym(Bool, False{}, True{}, h) : ud.bool_disc(_)
45	  Unit{}
46	
47	def ud.ex_falso(-A: Type, e: Empty) -> A:
48	  match e:
49	
50	def ud.no_lt_one(+np: Nat) -> {Nat.is_lt(1n+np, 1n) == True{} : Bool} -> Empty:
51	  match np:
52	    case 0n:
53	      h => ud.bool_clash(h)
54	    case 1n+q:
55	      h => ud.bool_clash(h)
56	
57	# r < bp + 1 gives (bp - r) + r == bp
58	def ud.sub_add(+bp: Nat, +r: Nat, h: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.add(Nat.sub(bp, r), r) == bp : Nat}:
59	  match bp r:
60	    case 0n 0n:
61	      {==}
62	    case 0n 1n+q:
63	      ud.ex_falso({Nat.add(Nat.sub(0n, 1n+q), 1n+q) == 0n : Nat}, ud.no_lt_one(q, h))
64	    case 1n+b 0n:
65	      UL.nat_add_zero(1n+b)
66	    case 1n+b 1n+q:
67	      Equal.trans(Nat, Nat.add(Nat.sub(b, q), 1n+q), 1n+Nat.add(Nat.sub(b, q), q), 1n+b, UL.nat_add_succ(Nat.sub(b, q), q), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(Nat.sub(b, q), q), b, ud.sub_add(b, q, h)))
68	
69	# Division
70	
71	def ud.dm_lhs(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> Nat:
72	  Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)))
73	
74	def ud.dm_sum(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> {Nat.add(m, r) == bp : Nat} -> {ud.dm_lhs(n, m, d, r, bp) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}:
75	  match n m:
76	    case 0n _:
77	      h => {==}
78	    case 1n+np 0n:
79	      +h =>
80	        +dd = Nat.mul(d, 1n+bp)
81	        +x = Nat.add(Nat.add(bp, dd), 0n)
82	        %Equal.sym(Nat, r, bp, h) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, Nat.add(dd, _)) : Nat}
83	        %UL.nat_add_comm(bp, dd) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, _) : Nat}
84	        %UL.nat_add_zero(Nat.add(bp, dd)) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, _) : Nat}
85	        %UL.nat_add_succ(np, x) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == _ : Nat}
86	        ud.dm_sum(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, UL.nat_add_zero(r), h))
87	    case 1n+np 1n+mp:
88	      h =>
89	        +dd = Nat.mul(d, 1n+bp)
90	        %UL.nat_add_succ(np, Nat.add(dd, r)) : {ud.dm_lhs(1n+np, 1n+mp, d, r, bp) == _ : Nat}
91	        %UL.nat_add_succ(dd, r) : {ud.dm_lhs(1n+np, 1n+mp, d, r, bp) == Nat.add(np, _) : Nat}
92	        ud.dm_sum(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, UL.nat_add_succ(mp, r), h))
93	
94	def ud.div_mod(+k: Nat, +bp: Nat) -> {Nat.add(Nat.mul(Nat.div(k, 1n+bp), 1n+bp), Nat.mod(k, 1n+bp)) == k : Nat}:
95	  Equal.trans(Nat, ud.dm_lhs(k, bp, 0n, 0n, bp), Nat.add(k, 0n), k, ud.dm_sum(k, bp, 0n, 0n, bp, UL.nat_add_zero(bp)), UL.nat_add_zero(k))
96	
97	def ud.lt_add(+m: Nat, +r: Nat) -> {Nat.is_lt(r, 1n+Nat.add(m, r)) == True{} : Bool}:
98	  match r:
99	    case 0n:
100	      {==}
101	    case 1n+p:
102	      %Equal.sym(Nat, Nat.add(m, 1n+p), 1n+Nat.add(m, p), UL.nat_add_succ(m, p)) : {Nat.is_lt(1n+p, 1n+_) == True{} : Bool}
103	      ud.lt_add(m, p)
104	
105	def ud.dm_lt(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> {Nat.add(m, r) == bp : Nat} -> {Nat.is_lt(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp) == True{} : Bool}:
106	  match n m:
107	    case 0n _:
108	      h =>
109	        %h : {Nat.is_lt(r, 1n+_) == True{} : Bool}
110	        ud.lt_add(m, r)
111	    case 1n+np 0n:
112	      h => ud.dm_lt(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, UL.nat_add_zero(r), h))
113	    case 1n+np 1n+mp:
114	      h => ud.dm_lt(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, UL.nat_add_succ(mp, r), h))
115	
116	def ud.mod_lt(+k: Nat, +bp: Nat) -> {Nat.is_lt(Nat.mod(k, 1n+bp), 1n+bp) == True{} : Bool}:
117	  ud.dm_lt(k, bp, 0n, 0n, bp, UL.nat_add_zero(bp))
118	
119	# fewer steps than m left in the round: the remainder grows by n
120	def ud.dm_small(+n: Nat, +m: Nat, +d: Nat, +r: Nat) -> {Nat.is_lt(n, 1n+m) == True{} : Bool} -> {Nat.divmod.go(n, m, d, r) == (d, Nat.add(n, r)) : Nat & Nat}:
121	  match n m:
122	    case 0n _:
123	      h => {==}
124	    case 1n+np 0n:
125	      h => ud.ex_falso({Nat.divmod.go(1n+np, 0n, d, r) == (d, Nat.add(1n+np, r)) : Nat & Nat}, ud.no_lt_one(np, h))
126	    case 1n+np 1n+mp:
127	      h =>
128	        %UL.nat_add_succ(np, r) : {Nat.divmod.go(1n+np, 1n+mp, d, r) == (d, _) : Nat & Nat}
129	        ud.dm_small(np, mp, d, 1n+r, h)
130	
131	# finishing a round: m steps, then one more starts the next
132	def ud.dm_round(+m: Nat, +n: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(Nat.add(m, 1n+n), m, d, r) == Nat.divmod.go(n, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}:
133	  match m:
134	    case 0n:
135	      {==}
136	    case 1n+mp:
137	      %UL.nat_add_succ(mp, r) : {Nat.divmod.go(Nat.add(1n+mp, 1n+n), 1n+mp, d, r) == Nat.divmod.go(n, _, 1n+d, 0n) : Nat & Nat}
138	      ud.dm_round(mp, n, d, 1n+r)
139	
140	def ud.dm_rounds(+g: Nat, +i: Nat, +d: Nat, +bp: Nat) -> {Nat.is_lt(i, 1n+bp) == True{} : Bool} -> {Nat.divmod.go(Nat.add(Nat.mul(g, 1n+bp), i), bp, d, 0n) == (Nat.add(g, d), i) : Nat & Nat}:
141	  match g:
142	    case 0n:
143	      h =>
144	        %UL.nat_add_zero(i) : {Nat.divmod.go(i, bp, d, 0n) == (d, _) : Nat & Nat}
145	        ud.dm_small(i, bp, d, 0n, h)
146	    case 1n+gp:
147	      h =>
148	        +gg = Nat.mul(gp, 1n+bp)
149	        +y = Nat.add(gg, i)
150	        %Equal.sym(Nat, Nat.add(Nat.add(bp, gg), i), Nat.add(bp, y), UL.nat_add_assoc(bp, gg, i)) : {Nat.divmod.go(1n+_, bp, d, 0n) == (1n+Nat.add(gp, d), i) : Nat & Nat}
151	        %UL.nat_add_succ(bp, y) : {Nat.divmod.go(_, bp, d, 0n) == (1n+Nat.add(gp, d), i) : Nat & Nat}
152	        %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(bp, 1n+y), bp, d, 0n), Nat.divmod.go(y, Nat.add(bp, 0n), 1n+d, 0n), ud.dm_round(bp, y, d, 0n)) : {_ == (1n+Nat.add(gp, d), i) : Nat & Nat}
153	        %Equal.sym(Nat, Nat.add(bp, 0n), bp, UL.nat_add_zero(bp)) : {Nat.divmod.go(y, _, 1n+d, 0n) == (1n+Nat.add(gp, d), i) : Nat & Nat}
154	        %UL.nat_add_succ(gp, d) : {Nat.divmod.go(y, bp, 1n+d, 0n) == (_, i) : Nat & Nat}
155	        ud.dm_rounds(gp, i, 1n+d, bp, h)
156	
157	# Rounding up. Nat.sub(1 + bp, 1) is Nat.sub(bp, 0), which is bp by
158	# ud.sub_zero.
159	
160	# a + bp == (a + (bp - r)) + r, for r < 1 + bp
161	def ud.cover_sum(+bp: Nat, +a: Nat, +r: Nat, h: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.add(a, Nat.sub(bp, 0n)) == Nat.add(Nat.add(a, Nat.sub(bp, r)), r) : Nat}:
162	  %Equal.sym(Nat, Nat.sub(bp, 0n), bp, ud.sub_zero(bp)) : {Nat.add(a, _) == Nat.add(Nat.add(a, Nat.sub(bp, r)), r) : Nat}
163	  %Equal.sym(Nat, Nat.add(Nat.add(a, Nat.sub(bp, r)), r), Nat.add(a, Nat.add(Nat.sub(bp, r), r)), UL.nat_add_assoc(a, Nat.sub(bp, r), r)) : {Nat.add(a, bp) == _ : Nat}
164	  %ud.sub_add(bp, r, h) : {Nat.add(a, _) == Nat.add(a, Nat.add(Nat.sub(bp, r), r)) : Nat}
165	  {==}
166	
167	def ud.cover(+bp: Nat, +a: Nat) -> {Nat.mul(Nat.div(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp), 1n+bp) == Nat.add(a, Nat.sub(Nat.sub(1n+bp, 1n), Nat.mod(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp))) : Nat}:
168	  +t = Nat.add(a, Nat.sub(bp, 0n))
169	  +q = Nat.div(t, 1n+bp)
170	  +r = Nat.mod(t, 1n+bp)
171	  %Equal.sym(Nat, Nat.sub(bp, 0n), bp, ud.sub_zero(bp)) : {Nat.mul(q, 1n+bp) == Nat.add(a, Nat.sub(_, r)) : Nat}
172	  ud.add_cancel(r, Nat.mul(q, 1n+bp), Nat.add(a, Nat.sub(bp, r)), Equal.trans(Nat, Nat.add(Nat.mul(q, 1n+bp), r), t, Nat.add(Nat.add(a, Nat.sub(bp, r)), r), ud.div_mod(t, bp), ud.cover_sum(bp, a, r, ud.mod_lt(t, bp))))
173	
174	# The laws
175	
176	def Laws.nat_div_mod(a, bp):
177	  ud.div_mod(a, bp)
178	
179	def Laws.nat_mod_lt(a, bp):
180	  ud.mod_lt(a, bp)
181	
182	def Laws.nat_divmod_exact(g, i, bp, h):
183	  %UL.nat_add_zero(g) : {Nat.divmod.go(Nat.add(Nat.mul(g, 1n+bp), i), bp, 0n, 0n) == (_, i) : Nat & Nat}
184	  ud.dm_rounds(g, i, 0n, bp, h)
185	
186	def Laws.nat_round_up(bp, a):
187	  ud.cover(bp, a)