proofs/math/natural/fact.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend as Fact

8 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ./arith.bend as R
import ./lcm.bend as LC
import ../../../spec/math/natural.bend as S

Definitions

def mul_left_comm source · line 20 · raw

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

(x a) f == a (x f)

def factorial_go source · line 25 · raw

@+n:Nat -> @+acc:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.factorial_go(n, acc) == Nat.mul(acc, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(n)) : Nat}

def factorial_ok source · line 33 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.factorial(n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(n) : Nat}

factorial(n) == n!

def pos_mul source · line 36 · raw

@+p:Nat -> @+f:Nat -> @+h:{Nat.is_lt(0n, f) == True{} : Bool} -> {Nat.is_lt(0n, Nat.mul(1n+p, f)) == True{} : Bool}

def factorial_pos source · line 44 · raw

@+n:Nat -> {Nat.is_lt(0n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(n)) == True{} : Bool}

0 < n! (Mathlib Nat.factorial_pos)

def desc_succ source · line 54 · raw

@+m:Nat -> @+j:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(1n+m, 1n+j) == Nat.mul(1n+m, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(m, j)) : Nat}

(1+m).desc(1+j) == (1+m) * m.desc(j) (Mathlib Nat.succ_descFactorial_succ)

def desc_front source · line 63 · raw

@+m:Nat -> @+j:Nat -> {Nat.mul(m, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(Nat.sub(m, 1n), j)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(m, 1n+j) : Nat}

m * (m - 1).desc(j) == m.desc(1+j), the order perm multiplies in

def perm_go source · line 71 · raw

@+k:Nat -> @+m:Nat -> @+acc:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.perm_go(k, m, acc) == Nat.mul(acc, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(m, k)) : Nat}

def perm_ok source · line 81 · raw

@+n:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.perm(n, k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(n, k) : Nat}

perm(n, k) == n.descFactorial(k)

def desc_self source · line 85 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(n, n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(n) : Nat}

n.desc(n) == n! (Mathlib Nat.descFactorial_self)

def sub_lt_succ source · line 93 · raw

@+n:Nat -> @+j:Nat -> @+h:{Nat.is_lt(j, n) == True{} : Bool} -> {Nat.sub(n, j) == 1n+Nat.sub(n, 1n+j) : Nat}

j < n gives n - j == 1 + (n - (1 + j))

def factorial_mul_desc source · line 103 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, n) == True{} : Bool} -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(Nat.sub(n, k)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(n, k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(n) : Nat}

(n - k)! * n.desc(k) == n! (Mathlib Nat.factorial_mul_descFactorial)

def choose_zero_right source · line 121 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, 0n) == 1n : Nat}

def choose_one_right source · line 129 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, 1n) == n : Nat}

C(n, 1) == n

def succ_mul_choose source · line 138 · raw

@+n:Nat -> @+k:Nat -> {Nat.mul(1n+n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k)) == Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(1n+n, 1n+k), 1n+k) : Nat}

(n + 1) C(n, k) == C(n + 1, k + 1) (k + 1) (Mathlib Nat.add_one_mul_choose_eq)

def mul_sub_left source · line 164 · raw

@+a:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mul(a, Nat.sub(x, y)) == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}

a (x - y) == a x - a y

def choose_succ_right source · line 171 · raw

@+n:Nat -> @+k:Nat -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, 1n+k), 1n+k) == Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k), Nat.sub(n, k)) : Nat}

C(n, k + 1) (k + 1) == C(n, k) (n - k) (Mathlib Nat.choose_succ_right_eq)

def choose_mul_factorial source · line 182 · raw

@+n:Nat -> @+k:Nat -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.desc(n, k) : Nat}

C(n, k) k! == n.desc(k) (Mathlib Nat.descFactorial_eq_factorial_mul_choose)

def choose_eq_zero source · line 195 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_lt(n, k) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k) == 0n : Nat}

n < k gives C(n, k) == 0 (Mathlib Nat.choose_eq_zero_of_lt)

def pos_pos source · line 205 · raw

@+a:Nat -> @+b:Nat -> @+ha:{Nat.is_lt(0n, a) == True{} : Bool} -> @+hb:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.is_lt(0n, Nat.mul(a, b)) == True{} : Bool}

def choose_mul_facts source · line 213 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, n) == True{} : Bool} -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(Nat.sub(n, k)))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.factorial(n) : Nat}

C(n, k) (k! (n - k)!) == n! (Mathlib Nat.choose_mul_factorial_mul_factorial)

def sub_sub_self source · line 220 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, n) == True{} : Bool} -> {Nat.sub(n, Nat.sub(n, k)) == k : Nat}

n - (n - k) == k for k <= n

def sub_le_self source · line 226 · raw

@+n:Nat -> @+k:Nat -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}

def choose_symm source · line 237 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, Nat.sub(n, k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k) : Nat}

C(n, n - k) == C(n, k) (Mathlib Nat.choose_symm)

def comb_go source · line 251 · raw

@+j:Nat -> @+n:Nat -> @+i:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.comb_go(j, n, i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, i)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, Nat.add(i, j)) : Nat}

every r_i is C(n, i), so each division is exact

def comb_min source · line 261 · raw

@+n:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(k, Nat.sub(n, k)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, Nat.min(k, Nat.sub(n, k))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k) : Nat}

def comb_small source · line 268 · raw

@+n:Nat -> @+k:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(n, k) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.comb_small(n, k, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k) : Nat}

def comb_ok source · line 278 · raw

@+n:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.comb(n, k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.choose(n, k) : Nat}

comb(n, k) == C(n, k)