Conway addition thing

Stream: maths

[Kevin Buzzard]

Someone at Xena just asked me how to define addition on the following data structure:

[Kevin Buzzard]

IMG_20200130_190334916.jpg

[Scott Morrison]

In some sense, this is already in mathlib, as (particular terms in)pgame.

[Kevin Buzzard]

Yes, but to actually define addition on the data structure one needs some kind of reduction algorithm to turn the non-standard form of the number back into a number :-/

[Kevin Buzzard]

In some sense, this is already in mathlib, because mathlib has localisations and so it has $\mathbb{Z}[1/2]$ :P

[Mario Carneiro]

first things first, can you define the map from trees to real?

[Kevin Buzzard]

ha yeah, that took us a while :-)

[Kevin Buzzard]

You have to rewrite the tree as the integers with a tree hanging off each integer

[Kevin Buzzard]

and the moment you step off the integers then you're just adding or subtracting 2^{-n}

[Mario Carneiro]

import data.real.basic

inductive treenum
| leaf
| left (_: treenum)
| right (_: treenum)

inductive treepos
| start : treepos
| left : treepos
| right : treepos
| inner (n : ℕ) : treepos

noncomputable def to_real_aux : treenum → treepos → ℝ → ℝ
| treenum.leaf      _                 r := r
| (treenum.left i)  treepos.start     r := to_real_aux i treepos.left (r - 1)
| (treenum.left i)  treepos.left      r := to_real_aux i treepos.left (r - 1)
| (treenum.left i)  treepos.right     r := to_real_aux i (treepos.inner 2) (r - 1 / 2)
| (treenum.left i)  (treepos.inner n) r := to_real_aux i (treepos.inner (n+1)) (r - 1 / 2 ^ n)
| (treenum.right i) treepos.start     r := to_real_aux i treepos.right (r + 1)
| (treenum.right i) treepos.left      r := to_real_aux i (treepos.inner 2) (r + 1 / 2)
| (treenum.right i) treepos.right     r := to_real_aux i treepos.right (r + 1)
| (treenum.right i) (treepos.inner n) r := to_real_aux i (treepos.inner (n+1)) (r + 1 / 2 ^ n)

noncomputable def treenum.to_real (t : treenum) : ℝ := to_real_aux t treepos.start 0

instance : inhabited treenum := ⟨treenum.leaf⟩

noncomputable def treenum.add (t₁ t₂ : treenum) : treenum :=
classical.epsilon $ λ t', t'.to_real = t₁.to_real + t₂.to_real

[Mario Carneiro]

it's a cheat, of course