1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/logic.bend as L
4	import ../../../src/math/natural.bend as M
5	import ./arith.bend as R
6	
7	# divmod and clamp. divmod(a, b) is (a // b, a % b) with a == q b + r and
8	# r < b (Mathlib Nat.div_add_mod, Nat.mod_lt; Python divmod), ZeroDivision
9	# for b == 0; clamp(x, lo, hi) lies in [lo, hi] and is x when x already
10	# does (C++ std::clamp, Rust Ord::clamp; the reference's clamp, section
11	# 10), Domain for hi < lo.
12	
13	def divmod_done(+a: Nat, +bp: Nat) -> {M.divmod(a, 1n+bp) == Done{M.QR{Nat.div(a, 1n+bp), Nat.mod(a, 1n+bp)}} : Result<&2, &2, M.MathError, M.QuotRem>}:
14	  {==}
15	
16	def divmod_eq(+a: Nat, +bp: Nat) -> {a == Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) : Nat}:
17	  R.dm_eq(bp, a)
18	
19	def divmod_lt(+a: Nat, +bp: Nat) -> {Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp) == True{} : Bool}:
20	  R.dm_lt(bp, a)
21	
22	def divmod_zero(+a: Nat) -> {M.divmod(a, 0n) == Fail{M.ZeroDivision{}} : Result<&2, &2, M.MathError, M.QuotRem>}:
23	  {==}
24	
25	# ---- max and min ----
26	
27	def le_max_r(+x: Nat, +lo: Nat) -> {Nat.is_le(lo, Nat.max(x, lo)) == True{} : Bool}:
28	  match x lo:
29	    case 0n l0:
30	      N.le_refl(l0)
31	    case 1n+xp 0n:
32	      {==}
33	    case 1n+ +xp 1n+ +lp:
34	      le_max_r(xp, lp)
35	
36	def max_eq_l(+x: Nat, +lo: Nat, +h: {Nat.is_le(lo, x) == True{} : Bool}) -> {Nat.max(x, lo) == x : Nat}:
37	  match x lo:
38	    case 0n 0n:
39	      {==}
40	    case 0n 1n+lp:
41	      Empty.absurd({Nat.max(0n, 1n+lp) == 0n : Nat}, L.false_true(h))
42	    case 1n+xp 0n:
43	      {==}
44	    case 1n+ +xp 1n+ +lp:
45	      N.succ_cong(Nat.max(xp, lp), xp, max_eq_l(xp, lp, h))
46	
47	def min_le_r(+y: Nat, +hi: Nat) -> {Nat.is_le(Nat.min(y, hi), hi) == True{} : Bool}:
48	  match y hi:
49	    case 0n h0:
50	      N.zero_le(h0)
51	    case 1n+yp 0n:
52	      {==}
53	    case 1n+ +yp 1n+ +hp:
54	      min_le_r(yp, hp)
55	
56	def le_min(+lo: Nat, +y: Nat, +hi: Nat, +h1: {Nat.is_le(lo, y) == True{} : Bool}, +h2: {Nat.is_le(lo, hi) == True{} : Bool}) -> {Nat.is_le(lo, Nat.min(y, hi)) == True{} : Bool}:
57	  match lo y hi:
58	    case 0n y0 h0:
59	      N.zero_le(Nat.min(y0, h0))
60	    case 1n+lp 0n h0:
61	      Empty.absurd({Nat.is_le(1n+lp, Nat.min(0n, h0)) == True{} : Bool}, L.false_true(h1))
62	    case 1n+lp 1n+yp 0n:
63	      Empty.absurd({Nat.is_le(1n+lp, Nat.min(1n+yp, 0n)) == True{} : Bool}, L.false_true(h2))
64	    case 1n+ +lp 1n+ +yp 1n+ +hp:
65	      le_min(lp, yp, hp, h1, h2)
66	
67	def min_eq_l(+y: Nat, +hi: Nat, +h: {Nat.is_le(y, hi) == True{} : Bool}) -> {Nat.min(y, hi) == y : Nat}:
68	  match y hi:
69	    case 0n h0:
70	      {==}
71	    case 1n+yp 0n:
72	      Empty.absurd({Nat.min(1n+yp, 0n) == 1n+yp : Nat}, L.false_true(h))
73	    case 1n+ +yp 1n+ +hp:
74	      N.succ_cong(Nat.min(yp, hp), yp, min_eq_l(yp, hp, h))
75	
76	# ---- clamp ----
77	
78	def clamp_done(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_le(lo, hi) == True{} : Bool}) -> {M.clamp(x, lo, hi) == Done{Nat.min(Nat.max(x, lo), hi)} : Result<&2, &2, M.MathError, Nat>}:
79	  %Equal.sym(Bool, Nat.is_lt(hi, lo), False{}, N.le_not_lt(hi, lo, h)) : {M.clamp_ok(x, lo, hi, _) == Done{Nat.min(Nat.max(x, lo), hi)} : Result<&2, &2, M.MathError, Nat>}
80	  {==}
81	
82	def clamp_domain(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_lt(hi, lo) == True{} : Bool}) -> {M.clamp(x, lo, hi) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}:
83	  %Equal.sym(Bool, Nat.is_lt(hi, lo), True{}, h) : {M.clamp_ok(x, lo, hi, _) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}
84	  {==}
85	
86	# lo <= clamp and clamp <= hi
87	def clamp_ge(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_le(lo, hi) == True{} : Bool}) -> {Nat.is_le(lo, Nat.min(Nat.max(x, lo), hi)) == True{} : Bool}:
88	  le_min(lo, Nat.max(x, lo), hi, le_max_r(x, lo), h)
89	
90	def clamp_le(+x: Nat, +lo: Nat, +hi: Nat) -> {Nat.is_le(Nat.min(Nat.max(x, lo), hi), hi) == True{} : Bool}:
91	  min_le_r(Nat.max(x, lo), hi)
92	
93	# x in [lo, hi] is left alone
94	def clamp_id(+x: Nat, +lo: Nat, +hi: Nat, +h1: {Nat.is_le(lo, x) == True{} : Bool}, +h2: {Nat.is_le(x, hi) == True{} : Bool}) -> {Nat.min(Nat.max(x, lo), hi) == x : Nat}:
95	  %Equal.sym(Nat, Nat.max(x, lo), x, max_eq_l(x, lo, h1)) : {Nat.min(_, hi) == x : Nat}
96	  min_eq_l(x, hi, h2)