~/bend-docscommunity

mathlib.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/mathlib.bend as Mathlib

Arithmetic for the proofs: addition, multiplication, equality, squares.

2 imports
import Base
import ./nat.bend as N

Definitions

def add source · line 6 · raw

@a:Nat -> @b:Nat -> Nat

def mul source · line 13 · raw

@a:Nat -> @+b:Nat -> Nat

def nat_eq source · line 20 · raw

@a:Nat -> @b:Nat -> Bool

def sq source · line 35 · raw

@+a:Nat -> Nat

def pow source · line 38 · raw

@+a:Nat -> @e:Nat -> Nat

def pythag source · line 47 · raw

@a:Nat -> @b:Nat -> @c:Nat -> Bool

Pythagoras, as a definition: a right triangle is a triple whose hypotenuse squared is the sum of the squared sides.

def sum_to source · line 51 · raw

@n:Nat -> Nat

1 + 2 + … + n

def sym source · line 64 · raw

@-A:Type -> @-a:A -> @-b:A -> @e:{a == b : A} -> {b == a : A}

def add_zero source · line 68 · raw

@a:Nat -> {add(a, 0n) == a : Nat}

def add_succ source · line 76 · raw

@a:Nat -> @b:Nat -> {add(a, 1n+b) == 1n+add(a, b) : Nat}

def pick source · line 86 · raw

@-A:Type -> @c:Bool -> @a:A -> @b:A -> A

def nat_le source · line 93 · raw

@a:Nat -> @b:Nat -> Bool

def msub_go source · line 106 · raw

@b:Nat -> @a:Nat -> Nat

subtraction that matches its second argument first, so that msub(x, 0) and msub(2+x, 2) normalize even for symbolic x

def msub source · line 117 · raw

@a:Nat -> @b:Nat -> Nat

def mod_go source · line 121 · raw

@f:Nat -> @+n:Nat -> @+d:Nat -> Nat

n mod d, by repeated subtraction (fuel keeps it structural)

def mod source · line 128 · raw

@+n:Nat -> @+d:Nat -> Nat

def divides source · line 131 · raw

@+d:Nat -> @+n:Nat -> Bool

def has_divisor source · line 135 · raw

@+n:Nat -> @k:Nat -> Bool

does any d with 2 ≤ d ≤ k divide n?

def is_prime source · line 147 · raw

@+n:Nat -> Bool

def mersenne source · line 151 · raw

@p:Nat -> Nat

the p-th Mersenne number, 2^p − 1

def or_true source · line 161 · raw

@b:Bool -> {Bool.or(b, True{}) == True{} : Bool}

def double source · line 168 · raw

@n:Nat -> Nat

def double_add source · line 175 · raw

@y:Nat -> {double(y) == add(y, y) : Nat}

def mul2_double source · line 185 · raw

@+m:Nat -> {mul(2n, m) == double(m) : Nat}

def mod2_zero source · line 189 · raw

@x:Nat -> @g:Nat -> {mod_go(1n+add(x, g), double(x), 2n) == 0n : Nat}

def divides2_double source · line 196 · raw

@+y:Nat -> {divides(2n, double(1n+y)) == True{} : Bool}

def has2 source · line 201 · raw

@k:Nat -> @+m:Nat -> @e:{divides(2n, m) == True{} : Bool} -> {has_divisor(m, 2n+k) == True{} : Bool}

def use_shape source · line 211 · raw

@-n:Nat -> @w:(&x:Nat -> {pow(2n, 2n+n) == double(2n+x) : Nat}) -> @-P:Type -> @k:(@x:Nat -> @e:{pow(2n, 2n+n) == double(2n+x) : Nat} -> P) -> P

def pow2_shape source · line 218 · raw

@n:Nat -> &x:Nat -> {pow(2n, 2n+n) == double(2n+x) : Nat}

every 2^(2+n) is double(2+x) for some x

def add_bridge source · line 241 · raw

@a:Nat -> @-b:Nat -> {add(a, b) == Nat.add(a, b) : Nat}

def mul_bridge source · line 248 · raw

@a:Nat -> @+b:Nat -> {mul(a, b) == Nat.mul(a, b) : Nat}

def nat_eq_true source · line 257 · raw

@a:Nat -> @b:Nat -> @e:{a == b : Nat} -> {nat_eq(a, b) == True{} : Bool}

def nat_eq_false source · line 268 · raw

@a:Nat -> @b:Nat -> @ne:(@_:{a == b : Nat} -> Empty) -> {nat_eq(a, b) == False{} : Bool}

def sqrt2_carry source · line 279 · raw

@+p:Nat -> @+q:Nat -> @e:{mul(1n+p, 1n+p) == mul(2n, mul(1n+q, 1n+q)) : Nat} -> {Nat.mul(1n+p, 1n+p) == Nat.mul(2n, Nat.mul(1n+q, 1n+q)) : Nat}