~/bend-docscommunity

gcd.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/gcd.bend as Gcd

lib/gcd.bend -- divisibility, Bezout coprimality, Euclid's algorithm, and the theorem "if a b is a square and a, b are coprime then a is a square".

This is the bottom of the ladder that lib/pythag.bend and demos/math/fermat4.bend stand on. Two propositions carry everything:

Dvd<d, n> d divides n: a Nat k with d k = n Cop<a, b> a and b are coprime: INTEGERS u, v with u a + v b = 1

Both are Data (a record of a witness and an equation), so a proof of either can be copied with + -- unlike a computed proposition such as Nat.Le, which has to be copied in continuation-passing style.

Coprimality is Bezout's identity rather than "gcd = 1" because every use of it below is an algebraic one: Gauss's lemma (a | b c and a coprime to b give a | c) and the closure of coprimality under products are both one ring identity in Int, where "gcd = 1" would need a fresh induction each time. The integers come from lib/claims/int.bend + int_filled.bend, whose ring laws are already proven.

Euclid's algorithm is run by SUBTRACTION, not by division: gcd(a, b) with b = a + c recurses on (a, c). That keeps the whole file free of divmod (so it does not depend on lib/claims/nat_filled.bend, and inherits no TODOs), and the Bezout coefficients transport through a subtraction step with one rewrite -- u a + v c = g becomes (u - v) a + v b = g.

5 imports
import Base
import ./nat.bend as N
import ./sqrt2.bend as S2
import ./int.bend as I
import ./int_filled.bend as IF

Types

type Dvd source · line 111 · raw

@-d:Nat -> @-n:Nat -> Data

type Cop source · line 204 · raw

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

type Bez source · line 385 · raw

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

type Split source · line 650 · raw

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

Split<a, b>: a common divisor 1+gp of a and b whose cofactors are COPRIME. That is the only property of a greatest common divisor this file uses.

type IsSq source · line 705 · raw

@-n:Nat -> Data

Definitions

def gc.mul_zero_l source · line 38 · raw

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

a (1+b) = 0 forces a = 0

def gc.mul_eq_one source · line 46 · raw

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

a b = 1 forces a = 1

def gc.succ_pos source · line 65 · raw

@+a:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, 1n+a)

a positive number is not zero

def gc.iadd_mul source · line 73 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+z:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(x, y), z) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(x, z), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(y, z)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

(x + y) z = x z + y z

def gc.imul_swap source · line 80 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+z:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(x, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(y, z)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(y, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(x, z)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

x (y z) = y (x z)

def gc.imul_shift source · line 86 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+z:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(x, y), z) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(x, z), y) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

(x y) z = (x z) y

def gc.iadd_swap source · line 92 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+z:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(x, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(y, z)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(y, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(x, z)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

x + (y + z) = y + (x + z)

def gc.ione_mul source · line 98 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n}, x) == x : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

1 x = x

def gc.abs_pos source · line 104 · raw

@n:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{n}) == n : Nat}

the absolute value of Pos{n} is n, which is what carries an Int equation back into Nat: abs(Pos{n}) = abs(Pos{d} * x) = d * abs(x)

def gc.dvd_refl source · line 114 · raw

@+d:Nat -> Dvd<d, d>

def gc.dvd_one source · line 117 · raw

@+n:Nat -> Dvd<1n, n>

def gc.dvd_zero source · line 120 · raw

@d:Nat -> Dvd<d, 0n>

def gc.dvd_eq source · line 124 · raw

@-d:Nat -> @-n:Nat -> @-m:Nat -> @e:{n == m : Nat} -> @h:Dvd<d, n> -> Dvd<d, m>

n = m carries d | n to d | m

def gc.dvd_trans source · line 129 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @h1:Dvd<a, b> -> @h2:Dvd<b, c> -> Dvd<a, c>

d | n and n | c give d | c

def gc.dvd_mul_r source · line 144 · raw

@+d:Nat -> @+n:Nat -> @+m:Nat -> @h:Dvd<d, n> -> Dvd<d, Nat.mul(n, m)>

