## Stream: maths

#### 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):

IMG_20200130_190334916.jpg

#### 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