{{ message }}

Instantly share code, notes, and snippets.

# gretingz/rust1plus1.md

Last active Jan 17, 2021
Proving that 1 + 1 = 2 in Rust

# Proving that 1 + 1 = 2 in Rust

The fact that 1 + 1 is equal to 2 is one of those things that is so obvious it may be hard to justify why. Fortunately mathematicians have devised a way of formalizing arithmetic and subsequently proving that 1 + 1 = 2. Natural numbers are based on the Peano axioms. They are a set of simple rules that define (along with a formal system) what natural numbers are. So in order to prove 1 + 1 = 2 in Rust we first need a formal system capable of handling logic. The formal system that we'll be using is not some random crate, but Rust's type system itself! We will not have any runtime code, instead the type checker will do all the work for us.

## Implementing the Peano axioms

First let's go trough the Peano axioms. The first axiom is that "Zero is a natural number". Basically what it says is that zero exists. In order to express that in the type system, we just write:

`struct Zero();`

The sixth and seventh axioms state that every natural number has a unique successor. Mathematically this successor function is written as `S(n)`, and (by definition of addition) `S(n) = n + 1`. These axioms can be written with a generic type that looks like this:

`struct Successor<P>(P);`

So to write natural numbers we just do

```type One = Successor<Zero>;
type Two = Successor<One>;
type Three = Successor<Two>;
type Four = Successor<Three>;
type Five = Successor<Four>;```

This definition also satisfies the eighth axiom which states that there doesn't exist a natural number smaller than zero. The second, third, fourth and fifth axiom all define how equality works. We don't have to translate them to Rust, because Rust already has a system of equality between types.

The ninth axiom is a bit more tricky. It states that you can use induction to prove things about natural numbers. However it is not necessary to express it in Rust for simple proofs like these.

## Implementing addition and proving 1 + 1 = 2

Now that the Peano axioms are done, we can define addition. First we'll write

```struct AddHelper<A, B>(A, B);

type Result;
}```

The `Result` associated type is simply the value of the addition. Next we'll implement the `Add` trait for `AddHelper`:

```impl<A> Add for AddHelper<A, Zero> {
type Result = A;
}```

This first `impl` simply states that `a + 0 = a`. For non-zero addition we write:

```impl<A, B> Add for AddHelper<A, Successor<B>> where AddHelper<A, B> : Add {
}```

It may be a bit harder to read but this trait is implemented for `AddHelper<A, Successor<B>>`. So it calculates the result of `a + (b + 1)`. If we then look at `Result`, it's type is `Successor<<AddHelper<A, B> as Add>::Result>`. In other words it's `(a + b) + 1`. So what this `impl` is really saying is that `a + (b + 1) = (a + b) + 1`. Or if you want to use `S(x)` to denote the successor, `a + S(b) = S(a + b)`.

The reason why this recursive definition works is that it essentially decrements the right hand side, until it's reduced to the trivial `a + 0` case. For example `3 + 2 = 3 + S(S(0)) = S(3 + S(0)) = S(S(3 + 0)) = S(S(3)) = 5`.

Now we can prove that `1 + 1 = 2`. To prove that two types are equal we can use a const declaration like so:

`const QED : Option<<AddHelper<One, One> as Add>::Result> = Option::<Two>::None;`

Here we use an Option to wrap the types, because with Option you don't have to create an instance of the wrapped type, but the type checker still checks if the types are equal.

The left type is `<AddHelper<One, One> as Add>::Result`, which is in other words `1 + 1`. On the right side we have `Two`. In other words `1 + 1 = 2`.

If we change `Two` to `Three` we get an error as expected. We also get an error if we try `2 + 2 = 5`. Take that Ingsoc!

## Implementing multiplication and proving 3² + 4² = 5²

Multiplication can be defined similarly to addition. We write:

```struct MulHelper<A, B>(A, B);
trait Mul {
type Result;
}```

Next we define multiplication with zero:

```impl<A> Mul for MulHelper<A, Zero> {
type Result = Zero;
}```

And then with a successor:

```impl<A, B> Mul for MulHelper<A, Successor<B>> where AddHelper<A, <MulHelper<A, B> as Mul>::Result> : Add {
}```

Here multiplication is implemented for `MulHelper<A, Successor<B>>`, which just means `a * S(b)`. The type of the result may be a bit harder to read, but it is equivalent to `a + a * b`. So in other words `a * (b + 1) = a + a * b`

The problem is that this doesn't actually work, instead it causes some sort of infinite recursion when calculating trait bounds. I could spend a few hours trying to understand how Rust calculates trait bounds and fix the problem, but instead I'm just gonna take the lazy route and rewrite multiplication in a form that is slightly easier for Rust to understand.

To do that let's first write the following struct:

`struct MulImplHelper<Acc, A, B>(Acc, A, B);`

Mathematically this represents `acc + a * b`. We then define multiplication recursively as follows:

`0 + a * S(b) = a + a * b`

`S(acc) + a * b = S(acc + a * b)`

`0 + a * 0 = 0`

And then to define multiplication we write:

`a * b = 0 + a * b`

In rust that looks like

```trait Mul {
type Result;
}

// S(Acc) + A * B = S(Acc + A * B)
impl<Acc, A, B> Mul for MulImplHelper<Successor<Acc>, A, B> where MulImplHelper<Acc, A, B> : Mul {
type Result = Successor<<MulImplHelper<Acc, A, B> as Mul>::Result>;
}

// 0 + A * S(B) = A + A * B
impl<A, B> Mul for MulImplHelper<Zero, A, Successor<B>> where MulImplHelper<A, A, B> : Mul {
type Result = <MulImplHelper<A, A, B> as Mul>::Result;
}

// 0 + A * 0 = 0
impl<A> Mul for MulImplHelper<Zero, A, Zero> {
type Result = Zero;
}

struct MulHelper<A, B>(A, B);

// A * B = 0 + A * B
impl<A, B> Mul for MulHelper<A, B> where MulImplHelper<Zero, A, B> : Mul {
type Result = <MulImplHelper<Zero, A, B> as Mul>::Result;
}```

I'm not sure why this works better than the previous definition, but my guess is that it has to do something with the fact that the type of recursion here is much simpler.

Now that multiplication is defined we can prove that 3² + 4² = 5²:

```// Define separatly for clarity
type ThreeSquared = <MulHelper<Three, Three> as Mul>::Result;
type FourSquared = <MulHelper<Four, Four> as Mul>::Result;
type FiveSquared = <MulHelper<Five, Five> as Mul>::Result;

## What are the limits for proving things in Rust?

Rust's type system is turing complete, so in theory you could implement any formal system in it and then use that. Using the vanilla type system, it's possible to constructively prove existential statements. It should also be possible to prove that something can't exist, using proof by contradiction. The reason why proofs by contradiction should be possible is that when implementing a trait with generics you are essentially saying that assuming X (the generic parameters satisfy some traits), then Y (the type satisfies the trait you are implementing). If Y is a logical contradiction, then X must be also, therefore X can't exist.

### alexxroche commented Oct 12, 2020

 s/what is/what it/

### sollyucko commented Oct 14, 2020

 FWIW, you can use generic type aliases to make the syntax more ergonomic: ```type Add = as AddTrait>::Result; type Mul = as MulTrait>::Result; type Squared = Mul; const QED : Option, Squared>> = Option::>::None;```

 Cool!

### j0hnmeow commented Oct 26, 2020

 Some countries use quite different first Peano axiom: it uses 1 instead of 0.