proofs/math/natural/misc.bend
bend-collections-laws-containers@1.0.0.0 · 96 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as M
5import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/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
13def 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
16def 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
19def 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
22def 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
27def 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
36def 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
47def 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
56def 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
67def 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
78def 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
82def 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
87def 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
90def 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
94def 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)