~/bend-docscommunity

proofs/math/typed/combnat.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend as Combnat

13 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/natural.bend as S
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/arith.bend as AR2
import ../natural/bits.bend as BT
import ../natural/fact.bend as FA
import ../natural/gcd.bend as GC
import ../natural/lcm.bend as LC
import ./natfuel.bend as NF

Definitions

def true_ne_false source · line 21 · raw

@+h:{True{} == False{} : Bool} -> Empty

def le_cancel_c source · line 26 · raw

@+a:Nat -> @+b:Nat -> @+cp:Nat -> @+h:{Nat.is_le(Nat.mul(a, 1n+cp), Nat.mul(b, 1n+cp)) == True{} : Bool} -> @+d:Bool -> @+hd:{Nat.is_lt(b, a) == d : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

def le_cancel source · line 36 · raw

@+a:Nat -> @+b:Nat -> @+cp:Nat -> @+h:{Nat.is_le(Nat.mul(a, 1n+cp), Nat.mul(b, 1n+cp)) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

def sub_half source · line 42 · raw

@+i:Nat -> {Nat.sub(1n+Nat.double(i), i) == 1n+i : Nat}

1 + 2 i == i + (1 + i), so (1 + 2 i) - i == 1 + i

def cstep source · line 47 · raw

@+n:Nat -> @+i:Nat -> @+h:{Nat.is_le(1n+Nat.double(i), n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, i), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, 1n+i)) == True{} : Bool}

1 + 2 i <= n gives C(n, i) <= C(n, 1 + i)

def cmono_d source · line 56 · raw

@+n:Nat -> @+i:Nat -> @+d:Nat -> @+h:{Nat.is_le(Nat.double(Nat.add(i, d)), n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, i), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, Nat.add(i, d))) == True{} : Bool}

2 (i + d) <= n gives C(n, i) <= C(n, i + d)

def cmono source · line 70 · raw

@+n:Nat -> @+i:Nat -> @+k:Nat -> @+hi:{Nat.is_le(i, k) == True{} : Bool} -> @+hk:{Nat.is_le(Nat.double(k), n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, i), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, k)) == True{} : Bool}

i <= k, 2 k <= n give C(n, i) <= C(n, k)

def cn_mono source · line 77 · raw

@+m:Nat -> @+j:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(m, j), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(1n+m, j)) == True{} : Bool}

def cn_mono_d source · line 90 · raw

@+m:Nat -> @+d:Nat -> @+j:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(m, j), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(Nat.add(d, m), j)) == True{} : Bool}

def central source · line 97 · raw

@+i:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(i), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(Nat.double(i), i)) == True{} : Bool}

def cbig source · line 111 · raw

@+K:Nat -> @+n:Nat -> @+i:Nat -> @+hK:{Nat.is_le(K, i) == True{} : Bool} -> @+h2:{Nat.is_le(Nat.double(i), n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(n, i)) == True{} : Bool}

K <= i, 2 i <= n give 2^K <= C(n, i)

def gg source · line 120 · raw

@+c:Nat -> @+jp:Nat -> Nat

g = gcd(c, j), c == wl g, j == wr g for j = 1 + jp

def wl source · line 123 · raw

@+c:Nat -> @+jp:Nat -> Nat

def wr source · line 126 · raw

@+c:Nat -> @+jp:Nat -> Nat

def e_c source · line 129 · raw

@+c:Nat -> @+jp:Nat -> {c == Nat.mul(wl(c, jp), gg(c, jp)) : Nat}

def e_j source · line 132 · raw

@+c:Nat -> @+jp:Nat -> {1n+jp == Nat.mul(wr(c, jp), gg(c, jp)) : Nat}

def g_pos source · line 135 · raw

@+c:Nat -> @+jp:Nat -> {Nat.is_lt(0n, gg(c, jp)) == True{} : Bool}

def wr_pos source · line 138 · raw

@+c:Nat -> @+jp:Nat -> {Nat.is_lt(0n, wr(c, jp)) == True{} : Bool}

def div_c source · line 141 · raw

@+c:Nat -> @+jp:Nat -> {Nat.div(c, gg(c, jp)) == wl(c, jp) : Nat}

def div_j source · line 144 · raw

@+c:Nat -> @+jp:Nat -> {Nat.div(1n+jp, gg(c, jp)) == wr(c, jp) : Nat}

def coprime source · line 148 · raw

@+c:Nat -> @+jp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(wl(c, jp), wr(c, jp)) == 1n : Nat}

gcd(wl, wr) == 1

def cross source · line 159 · raw

@+c:Nat -> @+jp:Nat -> @+t:Nat -> @+c1:Nat -> @+e:{Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat} -> {Nat.mul(wl(c, jp), t) == Nat.mul(c1, wr(c, jp)) : Nat}

with c' (1 + jp) == c t: wl t == c' wr

def sq source · line 168 · raw

@+c:Nat -> @+jp:Nat -> @+t:Nat -> @+c1:Nat -> Nat

the quotient t / wr

def t_eq source · line 172 · raw

@+c:Nat -> @+jp:Nat -> @+t:Nat -> @+c1:Nat -> @+e:{Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat} -> {t == Nat.mul(sq(c, jp, t, c1), wr(c, jp)) : Nat}

Euclid: wr | wl t and gcd(wl, wr) == 1 give wr | t

def div_t source · line 180 · raw

@+c:Nat -> @+jp:Nat -> @+t:Nat -> @+c1:Nat -> @+e:{Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat} -> {Nat.div(t, wr(c, jp)) == sq(c, jp, t, c1) : Nat}

def prod_eq source · line 184 · raw

@+c:Nat -> @+jp:Nat -> @+t:Nat -> @+c1:Nat -> @+e:{Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat} -> {Nat.mul(wl(c, jp), sq(c, jp, t, c1)) == c1 : Nat}

(c / g) (t / (j / g)) == c'