d | n gives d | n m

def gc.dvd_mul_l source · line 155 · raw

@+d:Nat -> @+n:Nat -> @+m:Nat -> @h:Dvd<d, n> -> Dvd<d, Nat.mul(m, n)>

d | n gives d | m n

def gc.dvd_add source · line 159 · raw

@+d:Nat -> @+x:Nat -> @+y:Nat -> @h1:Dvd<d, x> -> @h2:Dvd<d, y> -> Dvd<d, Nat.add(x, y)>

d | x and d | y give d | x + y

def gc.dvd_pos source · line 174 · raw

@d:Nat -> @+n:Nat -> @h:Dvd<d, 1n+n> -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, d)

a divisor of a positive number is positive

def gc.dvd_le.go source · line 184 · raw

@+d:Nat -> @+n:Nat -> @k:Nat -> @e:{Nat.mul(d, k) == 1n+n : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(d, 1n+n)

a divisor of a positive number is at most it

def gc.dvd_le source · line 195 · raw

@+d:Nat -> @+n:Nat -> @h:Dvd<d, 1n+n> -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(d, 1n+n)

def gc.cop_sym source · line 207 · raw

@+a:Nat -> @+b:Nat -> @c:Cop<a, b> -> Cop<b, a>

def gc.cop_one source · line 217 · raw

@b:Nat -> Cop<1n, b>

1 is coprime to everything

def gc.cop_eq_r source · line 220 · raw

@-a:Nat -> @-b:Nat -> @-c:Nat -> @e:{b == c : Nat} -> @h:Cop<a, b> -> Cop<a, c>

def gc.cop_eq_l source · line 224 · raw

@-a:Nat -> @-b:Nat -> @-c:Nat -> @e:{a == b : Nat} -> @h:Cop<a, c> -> Cop<b, c>

def gc.cop_dvd_l.go source · line 230 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+t:Nat -> @et:{Nat.mul(c, t) == a : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Cop<c, b>

a divisor of a is coprime to whatever a is coprime to: a = c t and u a + v b = 1 give (u t) c + v b = 1

def gc.cop_dvd_l source · line 238 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @hc:Cop<a, b> -> @hd:Dvd<c, a> -> Cop<c, b>

def gc.cop_common.go source · line 247 · raw

@+a:Nat -> @+b:Nat -> @+w:Nat -> @+s:Nat -> @+t:Nat -> @es:{Nat.mul(w, s) == a : Nat} -> @et:{Nat.mul(w, t) == b : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> {w == 1n : Nat}

a common divisor of a coprime pair is 1: a = w s, b = w t and u a + v b = 1 give w (u s + v t) = 1, so w = 1

def gc.cop_common source · line 261 · raw

@+a:Nat -> @+b:Nat -> @+w:Nat -> @hc:Cop<a, b> -> @d1:Dvd<w, a> -> @d2:Dvd<w, b> -> {w == 1n : Nat}

def gc.imul_rot source · line 271 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+z:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(x, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(y, z)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(y, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(z, x)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

x (y z) = y (z x)

def gc.gauss.mid source · line 283 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+k:Nat -> @ek:{Nat.mul(a, k) == Nat.mul(b, c) : Nat} -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{k})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{c}, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

a k = b c turns a (v k) into c (v b)

def gc.gauss.key source · line 292 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+k:Nat -> @ek:{Nat.mul(a, k) == Nat.mul(b, c) : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{c}, u), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{k}))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{c} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

the Int identity behind Gauss's lemma

def gc.gauss.go source · line 300 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+k:Nat -> @ek:{Nat.mul(a, k) == Nat.mul(b, c) : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Dvd<a, c>

def gc.gauss source · line 308 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @hc:Cop<a, b> -> @hd:Dvd<a, Nat.mul(b, c)> -> Dvd<a, c>

def gc.bez_l1 source · line 320 · raw

@+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+u2:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, b), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u2, a)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, u2), b), a) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def gc.bez_l2 source · line 324 · raw

