2010-05-15

Observable sharing and executable proofs

Every rational number has an infinite repeating decimal expansion. In particular, every integer admits two decimal expansions: one with and one without a "tail of nines". This means that 1 = 0.9999…, a provable fact that many people still choose to disbelieve. What do I mean here by "provable"? I mean "provable by finitistic reasoning", that is, by a purely algebraic proof free of notions of continuity or convergence. The proof in this particular (and particularly popular) case goes like this:

```    x     = 0.9999…
≡ { product by base is shift of decimal point }
10x     = 9.9999…
≡ { subtraction of finitely-expanded integer }
10x - 9 = 0.9999…
≡ { identity of decimal expansion }
10x - 9 = x
≡ { algebra }
9x     = 9
≡ { cancellation of multiplication }
x     = 1
```

The last two steps are elementary consequences of the fact that integers form a ring. The first three steps require justification. By definition, a decimal expansion of a positive real number x is a (possibly semi-infinite) sequence of digits 0 ≤ di < 10 such that for all iN, di = 0, and

```x = ⟨∑ i :: 10i⋅di⟩
```

and the decimal point separates the digits corresponding to 100 and 10-1, namely d0 from d-1.

Lemma 0 Any decimal number x can be expressed as the sum of an integer and a (possibly infinite) decimal part

Proof: By definition, x has a finite number of decimal digits to the left of the decimal point, namely for 0 ≤ i < N, hence:

```  x
= { definition }
⟨∑ i :: 10i⋅di ⟩
= { associativity of addition, a finite number N of times }
⟨∑ i : 0 ≤ i < N : 10i⋅di⟩ + ⟨∑ i : 0 > i : 10i⋅di⟩
= { naming the first term }
n + ⟨∑ i : 0 > i : 10i⋅di⟩
```

This justifies representing a positive real number as a pair of an integer and a possibly infinite purely fractional decimal expansion:

```type dec = Dec of int * int list
```

A sufficient condition for two numbers to be equal is that their decimal representations are the same:

```let eq (Dec (e, ds)) (Dec (e', ds')) = e = e' && ds == ds'
```

Here, since the decimal expansions could be infinite, I use physical equality on lists. This is a stronger condition than stated above. Now, the proof for the first step:

Lemma 1 Multiplying a positive real number x by 10 shifts the decimal point in its decimal expansion one place to the right

Proof:

```  10⋅x
= { lemma 0 }
10⋅(n + ⟨∑ i : 0 > i : 10i⋅di⟩)
= { product finitely distributes over sum }
10⋅n + 10⋅⟨∑ i : 0 > i : 10i⋅di⟩
= { product formally distributes over sum }
10⋅n + ⟨∑ i : 0 > i : 10i+1⋅di⟩
= { substitute i := i-1 }
10⋅n + ⟨∑ i : 1 > i : 10i⋅di-1⟩
= { lemma 0 }
(10⋅n + d0) + ⟨∑ i : 0 > i : 10i⋅di-1⟩
```

Note that the third step is not strictly speaking finitist but formal: it requires taking the distributivity of product over a summation as axiomatic if induction is not accepted. This justifies the following:

```let mul10 = function
| Dec (e, []     ) -> Dec (10 * e    , [])
| Dec (e, d :: ds) -> Dec (10 * e + d, ds)
```

The proof for the second step:

Lemma 2 Subtracting an integer k from a positive real number x only affects its integer part

Proof:

```  x - k
= { lemma 0 }
(n + ⟨∑ i : 0 > i : 10i⋅di⟩) - k
= { commutativity and associativity of sum }
(n - k) + ⟨∑ i : 0 > i : 10i⋅di⟩
```

This justifies the following:

```let subi (Dec (e, ds)) n =
if e < n then failwith "subi" else
Dec (e - n, ds)
```

Now the proof for the third step is purely executable and relies on physical equality of infinite lists of digits represented as circular lists:

```let nines = let rec ds = 9 :: ds in Dec (0, ds)
```

Of course, for more general repeating expansions, equality on heads won't suffice, but this case is nicely handled by a one-liner:

```let lemma = assert (eq nines (subi (mul10 nines) 9))
```

The purely verbal mathematical statement of this truth is that, since the first two steps operate on a finite prefix of the infinite expansion, the inifinite suffix is unchanged by the operations and hence identical to itself. In other words, the infinite summation is a purely formal object that remains unchanged from step to step.

Will this proof finally lay the "controversy" to rest, persuading even the staunchest finitist?

Edit: Thanks to id that alerted me in my confusion between structural and physical equality.