# Zulip Chat Archive

## Stream: maths

### Topic: Conway addition thing

#### Kevin Buzzard (Jan 30 2020 at 19:04):

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

#### Kevin Buzzard (Jan 30 2020 at 19:05):

#### Scott Morrison (Jan 30 2020 at 19:22):

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

.

#### Kevin Buzzard (Jan 30 2020 at 19:32):

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 (Jan 30 2020 at 19:32):

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

#### Mario Carneiro (Jan 30 2020 at 19:35):

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

#### Kevin Buzzard (Jan 30 2020 at 19:35):

ha yeah, that took us a while :-)

#### Kevin Buzzard (Jan 30 2020 at 19:36):

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

#### Kevin Buzzard (Jan 30 2020 at 19:36):

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

#### Mario Carneiro (Jan 30 2020 at 20:04):

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 (Jan 30 2020 at 20:05):

it's a cheat, of course

Last updated: May 09 2021 at 10:11 UTC