reals.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/reals.bend as Reals

0.999... = 1 -- a machine-checked proof, in one file.

Bend is a Python-shaped language where a TYPE is a claim and a PROGRAM of that type is its proof. There are no tactics: every proof below is an ordinary recursive function, and bend reals.bend --check verifies them.

The plan, in four steps:

1. Integers. Pos{n} is n, NegS{n} is -(1+n). One term per integer. 2. Rationals. Q{num, den} means num / (1 + den), so the denominator is never zero. Different terms may denote the same number. 3. Reals. A real is a RECIPE -- a little piece of data saying how the number was built -- and Real.at(x, n) is the interpreter that reads the recipe and hands back the n-th rational approximation, good to within 2^-n. 4. Equality. Two reals are equal when, for EVERY precision n, their n-th approximations sit within 2^-n + 2^-n of each other. Nothing ever has to compare infinitely many digits.

Then 0.999... is the recipe RNines{}, whose n-th approximation is 1 - 10^-n, and the theorem nines_is_one says it is equal to 1. The whole numerical content is one inequality: the gap 10^-n never exceeds the allowance 2^-n + 2^-n, because 2^n <= 10^n.

2 imports

import Base
import ./nat.bend as N

Types

type Int source · line 75 · raw

Data

Pos
```
@n:Nat -> Int
```
NegS
```
@n:Nat -> Int
```

type Q source · line 162 · raw

Data

Q
```
@num:Int -> @den:Nat -> Q
```

type Real source · line 268 · raw

Data

RQ
```
@q:Q -> Real
```
RNines
```
Real
```

Definitions

def le_copy source · line 36 · 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

N.Nat.Le(a, b) is a COMPUTED proposition: it reduces to Unit when a <= b and to Empty when it does not. So a proof of it is data -- but in Bend every variable is spent when used, and this one is needed twice below. le_copy re-derives a fresh pair by walking the two numbers down together.

def le_mul_l source · line 48 · 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))

x <= y => c*x <= c*y

def le_mul_r source · line 57 · raw

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

x <= y => x*c <= y*c

def Int.neg_nat source · line 80 · raw

@n:Nat -> Int

-n, for a natural n

def Int.sub_nat source · line 88 · raw

@a:Nat -> @b:Nat -> Int

a - b for two naturals, as an integer: count both down until one runs out

def Int.neg source · line 99 · raw

@a:Int -> Int

def Int.add source · line 106 · raw

@a:Int -> @b:Int -> Int

def Int.mul source · line 117 · raw

@a:Int -> @b:Int -> Int

def Int.abs source · line 128 · raw

@a:Int -> Nat

def Int.Le source · line 136 · raw

@a:Int -> @b:Int -> Type

a <= b, again as a computed proposition

def Int.sub_nat_zero source · line 147 · raw

@x:Nat -> {Int.sub_nat(x, 0n) == Pos{x} : Int}

def Q.of_nat source · line 165 · raw

@n:Nat -> Q

def Q.num source · line 168 · raw

@q:Q -> Int

def Q.den_int source · line 173 · raw

@q:Q -> Int

def Q.Eq source · line 182 · raw

@+x:Q -> @+y:Q -> Type

2/4 and 1/2 are different TERMS but the same number, so equality of rationals is this relation -- cross multiplication -- not ==. (The proof below never needs it; it is here because "what equality means" is the whole subject of this file.)

def Q.dmul source · line 188 · raw

@b:Nat -> @+d:Nat -> Nat

the denominator of a product, in "minus one" form. The point of writing it this way: 1 + Q.dmul(b, d) and Nat.mul(1n+b, 1n+d) unfold to the SAME term, so no lemma is ever needed to move between the two.

def Q.add source · line 192 · raw

@a:Q -> @b:Q -> Q

a/(1+e1) + b/(1+e2) = (a(1+e2) + b(1+e1)) / ((1+e1)(1+e2))

def Q.neg source · line 199 · raw

@a:Q -> Q

def Q.sub source · line 204 · raw

@a:Q -> @b:Q -> Q

def Q.abs source · line 207 · raw

@a:Q -> Q

def Q.Le source · line 213 · raw

@a:Q -> @b:Q -> Type

a/(1+d1) <= b/(1+d2) is decided by cross multiplication

def two_pow_m1 source · line 228 · raw

@n:Nat -> Nat

two_pow_m1(n) = 2^n - 1, so 1n+two_pow_m1(n) is 2^n

def ten_pow_m1 source · line 236 · raw

@n:Nat -> Nat

ten_pow_m1(n) = 10^n - 1, so 1n+ten_pow_m1(n) is 10^n

