sqrt2.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/sqrt2.bend as Sqrt2

lib/sqrt2.bend -- the square root of 2 is irrational, from lib/nat.bend.

The statement is about naturals, as it has been since Euclid: there are no p, q with (1+p)^2 = 2 (1+q)^2 (the 1+ rules out zero). The proof is the classical descent -- (1+p)^2 is even, so 1+p is even, say 2k; then (1+q)^2 = 2 k^2 is the same equation with a smaller pair -- run down a fuel that bounds p, since Bend's recursion must shrink a Nat.

2 imports

import Base
import ./nat.bend as N

Definitions

def Nat.sq_double source · line 13 · raw

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

2 k^2 counted twice: (2k)^2 = 2 (2 k^2)

def Nat.le_copy source · line 23 · raw

@a:Nat -> @b:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> @-P:Type -> @k:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> @_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> P) -> P

a <= b implies a^2 <= b^2. The hypothesis is spent three times per step, and an order proof is not Data, so a CPS copier hands out replicas.

def Nat.le_sq.step source · line 34 · raw

@+p:Nat -> @+q:Nat -> @h1:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(p, q) -> @h2:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(p, q) -> @ih:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.mul(p, p), Nat.mul(q, q)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(p, Nat.mul(p, 1n+p)), Nat.add(q, Nat.mul(q, 1n+q)))

def Nat.le_sq source · line 39 · raw

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

def Nat.le_double source · line 54 · raw

@a:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, Nat.double(a))

def Nat.is_lt_false source · line 63 · raw

@a:Nat -> @b:Nat -> @e:{Nat.is_lt(a, b) == False{} : Bool} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(b, a)

deciding a < b at run time, reflected into the two propositions

def Nat.decide_lt.go source · line 74 · raw

@a:Nat -> @b:Nat -> @c:Bool -> @e:{Nat.is_lt(a, b) == c : Bool} -> @-P:Type -> @lt:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(a, b) -> P) -> @ge:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(b, a) -> P) -> P

def Nat.decide_lt source · line 81 · raw

@+a:Nat -> @+b:Nat -> @-P:Type -> @lt:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(a, b) -> P) -> @ge:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(b, a) -> P) -> P

def Nat.sqrt2.lt.ge source · line 85 · raw

@+p:Nat -> @+q:Nat -> @e:{Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat} -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+p, 1n+q) -> Empty

if (1+p)^2 = 2 (1+q)^2 then 1+q < 1+p: otherwise (1+p)^2 <= (1+q)^2 < 2 (1+q)^2

def Nat.sqrt2.lt source · line 92 · raw

@+p:Nat -> @+q:Nat -> @e:{Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(1n+q, 1n+p)

def Nat.sqrt2.even source · line 96 · raw

@+p:Nat -> @+q:Nat -> @e:{Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+p) == True{} : Bool}

(1+p)^2 even, so 1+p even

def Nat.sqrt2.step source · line 105 · raw

@g:Nat -> @+p:Nat -> @+q:Nat -> @k:Nat -> @hk:{1n+p == Nat.double(k) : Nat} -> @+e:{Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat} -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(p, 1n+g) -> @rec:(@q2:Nat -> @j:Nat -> @b:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(q2, g) -> @e2:{Nat.mul(1n+q2, 1n+q2) == Nat.double(Nat.mul(1n+j, 1n+j)) : Nat} -> Empty) -> Empty

the descent step, with 1+p = double(k) in hand: k = 1+j, and then (1+q)^2 = double((1+j)^2) with 1+q < 1+p, so the fuel drops

def Nat.sqrt2.go source · line 121 · raw

@f:Nat -> @p:Nat -> @+q:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(p, f) -> @+e:{Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat} -> Empty

def Nat.sqrt2_irrational source · line 139 · raw

@+p:Nat -> @+q:Nat -> @e:{Nat.mul(1n+p, 1n+p) == Nat.mul(2n, Nat.mul(1n+q, 1n+q)) : Nat} -> Empty

THE THEOREM: no (1+p)^2 equals 2 (1+q)^2