@+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v2:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+c:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, b), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v2, c)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, v2), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(b, c)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def gc.bez_prod source · line 329 · raw

@+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+u2:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v2:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+c:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, b)), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u2, a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v2, c))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u2, a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v2, c))), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, u2), b)), a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, v2), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(b, c))) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def gc.cop_mul.go source · line 350 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+u2:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v2:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h1:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> @h2:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u2, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v2, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{c})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Cop<a, Nat.mul(b, c)>

def gc.cop_mul source · line 364 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @hb:Cop<a, b> -> @hc:Cop<a, c> -> Cop<a, Nat.mul(b, c)>

def gc.cop_sq source · line 372 · raw

@+a:Nat -> @+b:Nat -> @h:Cop<a, b> -> Cop<a, Nat.mul(b, b)>

a coprime to b is coprime to b squared

def gc.bez_eq_r source · line 389 · raw

@-a:Nat -> @-b:Nat -> @-c:Nat -> @e:{b == c : Nat} -> @z:Bez<a, b> -> Bez<a, c>

def gc.bez_sym source · line 393 · raw

@+a:Nat -> @+b:Nat -> @z:Bez<a, b> -> Bez<b, a>

def gc.bez_step source · line 403 · raw

@+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+xa:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+xc:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.sub(u, v), xa), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(xa, xc))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, xa), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, xc)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

(u - v) A + v (A + C) = u A + v C : the whole content of a subtraction step

def gc.bez_up source · line 444 · raw

@+a:Nat -> @+c:Nat -> @z:Bez<a, c> -> Bez<a, Nat.add(a, c)>

from a common divisor of (a, c), one of (a, a + c)

def gc.bez_refl source · line 459 · raw

@+a:Nat -> Bez<a, a>

1 a + 0 a = a

def gc.split_lt.open source · line 466 · raw

@-ap:Nat -> @-bp:Nat -> @-P:Type -> @k:(@d:Nat -> @e:{Nat.add(1n+ap, d) == bp : Nat} -> P) -> @w:(&d:Nat -> {Nat.add(1n+ap, d) == bp : Nat}) -> P

a < b gives b = (1+a) + d

def gc.split_lt source · line 470 · raw

@+ap:Nat -> @+bp:Nat -> @lt:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(ap, bp) -> @-P:Type -> @k:(@d:Nat -> @e:{Nat.add(1n+ap, d) == bp : Nat} -> P) -> P

def gc.euclid.go source · line 477 · raw

@f:Nat -> @ap:Nat -> @bp:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(ap, bp), f) -> Bez<1n+ap, 1n+bp>

THE ALGORITHM. The fuel is ap + bp and every step strictly lowers it: with a < b the pair (a, b) becomes (a, b - a), and with b < a the pair is turned round first. Both non-trivial branches are one bez_up, so the Bezout bookkeeping is written once.

def gc.euclid source · line 527 · raw

@ap:Nat -> @bp:Nat -> Bez<1n+ap, 1n+bp>

def gc.nmul_swap source · line 537 · raw

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

def gc.nmul_shift source · line 542 · raw

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

def gc.nsq_prod source · line 547 · raw

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

def gc.ncancel_r source · line 552 · raw

@+m:Nat -> @x:Nat -> @y:Nat -> @e:{Nat.mul(x, 1n+m) == Nat.mul(y, 1n+m) : Nat} -> {x == y : Nat}

def gc.ncancel source · line 570 · raw

@+m:Nat -> @+x:Nat -> @+y:Nat -> @e:{Nat.mul(1n+m, x) == Nat.mul(1n+m, y) : Nat} -> {x == y : Nat}

def gc.pos_of_mul source · line 577 · raw

@g:Nat -> @+k:Nat -> @+ap:Nat -> @e:{Nat.mul(g, k) == 1n+ap : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, g)

a factor of a positive product is positive

def gc.pos_of_mul_r source · line 584 · raw

@+g:Nat -> @+k:Nat -> @+ap:Nat -> @e:{Nat.mul(g, k) == 1n+ap : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, k)

