Naturals Explosion

What is it?

A formally verified proof that if 0 equals 1 then all naturals are the same number. I’m a computer scientist so 0 is natural for me. 😁

Why? It’s about making a point.

It may look unuseful, but did you ever wondered the consequences of simple false statements? Have you ever thought that simply supposing that zero equals one can lead to natural numbers being blown up?

But not really. I’m just practicing Agda

Here, using the knowledge acquired with the Equality Chapter from the book Programming Language Foundations in Agda (Kokke & Wadler), I’ve proved that for practicing purposes. The proof is self-contained: every definition and property is explicitly defined.

And you can use the idea to practice whatever you wish

Learning a proof assistant? Try out the idea! I’d love to see it.