Hi there,

I've been learning Rust for a period. Yesterday someone asked me to try to do formal verification with the Rust type system. So I decided to write one to prove the associative law of addition. One is to exercise my programming skills, the other is for fun :D.

The source code is here.

# Target

To prove `a + (b + c) = (a + b) + c`

, for any natural number a, b and c.

# Steps

## Addition

We need to define what "natural number" exactly are, which are `Zero`

and its successors.

```
struct Succ<N>(N);
struct Zero;
```

And then, we define a trait indicates if a type is a natural number.

```
trait Nature {
type Add<T: Nature>: Nature;
}
```

Implement it for `Zero`

to say `0 + n = n`

.

```
impl Nature for Zero {
type Add<T: Nature> = T;
}
```

For `Succ<T>`

to nest successors.

```
impl<T> Nature for Succ<T>
where
T: Nature,
{
type Add<U: Nature> = Succ<T::Add<U>>;
}
```

Now we can add two numbers.

```
type One = Succ<Zero>;
type Two = Succ<Succ<Zero>>;
type Three = Succ<Succ<Succ<Zero>>>;
type Four = Succ<Succ<Succ<Succ<Zero>>>>;
// 2 + 1 + 1 = 4
fn add_test(x: <<Two as Nature>::Add<One> as Nature>::Add<One>) -> Four {
x
}
```

## Associative Law

It's hard to let Rust understand that two types are equal. Using functions is unintuitive and sounds like cheating because not only uses type system. So I can only put this law into trait bounds. But because of the generic types (B and C), so I cannot put this into `Nature`

trait.

Firstly we define two types, `(a + b) + c`

and `a + (b + c)`

, for any natural number a, b, c.

```
// (a + b) + c
type APlusBPlusC1<A, B, C> = <<A as Nature>::Add<B> as Nature>::Add<C>;
// a + (b + c)
type APlusBPlusC2<A, B, C> = <A as Nature>::Add<<B as Nature>::Add<C>>;
```

Now our target is to implements `Assoc`

trait for `Zero`

and any of its successors.

```
trait Assoc<B, C>
where
Self: Nature,
B: Nature,
C: Nature,
// this is the key trait bound,
// satisfying this equivalent to satisfying associative law for
// specified natural numbers `Self`, `B` and `C`
<Self as Nature>::Add<B>: Nature<Add<C> = APlusBPlusC2<Self, B, C>>,
{
fn assoc(x: APlusBPlusC1<Self, B, C>) -> APlusBPlusC2<Self, B, C> {
x
}
}
```

It's more than easy to implement it for `Zero`

.

```
impl<B, C> Assoc<B, C> for Zero
where
B: Nature,
C: Nature,
{
}
```

But if we want to implement it for `Succ<T>`

, `T`

is required to implement both `Nature`

and `Assoc<B, C>`

.

```
impl<T, B, C> Assoc<B, C> for Succ<T>
where
T: Nature,
B: Nature,
C: Nature,
// so we need this
<T as Nature>::Add<B>: Nature<Add<C> = APlusBPlusC2<T, B, C>>,
T: Assoc<B, C>,
{
}
```

So we are done.

Let's take a test.

```
fn main() {
let _ = <Two as Assoc<One, Three>>::assoc;
}
```

This function compiles, indicates `Two`

, `One`

and `Three`

satisfy associative law of addition.

## Conclusion

This proof is just a attempt, there is still room for improvement:

- How to require
`Nature`

implements`Assoc<B, C>`

for generic type`B`

,`C`

? Associate functions are not allowed. - Is there any other way to prove?

Thanks for reading.

(Double thanks if you have any suggestions for me. )