proofs/math/natural/lists.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists.bend as Lists

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 ./gcd.bend as G
import ./lcm.bend as LC
import ../../../spec/math/natural.bend as S

Definitions

def sum_go source · line 20 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sum_go(xs, acc) == Nat.add(acc, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.lsum(xs)) : Nat}

def sum_ok source · line 27 · raw

@+xs:List<&2, Nat> -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sum(xs) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.lsum(xs) : Nat}

def prod_go source · line 30 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.prod_go(xs, acc) == Nat.mul(acc, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.lprod(xs)) : Nat}

def prod_ok source · line 37 · raw

@+xs:List<&2, Nat> -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.prod(xs) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.lprod(xs) : Nat}

def nth0 source · line 42 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> @+d:Nat -> Nat

def dvd_with source · line 46 · raw

@+d:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> Type

d divides every element: xs[i] == ks[i] d

def mul_with source · line 50 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> Type

m is a multiple of every element: m == ks[i] xs[i]

def dvd_trans source · line 54 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+k1:Nat -> @+k2:Nat -> @+e1:{a == Nat.mul(k1, b) : Nat} -> @+e2:{b == Nat.mul(k2, c) : Nat} -> {a == Nat.mul(Nat.mul(k1, k2), c) : Nat}

(a == k1 b and b == k2 c) gives a == (k1 k2) c

def gw_acc source · line 58 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> Nat

the quotient acc / gcd_all_go(xs, acc)

def g_acc source · line 65 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> {acc == Nat.mul(gw_acc(xs, acc), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_all_go(xs, acc)) : Nat}

def gw_nth source · line 73 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> @+i:Nat -> Nat

the quotient (xs[i]) / gcd_all_go(xs, acc)

def g_nth source · line 82 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> @+i:Nat -> {nth0(xs, i, 0n) == Nat.mul(gw_nth(xs, acc, i), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_all_go(xs, acc)) : Nat}

def gcd_all_dvd source · line 92 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> {nth0(xs, i, 0n) == Nat.mul(gw_nth(xs, 0n, i), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_all(xs)) : Nat}

gcd_all(xs) divides every element: xs[i] == k gcd_all(xs) (0 past the end) (Mathlib Finset.gcd_dvd)

def gw_dvd source · line 96 · raw

@+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @+acc:Nat -> @+ka:Nat -> Nat

the quotient gcd_all_go(xs, acc) / d for a common divisor d

def g_dvd source · line 107 · raw

@+d:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @+acc:Nat -> @+ka:Nat -> @+ea:{acc == Nat.mul(ka, d) : Nat} -> @h:dvd_with(d, xs, ks) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_all_go(xs, acc) == Nat.mul(gw_dvd(xs, ks, acc, ka), d) : Nat}

def dvd_gcd_all source · line 120 · raw

@+d:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @h:dvd_with(d, xs, ks) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_all(xs) == Nat.mul(gw_dvd(xs, ks, 0n, 0n), d) : Nat}

every common divisor of the elements divides gcd_all(xs) (Mathlib Finset.dvd_gcd)

def lw_acc source · line 125 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> Nat

def l_acc source · line 132 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm_all_go(xs, acc) == Nat.mul(lw_acc(xs, acc), acc) : Nat}

def lw_nth source · line 139 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> @+i:Nat -> Nat

def l_nth source · line 148 · raw

@+xs:List<&2, Nat> -> @+acc:Nat -> @+i:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm_all_go(xs, acc) == Nat.mul(lw_nth(xs, acc, i), nth0(xs, i, 1n)) : Nat}

def dvd_lcm_all source · line 158 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm_all(xs) == Nat.mul(lw_nth(xs, 1n, i), nth0(xs, i, 1n)) : Nat}

every element divides lcm_all(xs) (1 past the end) (Mathlib Finset.dvd_lcm)

def lw_mul source · line 161 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @+acc:Nat -> @+ka:Nat -> Nat

def l_mul source · line 172 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @+acc:Nat -> @+ka:Nat -> @+ea:{m == Nat.mul(ka, acc) : Nat} -> @h:mul_with(m, xs, ks) -> {m == Nat.mul(lw_mul(m, xs, ks, acc, ka), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm_all_go(xs, acc)) : Nat}

def lcm_all_dvd source · line 185 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @h:mul_with(m, xs, ks) -> {m == Nat.mul(lw_mul(m, xs, ks, 1n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm_all(xs)) : Nat}

lcm_all(xs) divides every common multiple of the elements (Mathlib Finset.lcm_dvd)