def gc.pos_shape source · line 587 · raw

@g:Nat -> @p:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, g) -> @-P:Type -> @k:(@gp:Nat -> @e:{g == 1n+gp : Nat} -> P) -> P

def gc.pnat source · line 599 · raw

@z:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Nat

def gc.pos_ne_zero source · line 606 · raw

@+gp:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n+gp} == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{0n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Empty

def gc.ineg_add source · line 609 · raw

@+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.neg(y), y) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{0n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def gc.isub_zero source · line 613 · raw

@+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @e:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(x, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.neg(y)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{0n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> {x == y : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def gc.icancel source · line 626 · raw

@+gp:Nat -> @+x:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+y:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @e:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n+gp}, x) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n+gp}, y) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> {x == y : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def gc.dist2 source · line 641 · raw

@+a:Nat -> @+b:Nat -> @+w:Nat -> @+s:Nat -> @+t:Nat -> @es:{Nat.mul(w, s) == a : Nat} -> @et:{Nat.mul(w, t) == b : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{w}, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{s}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{t}))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

w (u s + v t) = u (w s) + v (w t)

def gc.split.go source · line 656 · raw

@+a:Nat -> @+b:Nat -> @+gp:Nat -> @+k1:Nat -> @+k2:Nat -> @e1:{Nat.mul(1n+gp, k1) == a : Nat} -> @e2:{Nat.mul(1n+gp, k2) == b : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n+gp} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Split<a, b>

def gc.split.mk source · line 667 · raw

@+a:Nat -> @+b:Nat -> @g:Nat -> @k1:Nat -> @k2:Nat -> @e1:{Nat.mul(g, k1) == a : Nat} -> @e2:{Nat.mul(g, k2) == b : Nat} -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{a}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{g} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> @pos:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, g) -> Split<a, b>

def gc.split_of.fin source · line 674 · raw

@+ap:Nat -> @+b:Nat -> @+g:Nat -> @ga:Dvd<g, 1n+ap> -> @gb:Dvd<g, b> -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n+ap}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{b})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{g} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Split<1n+ap, b>

def gc.split_of source · line 683 · raw

@+ap:Nat -> @+b:Nat -> @z:Bez<1n+ap, b> -> Split<1n+ap, b>

def gc.split source · line 688 · raw

@ap:Nat -> @bp:Nat -> Split<1n+ap, 1n+bp>

def gc.ncancel_pos source · line 708 · raw

@+x:Nat -> @+y:Nat -> @m:Nat -> @pos:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, m) -> @e:{Nat.mul(m, x) == Nat.mul(m, y) : Nat} -> {x == y : Nat}

def gc.sq_fin source · line 715 · raw

@+av:Nat -> @+b:Nat -> @+a1:Nat -> @+c1:Nat -> @+gp:Nat -> @+w:Nat -> @+ea:{Nat.mul(1n+gp, a1) == 1n+av : Nat} -> @ew:{Nat.mul(a1, w) == 1n+gp : Nat} -> @key1:{Nat.mul(a1, b) == Nat.mul(1n+gp, Nat.mul(c1, c1)) : Nat} -> @hc:Cop<1n+av, b> -> IsSq<1n+av>

def gc.sq_open source · line 738 · raw

@+av:Nat -> @+b:Nat -> @+a1:Nat -> @+c1:Nat -> @+gp:Nat -> @ea:{Nat.mul(1n+gp, a1) == 1n+av : Nat} -> @key1:{Nat.mul(a1, b) == Nat.mul(1n+gp, Nat.mul(c1, c1)) : Nat} -> @hc:Cop<1n+av, b> -> @dw:Dvd<a1, 1n+gp> -> IsSq<1n+av>

def gc.sq_main2 source · line 743 · raw

