~/bend-docscommunity

pythag.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/pythag.bend as Pythag

lib/pythag.bend -- primitive Pythagorean triples, on top of lib/gcd.bend.

THE THEOREM (Pyth, at the bottom of the file). If

A^2 + B^2 = C^2, A, B, C > 0, gcd(A, B) = 1, B even

then there are m > n > 0, coprime, with

A + n^2 = m^2 (i.e. A = m^2 - n^2) B = 2 m n C = m^2 + n^2

Everything is stated additively, so no truncated subtraction is ever needed: "A = m^2 - n^2" is "A + n^2 = m^2", and the two halves of C - A and C + A arrive as witnesses.

The proof: A and C are odd (A because it is coprime to the even B, C because C^2 = A^2 + B^2 is odd), so C - A and C + A are even; write C = A + 2u and v = A + u, so that u + v = C and u + A = v. Expanding C^2 = (A + 2u)^2 in A^2 + B^2 = C^2 leaves B^2 = 4 u v, and B = 2k gives k^2 = u v. A common divisor of u and v divides u + v = C and v - u = A, and gcd(A, C) = 1 (a common divisor of A and C divides C^2 - A^2 = B^2, and gcd(A^2, B^2) = 1), so u and v are coprime. The square theorem of lib/gcd.bend then makes u = n^2 and v = m^2, and the three identities above fall out.

The file also proves the ONE congruence fact the descent needs: odd^2 + odd^2 is never a square (mod 4 it would be 2). It is used twice in demos/math/fermat4.bend -- once to see that x and y cannot both be odd, and once to see that the smaller leg of the second triple is even.

4 imports
import Base
import ./nat.bend as N
import ./sqrt2.bend as S2
import ./gcd.bend as G

Types

type Pyth source · line 406 · raw

@-xa:Nat -> @-xb:Nat -> @-xc:Nat -> Data

Definitions

def py.double_dist source · line 42 · raw

@+x:Nat -> @+y:Nat -> {Nat.add(Nat.double(x), Nat.double(y)) == Nat.double(Nat.add(x, y)) : Nat}

2x + 2y = 2(x + y)

def py.mul_double source · line 49 · raw

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

a (2b) = 2(ab)

def py.double_mul source · line 55 · raw

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

(2a) b = 2(ab)

def py.not_false source · line 66 · raw

@b:Bool -> @e:{Bool.not(b) == False{} : Bool} -> {b == True{} : Bool}

def py.not_true source · line 73 · raw

@b:Bool -> @e:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

def py.dvd2_of_even source · line 80 · raw

@+n:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(n) == True{} : Bool} -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<2n, n>

def py.even_shape source · line 86 · raw

@+n:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(n) == True{} : Bool} -> @-P:Type -> @k:(@a:Nat -> @h:{n == Nat.double(a) : Nat} -> P) -> P

def py.odd_shape source · line 89 · raw

@n:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(n) == False{} : Bool} -> @-P:Type -> @k:(@a:Nat -> @h:{n == 1n+Nat.double(a) : Nat} -> P) -> P

def py.sq_odd source · line 105 · raw

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

(1 + 2a)^2 = 1 + 4(a + a^2)

def py.odd_odd.core source · line 120 · raw

@+a:Nat -> @+b:Nat -> @+w:Nat -> @e:{Nat.add(Nat.mul(1n+Nat.double(a), 1n+Nat.double(a)), Nat.mul(1n+Nat.double(b), 1n+Nat.double(b))) == Nat.mul(Nat.double(w), Nat.double(w)) : Nat} -> Empty

def py.odd_odd.fin source · line 146 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> @+a:Nat -> @+b:Nat -> @+w:Nat -> @hx:{x == 1n+Nat.double(a) : Nat} -> @hy:{y == 1n+Nat.double(b) : Nat} -> @hz:{z == Nat.double(w) : Nat} -> @e:{Nat.add(Nat.mul(x, x), Nat.mul(y, y)) == Nat.mul(z, z) : Nat} -> Empty

def py.odd_odd source · line 156 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> @+ex:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(x) == False{} : Bool} -> @+ey:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(y) == False{} : Bool} -> @+e:{Nat.add(Nat.mul(x, x), Nat.mul(y, y)) == Nat.mul(z, z) : Nat} -> Empty

THE CONGRUENCE FACT: x and y odd makes x^2 + y^2 no square.

def py.expand.inner source · line 181 · raw

