1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../lib/nat.bend as N
4	import ../../lib/lemmas/proofs/nat_algebra.bend as A
5	import ../../../src/math/number.bend as NB
6	import ../../../spec/math/number.bend as SN
7	import ../typed/width.bend as WW
8	
9	# bit_count counts the 1 bits (Python int.bit_count; Lean 4 Mathlib
10	# Nat.bits and List.count true): each step adds n mod 2 == bit(n) and
11	# continues with n div 2 == half(n), the definition of ones.
12	
13	def half_div2(+n: Nat) -> {C.half(n) == Nat.div(n, 2n) : Nat}:
14	  match n:
15	    case 0n:
16	      {==}
17	    case 1n:
18	      {==}
19	    case 2n+ +q:
20	      Equal.trans(Nat, 1n+C.half(q), 1n+Nat.div(q, 2n), Nat.div(2n+q, 2n), Equal.cong(Nat, Nat, t => 1n+t, C.half(q), Nat.div(q, 2n), half_div2(q)), Equal.sym(Nat, Nat.div(2n+q, 2n), 1n+Nat.div(q, 2n), N.div2_step(q)))
21	
22	def ones_zero(+k: Nat) -> {SN.ones(k, 0n) == 0n : Nat}:
23	  match k:
24	    case 0n:
25	      {==}
26	    case 1n+ +p:
27	      ones_zero(p)
28	
29	# the loop adds the ones of its fuel's worth of bits
30	def go(+f: Nat, +n: Nat, +acc: Nat) -> {NB.bit_count_go(f, n, acc) == Nat.add(acc, SN.ones(f, n)) : Nat}:
31	  match f n:
32	    case 0n _:
33	      Equal.sym(Nat, Nat.add(acc, 0n), acc, A.add_zero(acc))
34	    case 1n+ +g 0n:
35	      %Equal.sym(Nat, SN.ones(g, 0n), 0n, ones_zero(g)) : {acc == Nat.add(acc, _) : Nat}
36	      Equal.sym(Nat, Nat.add(acc, 0n), acc, A.add_zero(acc))
37	    case 1n+ +g 1n+ +np:
38	      %Equal.sym(Nat, C.bit(1n+np), Nat.mod(1n+np, 2n), WW.bit_mod(1n+np)) : {NB.bit_count_go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n))) == Nat.add(acc, Nat.add(_, SN.ones(g, C.half(1n+np)))) : Nat}
39	      %Equal.sym(Nat, C.half(1n+np), Nat.div(1n+np, 2n), half_div2(1n+np)) : {NB.bit_count_go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n))) == Nat.add(acc, Nat.add(Nat.mod(1n+np, 2n), SN.ones(g, _))) : Nat}
40	      %A.add_assoc(acc, Nat.mod(1n+np, 2n), SN.ones(g, Nat.div(1n+np, 2n))) : {NB.bit_count_go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n))) == _ : Nat}
41	      go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n)))
42	
43	def bit_count_value(+n: Nat) -> SN.BitCount.value(n):
44	  go(n, n, 0n)