proofs/math/number/egcd.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend as Egcd

6 imports

import Base
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ../../../src/math/number.bend as NB
import ../../../spec/math/number.bend as SN
import ../natural/arith.bend as R

Definitions

def up_gcd source · line 16 · raw

@+q:Nat -> @r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EGcd -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_gcd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.eg_up(q, r)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_gcd(r) : Nat}

def gcd_go source · line 21 · raw

@+f:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_gcd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.egcd_go(f, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_go(f, a, b) : Nat}

def egcd_gcd source · line 31 · raw

@+a:Nat -> @+b:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.Egcd.gcd(a, b)

def qby source · line 37 · raw

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

(q b) y == b (q y)

def spread source · line 42 · raw

@+q:Nat -> @+b:Nat -> @+r:Nat -> @+y:Nat -> {Nat.mul(Nat.add(Nat.mul(q, b), r), y) == Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)) : Nat}

(q b + r) y == b (q y) + r y

def alg_pos source · line 48 · raw

@+g:Nat -> @+x:Nat -> @+y:Nat -> @+q:Nat -> @+b:Nat -> @+r:Nat -> @+ih:{Nat.mul(b, x) == Nat.add(g, Nat.mul(r, y)) : Nat} -> {Nat.mul(b, Nat.add(x, Nat.mul(q, y))) == Nat.add(g, Nat.mul(Nat.add(Nat.mul(q, b), r), y)) : Nat}

child b x == g + r y gives b (x + q y) == g + (q b + r) y

def alg_neg source · line 56 · raw

@+g:Nat -> @+x:Nat -> @+y:Nat -> @+q:Nat -> @+b:Nat -> @+r:Nat -> @+ih:{Nat.mul(r, y) == Nat.add(g, Nat.mul(b, x)) : Nat} -> {Nat.mul(Nat.add(Nat.mul(q, b), r), y) == Nat.add(g, Nat.mul(b, Nat.add(x, Nat.mul(q, y)))) : Nat}

child r y == g + b x gives (q b + r) y == g + b (x + q y)

def base source · line 65 · raw

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

the base case: a * 1 == a + b * 0

def up_sign source · line 70 · raw

@+a:Nat -> @+b:Nat -> @+q:Nat -> @+r:Nat -> @+ha:{a == Nat.add(Nat.mul(q, b), r) : Nat} -> @+g:Nat -> @+x:Nat -> @+y:Nat -> @+neg:Bool -> @+ih:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_pos(b, r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EG{g, x, y, neg}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_neg(b, r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EG{g, x, y, neg}) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_pos(a, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.eg_up(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EG{g, x, y, neg})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_neg(a, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.eg_up(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EG{g, x, y, neg})) : Nat}

def up_bez source · line 81 · raw

@+a:Nat -> @+b:Nat -> @+q:Nat -> @+r:Nat -> @+ha:{a == Nat.add(Nat.mul(q, b), r) : Nat} -> @c:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.EGcd -> @+ih:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_pos(b, r, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_neg(b, r, c) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_pos(a, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.eg_up(q, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_neg(a, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.eg_up(q, c)) : Nat}

one level up: from the child's identity for (b, r) to the parent's for (a, b), a == q b + r

def split source · line 87 · raw

@+a:Nat -> @+bp:Nat -> {a == Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) : Nat}

a == (a div b) b + a mod b

def bez_go source · line 90 · raw

@+f:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_pos(a, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.egcd_go(f, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.eg_neg(a, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.egcd_go(f, a, b)) : Nat}

def egcd_bezout source · line 99 · raw

@+a:Nat -> @+b:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.Egcd.bezout(a, b)