@+xa:Nat -> @+u:Nat -> {Nat.add(Nat.mul(xa, Nat.double(u)), Nat.add(Nat.mul(Nat.double(u), xa), Nat.mul(Nat.double(u), Nat.double(u)))) == Nat.double(Nat.double(Nat.mul(u, Nat.add(xa, u)))) : Nat}

def py.expand source · line 222 · raw

@+xa:Nat -> @+u:Nat -> {Nat.mul(Nat.add(xa, Nat.double(u)), Nat.add(xa, Nat.double(u))) == Nat.add(Nat.mul(xa, xa), Nat.double(Nat.double(Nat.mul(u, Nat.add(xa, u))))) : Nat}

def py.same_false source · line 259 · raw

@x:Bool -> @e:{0xd5e9362591c1667c9894b781190e1ac9/nat.Bool.same(False{}, x) == False{} : Bool} -> {x == True{} : Bool}

def py.lt_add_pos source · line 266 · raw

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

def py.sq_lt source · line 271 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @hsq:{Nat.add(Nat.mul(1n+av, 1n+av), Nat.mul(1n+bv, 1n+bv)) == Nat.mul(1n+cv, 1n+cv) : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(Nat.mul(1n+av, 1n+av), Nat.mul(1n+cv, 1n+cv))

A^2 < C^2, because B^2 is positive

def py.lt_of_sq source · line 276 · raw

@+a:Nat -> @+c:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(Nat.mul(a, a), Nat.mul(c, c)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(a, c)

and therefore A < C

def py.oddA.go source · line 284 · raw

@+av:Nat -> @+bv:Nat -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+bv> -> @hbe:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+bv) == True{} : Bool} -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == c : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == False{} : Bool}

A is odd: 2 would otherwise divide both A and the even B

def py.oddA source · line 295 · raw

@+av:Nat -> @+bv:Nat -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+bv> -> @hbe:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+bv) == True{} : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == False{} : Bool}

def py.oddC source · line 299 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @hsq:{Nat.add(Nat.mul(1n+av, 1n+av), Nat.mul(1n+bv, 1n+bv)) == Nat.mul(1n+cv, 1n+cv) : Nat} -> @exA:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == False{} : Bool} -> @hbe:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+bv) == True{} : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+cv) == False{} : Bool}

C is odd: C^2 = A^2 + B^2 is odd + even

def py.get_u.go source · line 316 · raw

@+av:Nat -> @+cv:Nat -> @exA:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == False{} : Bool} -> @exC:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+cv) == False{} : Bool} -> @+t:Nat -> @+ht:{Nat.add(2n+av, t) == 1n+cv : Nat} -> @-P:Type -> @k:(@up:Nat -> @hu:{Nat.add(1n+av, Nat.double(1n+up)) == 1n+cv : Nat} -> P) -> P

C - A is even and positive: C = A + 2(1+up)

def py.get_u.open source · line 337 · raw

@+av:Nat -> @+cv:Nat -> @exA:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == False{} : Bool} -> @exC:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+cv) == False{} : Bool} -> @-P:Type -> @k:(@up:Nat -> @hu:{Nat.add(1n+av, Nat.double(1n+up)) == 1n+cv : Nat} -> P) -> @w:(&t:Nat -> {Nat.add(2n+av, t) == 1n+cv : Nat}) -> P

def py.get_u source · line 341 · raw

@+av:Nat -> @+cv:Nat -> @hlt:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(1n+av, 1n+cv) -> @exA:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+av) == False{} : Bool} -> @exC:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+cv) == False{} : Bool} -> @-P:Type -> @k:(@up:Nat -> @hu:{Nat.add(1n+av, Nat.double(1n+up)) == 1n+cv : Nat} -> P) -> P

def py.copAC.k source · line 346 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @+hsq:{Nat.add(Nat.mul(1n+av, 1n+av), Nat.mul(1n+bv, 1n+bv)) == Nat.mul(1n+cv, 1n+cv) : Nat} -> @+hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+bv> -> @+g:Nat -> @d1:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<g, 1n+av> -> @d2:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<g, 1n+cv> -> {g == 1n : Nat}

gcd(A, C) = 1: a common divisor of A and C divides A^2 and C^2, hence also B^2 = C^2 - A^2, and A^2, B^2 are coprime

def py.copAC source · line 354 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @+hsq:{Nat.add(Nat.mul(1n+av, 1n+av), Nat.mul(1n+bv, 1n+bv)) == Nat.mul(1n+cv, 1n+cv) : Nat} -> @+hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+bv> -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+cv>

def py.copUV.k source · line 358 · raw

