1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/logic.bend as L
4	import ../../lib/lemmas/proofs/nat_algebra.bend as A
5	import ../../../src/math/natural.bend as M
6	import ./arith.bend as R
7	import ./roots.bend as RT
8	
9	# ilog(n, b) is the exact integer logarithm: b^r <= n < b^(r + 1) for
10	# n >= 1, b >= 2, and Domain otherwise (Lean 4 Mathlib Mathlib/Data/Nat/Log:
11	# Nat.pow_log_le_self, Nat.lt_pow_succ_log_self; the reference's ilog,
12	# section 10).
13	
14	# a <= b gives a + c <= b + c
15	def le_add_r(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:
16	  %Equal.sym(Nat, Nat.add(a, c), Nat.add(c, a), A.add_comm(a, c)) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool}
17	  %Equal.sym(Nat, Nat.add(b, c), Nat.add(c, b), A.add_comm(b, c)) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool}
18	  N.le_add_left(a, b, c, h)
19	
20	# a < a + c for c > 0
21	def lt_add_pos(+a: Nat, +c: Nat, +h: {Nat.is_lt(0n, c) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(a, c)) == True{} : Bool}:
22	  %Equal.sym(Nat, a, Nat.add(a, 0n), Equal.sym(Nat, Nat.add(a, 0n), a, A.add_zero(a))) : {Nat.is_lt(_, Nat.add(a, c)) == True{} : Bool}
23	  N.lt_add_left(0n, c, a, h)
24	
25	# k < b^k for b >= 2
26	def pow_gt(+bq: Nat, +k: Nat) -> {Nat.is_lt(k, Nat.pow(2n+bq, k)) == True{} : Bool}:
27	  match k:
28	    case 0n:
29	      {==}
30	    case 1n+ +kp:
31	      +p = Nat.pow(2n+bq, kp)
32	      +q = Nat.add(p, Nat.mul(bq, p))
33	      +hp = N.lt_succ_le_succ(kp, p, pow_gt(bq, kp))
34	      +hq = N.lt_le_trans(0n, p, q, RT.pow_pos(1n+bq, kp), N.le_add_right(p, Nat.mul(bq, p)))
35	      N.lt_le_trans(1n+kp, Nat.add(1n+kp, q), Nat.add(p, q), lt_add_pos(1n+kp, q, hq), le_add_r(1n+kp, p, q, hp))
36	
37	# the loop stops at k: b^k == p <= n < p b
38	def ilog_stop(+n: Nat, +bq: Nat, +k: Nat, +p: Nat, +hp: {p == Nat.pow(2n+bq, k) : Nat}, +hpn: {Nat.is_le(p, n) == True{} : Bool}, +hu: {False{} == Nat.is_le(Nat.mul(p, 2n+bq), n) : Bool}) -> {Nat.is_le(Nat.pow(2n+bq, k), n) == True{} : Bool} & {Nat.is_lt(n, Nat.pow(2n+bq, 1n+k)) == True{} : Bool}:
39	  +b = {2n+bq : Nat}
40	  +lt = N.not_le_lt(Nat.mul(p, b), n, Equal.sym(Bool, False{}, Nat.is_le(Nat.mul(p, b), n), hu))
41	  (Equal.trans(Bool, Nat.is_le(Nat.pow(b, k), n), Nat.is_le(p, n), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.pow(b, k), p, Equal.sym(Nat, p, Nat.pow(b, k), hp)), hpn),
42	   Equal.trans(Bool, Nat.is_lt(n, Nat.mul(b, Nat.pow(b, k))), Nat.is_lt(n, Nat.mul(p, b)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(n, z), Nat.mul(b, Nat.pow(b, k)), Nat.mul(p, b), Equal.trans(Nat, Nat.mul(b, Nat.pow(b, k)), Nat.mul(b, p), Nat.mul(p, b), Equal.cong(Nat, Nat, z => Nat.mul(b, z), Nat.pow(b, k), p, Equal.sym(Nat, p, Nat.pow(b, k), hp)), A.mul_comm(b, p))), lt))
43	
44	# with no fuel left k == n, and p b <= n is impossible: n == k < p <= p b
45	def ilog_absurd(+n: Nat, +bq: Nat, +k: Nat, +p: Nat, +hp: {p == Nat.pow(2n+bq, k) : Nat}, +hu: {True{} == Nat.is_le(Nat.mul(p, 2n+bq), n) : Bool}, +hf: {k == n : Nat}) -> Empty:
46	  +b = {2n+bq : Nat}
47	  +kp = Equal.trans(Bool, Nat.is_lt(k, p), Nat.is_lt(k, Nat.pow(b, k)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(k, z), p, Nat.pow(b, k), hp), pow_gt(bq, k))
48	  +kb = N.lt_le_trans(k, p, Nat.mul(p, b), kp, RT.le_mul_pos(p, b, {==}))
49	  +kn = N.lt_le_trans(k, Nat.mul(p, b), n, kb, Equal.sym(Bool, True{}, Nat.is_le(Nat.mul(p, b), n), hu))
50	  N.lt_ne(k, n, kn, hf)
51	
52	# the loop: p == b^k <= n, up is p b <= n, fuel + k == n
53	def ilog_ok(fuel: Nat, +n: Nat, +bq: Nat, +k: Nat, +p: Nat, +up: Bool, +hp: {p == Nat.pow(2n+bq, k) : Nat}, +hpn: {Nat.is_le(p, n) == True{} : Bool}, +hup: {up == Nat.is_le(p, Nat.div(n, 2n+bq)) : Bool}, +hf: {Nat.add(fuel, k) == n : Nat}) -> {Nat.is_le(Nat.pow(2n+bq, M.ilog_go(fuel, n, 2n+bq, k, p, up)), n) == True{} : Bool} & {Nat.is_lt(n, Nat.pow(2n+bq, 1n+M.ilog_go(fuel, n, 2n+bq, k, p, up))) == True{} : Bool}:
54	  match fuel up:
55	    case 0n False{}:
56	      ilog_stop(n, bq, k, p, hp, hpn, Equal.trans(Bool, False{}, Nat.is_le(p, Nat.div(n, 2n+bq)), Nat.is_le(Nat.mul(p, 2n+bq), n), hup, R.le_div(1n+bq, p, n)))
57	    case 1n+f False{}:
58	      ilog_stop(n, bq, k, p, hp, hpn, Equal.trans(Bool, False{}, Nat.is_le(p, Nat.div(n, 2n+bq)), Nat.is_le(Nat.mul(p, 2n+bq), n), hup, R.le_div(1n+bq, p, n)))
59	    case 0n True{}:
60	      Empty.absurd({Nat.is_le(Nat.pow(2n+bq, M.ilog_go(0n, n, 2n+bq, k, p, True{})), n) == True{} : Bool} & {Nat.is_lt(n, Nat.pow(2n+bq, 1n+M.ilog_go(0n, n, 2n+bq, k, p, True{}))) == True{} : Bool}, ilog_absurd(n, bq, k, p, hp, Equal.trans(Bool, True{}, Nat.is_le(p, Nat.div(n, 2n+bq)), Nat.is_le(Nat.mul(p, 2n+bq), n), hup, R.le_div(1n+bq, p, n)), hf))
61	    case 1n+ +f True{}:
62	      +b = {2n+bq : Nat}
63	      +hu = Equal.trans(Bool, True{}, Nat.is_le(p, Nat.div(n, b)), Nat.is_le(Nat.mul(p, b), n), hup, R.le_div(1n+bq, p, n))
64	      +pb = Nat.mul(p, b)
65	      ilog_ok(f, n, bq, 1n+k, pb, Nat.is_le(pb, Nat.div(n, b)), Equal.trans(Nat, pb, Nat.mul(b, p), Nat.pow(b, 1n+k), A.mul_comm(p, b), Equal.cong(Nat, Nat, z => Nat.mul(b, z), p, Nat.pow(b, k), hp)), Equal.sym(Bool, True{}, Nat.is_le(pb, n), hu), {==}, Equal.trans(Nat, Nat.add(f, 1n+k), 1n+Nat.add(f, k), n, A.add_succ(f, k), hf))
66	
67	def lt_two(+bq: Nat) -> {Nat.is_lt(2n+bq, 2n) == False{} : Bool}:
68	  match bq:
69	    case 0n:
70	      {==}
71	    case 1n+q:
72	      {==}
73	
74	# the value ilog(n, b) returns for n >= 1, b >= 2
75	def ilog_value(+np: Nat, +bq: Nat) -> Nat:
76	  M.ilog_go(1n+np, 1n+np, 2n+bq, 0n, 1n, Nat.is_le(1n, Nat.div(1n+np, 2n+bq)))
77	
78	def ilog_done(+np: Nat, +bq: Nat) -> {M.ilog(1n+np, 2n+bq) == Done{ilog_value(np, bq)} : Result<&2, &2, M.MathError, Nat>}:
79	  %Equal.sym(Bool, Nat.is_lt(2n+bq, 2n), False{}, lt_two(bq)) : {M.ilog_ok(1n+np, 2n+bq, Bool.or(False{}, _)) == Done{ilog_value(np, bq)} : Result<&2, &2, M.MathError, Nat>}
80	  {==}
81	
82	def ilog_bounds(+np: Nat, +bq: Nat) -> {Nat.is_le(Nat.pow(2n+bq, ilog_value(np, bq)), 1n+np) == True{} : Bool} & {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+ilog_value(np, bq))) == True{} : Bool}:
83	  ilog_ok(1n+np, 1n+np, bq, 0n, 1n, Nat.is_le(1n, Nat.div(1n+np, 2n+bq)), {==}, N.lt_succ_le_succ(0n, 1n+np, {==}), {==}, A.add_zero(1n+np))
84	
85	# b^ilog(n, b) <= n   (Mathlib Nat.pow_log_le_self)
86	def fst_b(-P: Type, -Q: Type, p: P & Q) -> P:
87	  (a, b) = p
88	  a
89	
90	def snd_b(-P: Type, -Q: Type, p: P & Q) -> Q:
91	  (a, b) = p
92	  b
93	
94	def pow_ilog_le(+np: Nat, +bq: Nat) -> {Nat.is_le(Nat.pow(2n+bq, ilog_value(np, bq)), 1n+np) == True{} : Bool}:
95	  fst_b({Nat.is_le(Nat.pow(2n+bq, ilog_value(np, bq)), 1n+np) == True{} : Bool}, {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+ilog_value(np, bq))) == True{} : Bool}, ilog_bounds(np, bq))
96	
97	# n < b^(ilog(n, b) + 1)   (Mathlib Nat.lt_pow_succ_log_self)
98	def lt_pow_succ_ilog(+np: Nat, +bq: Nat) -> {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+ilog_value(np, bq))) == True{} : Bool}:
99	  snd_b({Nat.is_le(Nat.pow(2n+bq, ilog_value(np, bq)), 1n+np) == True{} : Bool}, {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+ilog_value(np, bq))) == True{} : Bool}, ilog_bounds(np, bq))
100	
101	def ilog_zero(+b: Nat) -> {M.ilog(0n, b) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}:
102	  {==}
103	
104	def or_true(+n: Nat, +b: Nat) -> {M.ilog_ok(n, b, Bool.or(Nat.is_eq(n, 0n), True{})) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}:
105	  match n:
106	    case 0n:
107	      {==}
108	    case 1n+np:
109	      {==}
110	
111	def ilog_small_base(+n: Nat, +b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {M.ilog(n, b) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}:
112	  %Equal.sym(Bool, Nat.is_lt(b, 2n), True{}, hb) : {M.ilog_ok(n, b, Bool.or(Nat.is_eq(n, 0n), _)) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}
113	  or_true(n, b)