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 ≤ d_i < 10 such that for all i ≥ N, d_i = 0, and

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

and the decimal point separates the digits corresponding to 10⁰ and 10^-1, namely d₀ 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.