@+av:Nat -> @+cv:Nat -> @+up:Nat -> @+huv:{Nat.add(1n+up, Nat.add(1n+av, 1n+up)) == 1n+cv : Nat} -> @+cAC:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+cv> -> @+g:Nat -> @d1:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<g, 1n+up> -> @d2:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<g, Nat.add(1n+av, 1n+up)> -> {g == 1n : Nat}

gcd(u, v) = 1: a common divisor of u and v divides u + v = C and v - u = A

def py.copUV source · line 366 · raw

@+av:Nat -> @+cv:Nat -> @+up:Nat -> @+huv:{Nat.add(1n+up, Nat.add(1n+av, 1n+up)) == 1n+cv : Nat} -> @+cAC:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+cv> -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+up, Nat.add(1n+av, 1n+up)>

def py.bsq source · line 370 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @+up:Nat -> @hsq:{Nat.add(Nat.mul(1n+av, 1n+av), Nat.mul(1n+bv, 1n+bv)) == Nat.mul(1n+cv, 1n+cv) : Nat} -> @hu:{Nat.add(1n+av, Nat.double(1n+up)) == 1n+cv : Nat} -> {Nat.mul(1n+bv, 1n+bv) == Nat.double(Nat.double(Nat.mul(1n+up, Nat.add(1n+av, 1n+up)))) : Nat}

B^2 = 4 u v

def py.kk source · line 380 · raw

@+av:Nat -> @+bv:Nat -> @+up:Nat -> @+k:Nat -> @hk:{1n+bv == Nat.double(k) : Nat} -> @hb:{Nat.mul(1n+bv, 1n+bv) == Nat.double(Nat.double(Nat.mul(1n+up, Nat.add(1n+av, 1n+up)))) : Nat} -> {Nat.mul(k, k) == Nat.mul(1n+up, Nat.add(1n+av, 1n+up)) : Nat}

k^2 = u v, where B = 2k

def py.sq_pos.go source · line 390 · raw

@+target:Nat -> @s:Nat -> @+h:{Nat.mul(s, s) == 1n+target : Nat} -> @-P:Type -> @k:(@sv:Nat -> @hs:{Nat.mul(1n+sv, 1n+sv) == 1n+target : Nat} -> P) -> P

reading a square root off IsSq, in 1+ form

def py.sq_pos source · line 397 · raw

@+target:Nat -> @sq:0xd5e9362591c1667c9894b781190e1ac9/gcd.IsSq<1n+target> -> @-P:Type -> @k:(@sv:Nat -> @hs:{Nat.mul(1n+sv, 1n+sv) == 1n+target : Nat} -> P) -> P

def py.pyth.fin source · line 413 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @+up:Nat -> @+k:Nat -> @+nv:Nat -> @+mv:Nat -> @+hn:{Nat.mul(1n+nv, 1n+nv) == 1n+up : Nat} -> @+hm:{Nat.mul(1n+mv, 1n+mv) == Nat.add(1n+av, 1n+up) : Nat} -> @hcuv:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+up, Nat.add(1n+av, 1n+up)> -> @hk:{1n+bv == Nat.double(k) : Nat} -> @hkk:{Nat.mul(k, k) == Nat.mul(1n+up, Nat.add(1n+av, 1n+up)) : Nat} -> @huv:{Nat.add(1n+up, Nat.add(1n+av, 1n+up)) == 1n+cv : Nat} -> Pyth<1n+av, 1n+bv, 1n+cv>

def py.pyth source · line 451 · raw

@+av:Nat -> @+bv:Nat -> @+cv:Nat -> @+hsq:{Nat.add(Nat.mul(1n+av, 1n+av), Nat.mul(1n+bv, 1n+bv)) == Nat.mul(1n+cv, 1n+cv) : Nat} -> @+hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+bv> -> @+hbe:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+bv) == True{} : Bool} -> Pyth<1n+av, 1n+bv, 1n+cv>

A^2 + B^2 = C^2 with A, B, C > 0, gcd(A, B) = 1 and B even

def py.pyth_pos source · line 486 · raw

@a:Nat -> @pa:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, a) -> @b:Nat -> @pb:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, b) -> @c:Nat -> @pc:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, c) -> @+hsq:{Nat.add(Nat.mul(a, a), Nat.mul(b, b)) == Nat.mul(c, c) : Nat} -> @+hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<a, b> -> @+hbe:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(b) == True{} : Bool} -> Pyth<a, b, c>

the same theorem with positivity as a hypothesis rather than a shape, which is how the descent meets it