def eps source · line 244 · raw

@n:Nat -> Q

eps(n) = 2^-n : the error allowed at precision n

def ten_pow_inv source · line 248 · raw

@n:Nat -> Q

ten_pow_inv(n) = 10^-n

def Real.of_nat source · line 272 · raw

@n:Nat -> Real

def Real.at source · line 279 · raw

@x:Real -> @n:Nat -> Q

THE INTERPRETER. Real.at(x, n) reads the recipe x and returns its n-th rational approximation. A rational is its own approximation at every precision; 0.999... rounded to n decimal places is 0.99...9, which is exactly 1 - 10^-n.

def Real.Eq source · line 290 · raw

@x:Real -> @y:Real -> Type

WHAT EQUALITY MEANS. Two reals are equal when, at every precision n, their approximations differ by at most 2^-n + 2^-n -- each is allowed its own 2^-n of slack. This is a claim about all n at once, so it is proved, never computed; that is why 0.999... = 1 is a theorem.

def nines_at source · line 317 · raw

@+k:Nat -> Q

(10^n - 1) / 10^n, which is what "0.99...9 with n nines" is

def mkq source · line 320 · raw

@+z:Nat -> Q

def nines_spec_eq source · line 324 · raw

@+k:Nat -> {Q.sub(Q.of_nat(1n), ten_pow_inv(k)) == nines_at(k) : Q}

STEP 1: the interpreter's answer really is (10^n - 1)/10^n

def ten_succ source · line 329 · raw

@+p:Nat -> {1n+ten_pow_m1(1n+p) == Nat.mul(10n, 1n+ten_pow_m1(p)) : Nat}

10^(p+1) = 10 * 10^p

def pow_le source · line 333 · raw

@+k:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+two_pow_m1(k), 1n+ten_pow_m1(k))

STEP 3: 2^k <= 10^k. Induction: 2^(p+1) = 2 * 2^p <= 2 * 10^p <= 10 * 10^p.

def pos_add_neg source · line 345 · raw

@x:Nat -> @y:Nat -> {Int.add(Pos{x}, Int.neg(Pos{y})) == Int.sub_nat(x, y) : Int}

x + (-y) = x - y, for naturals cast into Int

def sub_succ source · line 357 · raw

@A:Nat -> {Int.sub_nat(A, 1n+A) == NegS{0n} : Int}

A - (A+1) = -1

def sub_one source · line 364 · raw

@+A:Nat -> {Int.sub_nat(Nat.mul(A, 1n), Nat.mul(1n, 1n+A)) == NegS{0n} : Int}

def neg_one_mul source · line 370 · raw

@+A:Nat -> {Int.mul(Int.neg(Pos{1n}), Pos{1n+A}) == Int.neg(Int.mul(Pos{1n}, Pos{1n+A})) : Int}

(-1) * b = -(1 * b): both sides compute to the same term

def nines_one_num source · line 375 · raw

@+A:Nat -> {Int.add(Int.mul(Pos{A}, Pos{1n}), Int.mul(Int.neg(Pos{1n}), Pos{1n+A})) == NegS{0n} : Int}

STEP 2: the numerator of (1 - 10^-n) - 1 is exactly -1. With A = 10^n - 1 this is A*1 + (-1)*(1+A) = -1.

def nines_one_est source · line 385 · raw

@+A:Nat -> @+Sn:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+Sn, 1n+A) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.mul(1n, Nat.mul(1n+Sn, 1n+Sn)), Nat.mul(Nat.add(Nat.mul(1n, 1n+Sn), Nat.mul(1n, 1n+Sn)), Nat.mul(1n+A, 1n)))

STEP 4: the estimate, cross-multiplied. With A = 10^n and Sn+1 = 2^n: 2^n * 2^n <= (2^n + 2^n) * 10^n because 2^n <= 10^n (h) and x <= x + x. The % lines only strip the multiplications by one that Q.Le left behind.

def nines_one_at source · line 396 · raw

@+n:Nat -> Q.Le(Q.abs(Q.sub(nines_at(n), Q.of_nat(1n))), Q.add(eps(n), eps(n)))

|0.99...9 - 1| <= 2^-n + 2^-n : steps 2, 3 and 4 put together

def nines_is_one_at source · line 401 · raw

@+n:Nat -> Q.Le(Q.abs(Q.sub(Q.sub(Q.of_nat(1n), ten_pow_inv(n)), Q.of_nat(1n))), Q.add(eps(n), eps(n)))

the same statement, phrased in the interpreter's own words

def nines_is_one source · line 412 · raw

Real.Eq(RNines{}, Real.of_nat(1n))