sqrt2.bend source
sqrt2.bend on the hub · documented module
# 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.import Baseimport ./nat.bend as N# 2 k^2 counted twice: (2k)^2 = 2 (2 k^2)def Nat.sq_double(+k: Nat) -> {Nat.mul(Nat.double(k), Nat.double(k)) == Nat.double(Nat.double(Nat.mul(k, k))) : Nat}: %Equal.sym(Nat, Nat.double(k), Nat.add(k, k), N.Nat.double_add(k)) : {Nat.mul(_, _) == Nat.double(Nat.double(Nat.mul(k, k))) : Nat} %Equal.sym(Nat, Nat.double(Nat.double(Nat.mul(k, k))), Nat.add(Nat.double(Nat.mul(k, k)), Nat.double(Nat.mul(k, k))), N.Nat.double_add(Nat.double(Nat.mul(k, k)))) : {Nat.mul(Nat.add(k, k), Nat.add(k, k)) == _ : Nat} %Equal.sym(Nat, Nat.double(Nat.mul(k, k)), Nat.add(Nat.mul(k, k), Nat.mul(k, k)), N.Nat.double_add(Nat.mul(k, k))) : {Nat.mul(Nat.add(k, k), Nat.add(k, k)) == Nat.add(_, _) : Nat} %Equal.sym(Nat, Nat.mul(Nat.add(k, k), Nat.add(k, k)), Nat.add(Nat.mul(k, Nat.add(k, k)), Nat.mul(k, Nat.add(k, k))), N.Nat.add_mul(k, k, Nat.add(k, k))) : {_ == Nat.add(Nat.add(Nat.mul(k, k), Nat.mul(k, k)), Nat.add(Nat.mul(k, k), Nat.mul(k, k))) : Nat} %Equal.sym(Nat, Nat.mul(k, Nat.add(k, k)), Nat.add(Nat.mul(k, k), Nat.mul(k, k)), N.Nat.mul_add(k, k, k)) : {Nat.add(_, _) == Nat.add(Nat.add(Nat.mul(k, k), Nat.mul(k, k)), Nat.add(Nat.mul(k, k), Nat.mul(k, k))) : Nat} {==}# 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_copy(a: Nat, b: Nat, h: N.Nat.Le(a, b), -P: Type, k: N.Nat.Le(a, b) -> N.Nat.Le(a, b) -> P) -> P: match a: case 0n: k(Unit{}, Unit{}) case 1n+p: match b: case 0n: match h: case 1n+q: Nat.le_copy(p, q, h, P, k)def Nat.le_sq.step(+p: Nat, +q: Nat, h1: N.Nat.Le(p, q), h2: N.Nat.Le(p, q), ih: N.Nat.Le(Nat.mul(p, p), Nat.mul(q, q))) -> N.Nat.Le(Nat.add(p, Nat.mul(p, 1n+p)), Nat.add(q, Nat.mul(q, 1n+q))): %Equal.sym(Nat, Nat.mul(p, 1n+p), Nat.add(p, Nat.mul(p, p)), N.Nat.mul_succ(p, p)) : N.Nat.Le(Nat.add(p, _), Nat.add(q, Nat.mul(q, 1n+q))) %Equal.sym(Nat, Nat.mul(q, 1n+q), Nat.add(q, Nat.mul(q, q)), N.Nat.mul_succ(q, q)) : N.Nat.Le(Nat.add(p, Nat.add(p, Nat.mul(p, p))), Nat.add(q, _)) N.Nat.le_add_both(p, q, Nat.add(p, Nat.mul(p, p)), Nat.add(q, Nat.mul(q, q)), h1, N.Nat.le_add_both(p, q, Nat.mul(p, p), Nat.mul(q, q), h2, ih))def Nat.le_sq(a: Nat, b: Nat, h: N.Nat.Le(a, b)) -> N.Nat.Le(Nat.mul(a, a), Nat.mul(b, b)): match a: case 0n: Unit{} case 1n+p: match b: case 0n: match h: case 1n+q: +p2 = p +q2 = q Nat.le_copy(p2, q2, h, N.Nat.Le(Nat.mul(1n+p2, 1n+p2), Nat.mul(1n+q2, 1n+q2)), h1 => h2 => Nat.le_copy(p2, q2, h2, N.Nat.Le(Nat.mul(1n+p2, 1n+p2), Nat.mul(1n+q2, 1n+q2)), h3 => h4 => Nat.le_sq.step(p2, q2, h1, h3, Nat.le_sq(p2, q2, h4))))def Nat.le_double(a: Nat) -> N.Nat.Le(a, Nat.double(a)): match a: case 0n: Unit{} case 1n+p: +p2 = p N.Nat.le_succ(p2, Nat.double(p2), Nat.le_double(p2))# deciding a < b at run time, reflected into the two propositionsdef Nat.is_lt_false(a: Nat, b: Nat, e: {Nat.is_lt(a, b) == False{} : Bool}) -> N.Nat.Le(b, a): match a b: case 0n 0n: Unit{} case 0n 1n+q: N.Bool.true_ne_false(e) case 1n+p 0n: Unit{} case 1n+p 1n+q: Nat.is_lt_false(p, q, e)def Nat.decide_lt.go(a: Nat, b: Nat, c: Bool, e: {Nat.is_lt(a, b) == c : Bool}, -P: Type, lt: N.Nat.Lt(a, b) -> P, ge: N.Nat.Le(b, a) -> P) -> P: match c: case True{}: lt(N.Nat.is_lt_true(a, b, e)) case False{}: ge(Nat.is_lt_false(a, b, e))def Nat.decide_lt(+a: Nat, +b: Nat, -P: Type, lt: N.Nat.Lt(a, b) -> P, ge: N.Nat.Le(b, a) -> P) -> P: Nat.decide_lt.go(a, b, Nat.is_lt(a, b), {==}, P, lt, ge)# if (1+p)^2 = 2 (1+q)^2 then 1+q < 1+p: otherwise (1+p)^2 <= (1+q)^2 < 2 (1+q)^2def Nat.sqrt2.lt.ge(+p: Nat, +q: Nat, e: {Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat}, h: N.Nat.Le(1n+p, 1n+q)) -> Empty: N.Nat.lt_irrefl(Nat.mul(1n+q, 1n+q), N.Nat.le_trans(1n+Nat.mul(1n+q, 1n+q), Nat.mul(1n+p, 1n+p), Nat.mul(1n+q, 1n+q), %Equal.sym(Nat, Nat.mul(1n+p, 1n+p), Nat.double(Nat.mul(1n+q, 1n+q)), e) : N.Nat.Le(1n+Nat.mul(1n+q, 1n+q), _) Nat.le_double(Nat.add(q, Nat.mul(q, 1n+q))), Nat.le_sq(1n+p, 1n+q, h)))def Nat.sqrt2.lt(+p: Nat, +q: Nat, e: {Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat}) -> N.Nat.Lt(1n+q, 1n+p): Nat.decide_lt(1n+q, 1n+p, N.Nat.Lt(1n+q, 1n+p), lt => lt, ge => Empty.absurd(N.Nat.Lt(1n+q, 1n+p), Nat.sqrt2.lt.ge(p, q, e, ge)))# (1+p)^2 even, so 1+p evendef Nat.sqrt2.even(+p: Nat, +q: Nat, e: {Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat}) -> {N.Nat.even(1n+p) == True{} : Bool}: Equal.trans(Bool, N.Nat.even(1n+p), N.Nat.even(Nat.mul(1n+p, 1n+p)), True{}, Equal.sym(Bool, N.Nat.even(Nat.mul(1n+p, 1n+p)), N.Nat.even(1n+p), N.Nat.even_sq(1n+p)), Equal.trans(Bool, N.Nat.even(Nat.mul(1n+p, 1n+p)), N.Nat.even(Nat.double(Nat.mul(1n+q, 1n+q))), True{}, Equal.cong(Nat, Bool, x => N.Nat.even(x), Nat.mul(1n+p, 1n+p), Nat.double(Nat.mul(1n+q, 1n+q)), e), N.Nat.even_double(Nat.mul(1n+q, 1n+q))))# 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 dropsdef Nat.sqrt2.step(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: N.Nat.Le(p, 1n+g), rec: @q2: Nat -> @j: Nat -> @b: N.Nat.Le(q2, g) -> @e2: {Nat.mul(1n+q2, 1n+q2) == Nat.double(Nat.mul(1n+j, 1n+j)) : Nat} -> Empty) -> Empty: match k: case 0n: N.Nat.succ_neq_zero(p, hk) case 1n+j: +j2 = j rec(q, j2, N.Nat.le_trans(1n+q, p, 1n+g, Nat.sqrt2.lt(p, q, e), bound), Equal.sym(Nat, Nat.double(Nat.mul(1n+j2, 1n+j2)), Nat.mul(1n+q, 1n+q), N.Nat.double_inj(Nat.double(Nat.mul(1n+j2, 1n+j2)), Nat.mul(1n+q, 1n+q), Equal.trans(Nat, Nat.double(Nat.double(Nat.mul(1n+j2, 1n+j2))), Nat.mul(Nat.double(1n+j2), Nat.double(1n+j2)), Nat.double(Nat.mul(1n+q, 1n+q)), Equal.sym(Nat, Nat.mul(Nat.double(1n+j2), Nat.double(1n+j2)), Nat.double(Nat.double(Nat.mul(1n+j2, 1n+j2))), Nat.sq_double(1n+j2)), Equal.trans(Nat, Nat.mul(Nat.double(1n+j2), Nat.double(1n+j2)), Nat.mul(1n+p, 1n+p), Nat.double(Nat.mul(1n+q, 1n+q)), Equal.sym(Nat, Nat.mul(1n+p, 1n+p), Nat.mul(Nat.double(1n+j2), Nat.double(1n+j2)), Equal.cong(Nat, Nat, x => Nat.mul(x, x), 1n+p, Nat.double(1n+j2), hk)), e)))))def Nat.sqrt2.go(f: Nat, p: Nat, +q: Nat, bound: N.Nat.Le(p, f), +e: {Nat.mul(1n+p, 1n+p) == Nat.double(Nat.mul(1n+q, 1n+q)) : Nat}) -> Empty: match f: case 0n: match p: case 0n: N.Bool.false_ne_true(Equal.trans(Bool, False{}, N.Nat.even(Nat.double(Nat.mul(1n+q, 1n+q))), True{}, Equal.cong(Nat, Bool, x => N.Nat.even(x), 1n, Nat.double(Nat.mul(1n+q, 1n+q)), e), N.Nat.even_double(Nat.mul(1n+q, 1n+q)))) case 1n+p1: match bound: case 1n+g: +g2 = g +p2 = p +q2 = q Nat.sqrt2.step(g2, p2, q2, N.Nat.half(1n+p2), N.Nat.even_half(1n+p2, Nat.sqrt2.even(p2, q2, e)), e, bound, q3 => j => b => e2 => Nat.sqrt2.go(g2, q3, j, b, e2))# THE THEOREM: no (1+p)^2 equals 2 (1+q)^2def Nat.sqrt2_irrational(+p: Nat, +q: Nat, e: {Nat.mul(1n+p, 1n+p) == Nat.mul(2n, Nat.mul(1n+q, 1n+q)) : Nat}) -> Empty: Nat.sqrt2.go(p, p, q, N.Nat.le_refl(p), Equal.trans(Nat, Nat.mul(1n+p, 1n+p), Nat.mul(2n, Nat.mul(1n+q, 1n+q)), Nat.double(Nat.mul(1n+q, 1n+q)), e, N.Nat.two_mul(Nat.mul(1n+q, 1n+q))))