@+av:Nat -> @+b:Nat -> @+cv:Nat -> @+gp:Nat -> @+a1:Nat -> @+c1:Nat -> @+ea:{Nat.mul(1n+gp, a1) == 1n+av : Nat} -> @ec:{Nat.mul(1n+gp, c1) == 1n+cv : Nat} -> @hcop:Cop<a1, c1> -> @hc:Cop<1n+av, b> -> @e:{Nat.mul(1n+av, b) == Nat.mul(1n+cv, 1n+cv) : Nat} -> IsSq<1n+av>

def gc.sq_main source · line 761 · raw

@+av:Nat -> @+b:Nat -> @+cv:Nat -> @hc:Cop<1n+av, b> -> @e:{Nat.mul(1n+av, b) == Nat.mul(1n+cv, 1n+cv) : Nat} -> @sp:Split<1n+av, 1n+cv> -> IsSq<1n+av>

def gc.sq_of_cop source · line 767 · raw

@+av:Nat -> @+b:Nat -> @c:Nat -> @hc:Cop<1n+av, b> -> @e:{Nat.mul(1n+av, b) == Nat.mul(c, c) : Nat} -> IsSq<1n+av>

a b = c^2 with a, b coprime and a positive makes a a square

def gc.le_mul_l source · line 786 · raw

@+c:Nat -> @+x:Nat -> @+y:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, y) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.mul(c, x), Nat.mul(c, y))

def gc.le_mul_cancel_l.no source · line 794 · raw

@+dp:Nat -> @+a:Nat -> @+b:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.mul(1n+dp, a), Nat.mul(1n+dp, b)) -> @lt:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(b, a) -> Empty

def gc.le_mul_cancel_l source · line 803 · raw

@+dp:Nat -> @+a:Nat -> @+b:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.mul(1n+dp, a), Nat.mul(1n+dp, b)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b)

def gc.dvd_sub.fin source · line 809 · raw

@+dp:Nat -> @+x:Nat -> @+y:Nat -> @+s:Nat -> @+bb:Nat -> @+aa:Nat -> @eB:{Nat.mul(1n+dp, bb) == x : Nat} -> @eA:{Nat.mul(1n+dp, aa) == s : Nat} -> @e:{Nat.add(x, y) == s : Nat} -> @+t:Nat -> @et:{Nat.add(bb, t) == aa : Nat} -> Dvd<1n+dp, y>

d | x and d | x + y give d | y

def gc.dvd_sub.open source · line 820 · raw

@+dp:Nat -> @+x:Nat -> @+y:Nat -> @+s:Nat -> @+bb:Nat -> @+aa:Nat -> @eB:{Nat.mul(1n+dp, bb) == x : Nat} -> @eA:{Nat.mul(1n+dp, aa) == s : Nat} -> @e:{Nat.add(x, y) == s : Nat} -> @w:(&t:Nat -> {Nat.add(bb, t) == aa : Nat}) -> Dvd<1n+dp, y>

def gc.dvd_sub.pos source · line 824 · raw

@+dp:Nat -> @+x:Nat -> @+y:Nat -> @+s:Nat -> @+bb:Nat -> @+aa:Nat -> @+eB:{Nat.mul(1n+dp, bb) == x : Nat} -> @+eA:{Nat.mul(1n+dp, aa) == s : Nat} -> @+e:{Nat.add(x, y) == s : Nat} -> Dvd<1n+dp, y>

def gc.dvd_sub.mk source · line 833 · raw

@d:Nat -> @+x:Nat -> @+y:Nat -> @+s:Nat -> @+bb:Nat -> @+aa:Nat -> @+eB:{Nat.mul(d, bb) == x : Nat} -> @+eA:{Nat.mul(d, aa) == s : Nat} -> @+e:{Nat.add(x, y) == s : Nat} -> Dvd<d, y>

def gc.dvd_sub source · line 843 · raw

@+d:Nat -> @+x:Nat -> @+y:Nat -> @+s:Nat -> @+e:{Nat.add(x, y) == s : Nat} -> @d1:Dvd<d, x> -> @d2:Dvd<d, s> -> Dvd<d, y>

def gc.cop_intro.go source · line 855 · raw

