mathlib.bend source

mathlib.bend on the hub · documented module

import Baseimport ./bits.bend as Bitsimport ./math.bend as Mathimport ./num.bend as Nmimport ./rat.bend as Rtimport ./set.bend as Seimport ./series.bend as Srimport ./mlib_linalg.bend as M2# Mathlib.bend — Lean Mathlib finite-fragment facade over this repo.## What this is: a single publishable entry point that maps the translatable# part of Lean's Mathlib to Bend2 definitions in this repo. See# MATHLIB_COVERAGE.md for the full area-by-area table (have / missing /# impossible). Anything about reals, topology, measure, or infinite# structures is honestly out of scope (Bend2 has only Nat/U32/F32; F32 is# axiomatic and unprovable; see README + BEND2_GAP_ANALYSIS.md).## What this file does:# - thin Mathlib-named wrappers (mlib_*) over existing checked defs#   (no re-proofs, no redefinitions — import and call);# - one U32 smoke checksum (mlib_selftest) combining one closed value#   from each wrapped area, so `bend mathlib.bend` normalizes it;# - closed-instance laws with definitional proofs ({==}).## Publish: `bend mathlib.bend --publish` (bundles this file + its imports).# --- wrappers (names are globally unique by mlib_ prefix) ---def mlib_pop(+x: U32) -> U32:  Bits.pop(x)def mlib_pow(+base: U32, +exp: U32) -> U32:  Math.pow_u32(base, exp)def mlib_gcd(+a: U32, +b: U32) -> U32:  Math.gcd(a, b)def mlib_is_prime(+n: U32) -> Bool:  Nm.is_prime(n)def mlib_mod_pow(+base: U32, +exp: U32, +m: U32) -> U32:  Nm.mod_pow(base, exp, m)def mlib_trisum_u32(n: Nat) -> U32:  U32.from_nat(Sr.trisum(n))def mlib_radd_num(a: Rt.Rat, b: Rt.Rat) -> U32:  Rt.num_of(Rt.radd(a, b))def mlib_mat_det_u32(m: M2.Mat2) -> U32:  U32.from_nat(M2.mmat_det(m))def mlib_set_size(s: Se.USet) -> U32:  Se.ssize(s)# --- smoke checksum: one closed value per area (expected 324) ---# 3 (pop) + 243 (pow) + 4 (gcd) + 1 (modpow) + 2 (set) + 55 (trisum)#   + 1 (prime) + 5 (rat 1/2+1/3=5/6 num) + 10 (mat det) = 324.def mlib_selftest() -> U32:  a = Bits.pop(7)  b = Math.pow_u32(3, 5)  c = Math.gcd(12, 8)  d = Nm.mod_pow(3, 4, 5)  e = Se.ssize(Se.sinsert(Se.sinsert(Se.sempty(), 1), 2))  f = U32.from_nat(Sr.trisum(10n))  g = Bool.to_u32(Nm.is_prime(7))  h = Rt.num_of(Rt.radd(Rt.mk_rat(False{}, 1, 2), Rt.mk_rat(False{}, 1, 3)))  i = U32.from_nat(M2.mmat_det(M2.mmat_example()))  (a + b + c + d + e + f + g + h + i : U32)# --- closed laws (all definitional) ---law mlib_pop_7:  {mlib_pop(7) == 3 : U32}def mlib_pop_7():  {==}law mlib_pow_3_5:  {mlib_pow(3, 5) == 243 : U32}def mlib_pow_3_5():  {==}law mlib_gcd_12_8:  {mlib_gcd(12, 8) == 4 : U32}def mlib_gcd_12_8():  {==}law mlib_prime_7:  {mlib_is_prime(7) == True{} : Bool}def mlib_prime_7():  {==}law mlib_modpow_345:  {mlib_mod_pow(3, 4, 5) == 1 : U32}def mlib_modpow_345():  {==}law mlib_trisum_10:  {mlib_trisum_u32(10n) == 55 : U32}def mlib_trisum_10():  {==}law mlib_radd_1_2_1_3_num:  {mlib_radd_num(Rt.mk_rat(False{}, 1, 2), Rt.mk_rat(False{}, 1, 3)) == 5 : U32}def mlib_radd_1_2_1_3_num():  {==}law mlib_mat_det_example:  {mlib_mat_det_u32(M2.mmat_example()) == 10 : U32}def mlib_mat_det_example():  {==}law mlib_set_size_two:  {mlib_set_size(Se.sinsert(Se.sinsert(Se.sempty(), 1), 2)) == 2 : U32}def mlib_set_size_two():  {==}law mlib_selftest_value:  {mlib_selftest() == 324 : U32}def mlib_selftest_value():  {==}