@+up:Nat -> @+vp:Nat -> @k:(@g:Nat -> @d1:Dvd<g, 1n+up> -> @d2:Dvd<g, 1n+vp> -> {g == 1n : Nat}) -> @gp:Nat -> @u1:Nat -> @v1:Nat -> @ea:{Nat.mul(1n+gp, u1) == 1n+up : Nat} -> @eb:{Nat.mul(1n+gp, v1) == 1n+vp : Nat} -> @hcop:Cop<u1, v1> -> Cop<1n+up, 1n+vp>

def gc.cop_intro.op source · line 875 · raw

@+up:Nat -> @+vp:Nat -> @k:(@g:Nat -> @d1:Dvd<g, 1n+up> -> @d2:Dvd<g, 1n+vp> -> {g == 1n : Nat}) -> @sp:Split<1n+up, 1n+vp> -> Cop<1n+up, 1n+vp>

def gc.cop_intro source · line 880 · raw

@+up:Nat -> @+vp:Nat -> @k:(@g:Nat -> @d1:Dvd<g, 1n+up> -> @d2:Dvd<g, 1n+vp> -> {g == 1n : Nat}) -> Cop<1n+up, 1n+vp>

def gc.cop_sq2 source · line 887 · raw

@+a:Nat -> @+b:Nat -> @h:Cop<a, b> -> Cop<Nat.mul(a, a), Nat.mul(b, b)>

def gc.cop_of_sq.go source · line 892 · raw

@+a:Nat -> @+b:Nat -> @+u:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+v:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(u, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{Nat.mul(a, a)}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(v, 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{Nat.mul(b, b)})) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{1n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int} -> Cop<a, b>

def gc.cop_of_sq source · line 900 · raw

@+a:Nat -> @+b:Nat -> @h:Cop<Nat.mul(a, a), Nat.mul(b, b)> -> Cop<a, b>

def gc.sq_inj.no source · line 906 · raw

@+a:Nat -> @+b:Nat -> @e:{Nat.mul(a, a) == Nat.mul(b, b) : Nat} -> @lt:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(a, b) -> Empty

squares are injective: a^2 = b^2 forces a = b

def gc.sq_inj source · line 916 · raw

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

def gc.sq_dvd.fin source · line 926 · raw

@+ap:Nat -> @+bp:Nat -> @+gp:Nat -> @+a1:Nat -> @+b1:Nat -> @+ea:{Nat.mul(1n+gp, a1) == 1n+ap : Nat} -> @+eb:{Nat.mul(1n+gp, b1) == 1n+bp : Nat} -> @hcop:Cop<a1, b1> -> @+k:Nat -> @ek:{Nat.mul(Nat.mul(1n+ap, 1n+ap), k) == Nat.mul(1n+bp, 1n+bp) : Nat} -> Dvd<1n+ap, 1n+bp>

a^2 | b^2 forces a | b: with G = gcd(a, b), a = G a1, b = G b1 and gcd(a1, b1) = 1, cancelling G^2 leaves a1^2 | b1^2, and a1^2 is a common divisor of the coprime pair a1^2, b1^2, so a1 = 1 and a = G divides b.

def gc.sq_dvd.op source · line 956 · raw

@+ap:Nat -> @+bp:Nat -> @sp:Split<1n+ap, 1n+bp> -> @h:Dvd<Nat.mul(1n+ap, 1n+ap), Nat.mul(1n+bp, 1n+bp)> -> Dvd<1n+ap, 1n+bp>

def gc.sq_dvd source · line 963 · raw

@+ap:Nat -> @+bp:Nat -> @h:Dvd<Nat.mul(1n+ap, 1n+ap), Nat.mul(1n+bp, 1n+bp)> -> Dvd<1n+ap, 1n+bp>

def gc.sq_dvd_pos source · line 967 · raw

@a:Nat -> @pa:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, a) -> @b:Nat -> @pb:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, b) -> @h:Dvd<Nat.mul(a, a), Nat.mul(b, b)> -> Dvd<a, b>

the same with positivity as a hypothesis rather than a shape