Decidable

I have been exploring the Lean programming language.

The language has a functional, ML style, like Haskell. But beyond that, Lean has an advanced, research grade, type system. Dependent Types allow Lean’s type system to be used independently as a theorem prover.

Advanced mathematics, and formal system verification, can be performed almost exclusively within the type system. This is not an incidental feature either. Frameworks for deep frontier mathematics and physics are being developed, and real formal verification of algorithms and protocols is possible (similar to TLA+).

Exploring the FP space and theorem proving can be eye opening. But there is an open question:

How do we get from this “pie in the sky” type programming back down to real, concrete, executable code?

During some exploration, I ran headlong into this problem. It became evident the clear separation of proofs and propositions, versus executable code. Working through an exploration of some basic Graph Theory turned up the distinction when trying to define graph properties. Proofs and propositions exist in Lean as a separate type universe.

Let’s explore the “bridge” between the paradigms.

Rock Paper Scissors

As a working example of Lean, theorems, and the bridge back to “real code”, we can work through the classic game.

There are three “throws” in the game. We need a type to describe these unique values.

In other languages, we might choose what are usually called Enum values, if a language supports algebraic data types (ADTs).

Lean does support ADTs, and in fact the type system is much more powerful than even GADTs.

Lean calls these kinds of types inductive:

inductive RockPaperScissors
  | rock
  | paper
  | scissors

The game is that two players “throw” a selection, and rules decide who wins.

Here is a function definition for whether a first throw “beats” a second:

def beats (fst snd: RockPaperScissors): Prop :=
  match fst, snd with
    | .rock, .scissors => True
    | .scissors, .paper => True
    | .paper, .rock => True
    | _, _ => False

Working through this, we see a definition (def) of a function. It takes two arguments (fst and snd) of type RockPaperScissors, our inductive type. And this returns a Prop, short for a Proposition, which in this function is either True or False.

An aside!

True and False for Propositions are the types of truth or contradiction. Do not confuse these with true and false, which are primitive Boolean values.

Consider a simple theorem about our definition of beats:

theorem paper_beats_rock_trivially : beats .paper .rock :=
  True.intro

Paper beats Rock.

That is true, intuitively, and now by proof.

There are other ways to express this proof, using tactics, or other syntactic sugar, but these mean exactly the same thing. Our beats .paper .rock is True.

For demonstration, here are other examples of ways to write the same theorem (one per line):

-- any one line completes the proof for this theorem

theorem paper_beats_rock_trivially : beats .paper .rock :=
  ⟨⟩
  by exact True.intro
  by trivial
  by apply True.intro
  by constructor
  by simp [beats]

Great!

We have proved that Paper beats Rock.

What if we want to execute our beats function in a program?

Our Proposition definition of beats exists entirely within the type system. If we compile our module, our theorem will be checked inline, and will raise an error if the proof is invalid.

But what if we try to evaluate our function?

#eval beats .rock .paper -- Error!

The compiler reports:

■ failed to synthesize    Decidable (beats RockPaperScissors.rock RockPaperScissors.paper)

It cannot create a runtime instance of the result of the beats function. We only have a logical proposition, but no real values.

And that brings us to the bridge between the abstract type system and executable code.

Decidable is a typeclass that bridges Propositions and Boolean types. Here is the definition from the Prelude:

class inductive Decidable (p : Prop) where
  /-- Proves that `p` is decidable by supplying a proof of `¬p` -/
  | isFalse (h : Not p) : Decidable p
  /-- Proves that `p` is decidable by supplying a proof of `p` -/
  | isTrue (h : p) : Decidable p

To implement Decidable, we can create an instance of it for beats:

instance (fst snd : RockPaperScissors) : Decidable (beats fst snd) :=
  match fst, snd with
    | .rock, .scissors => isTrue True.intro
    | .scissors, .paper => isTrue True.intro
    | .paper, .rock => isTrue True.intro

    | .rock, .rock | .rock, .paper
    | .paper, .paper | .paper, .scissors
    | .scissors, .scissors | .scissors, .rock
      => isFalse (fun h => h)

This is a bit verbose, and a bit arcane, so we should review.

This is an instance of the Decidable typeclass over a call to beats fst snd. What we are providing is a map for each case to isTrue or isFalse. This lets Lean now produce a Bool value for each beats result, from the Proposition result.

We unfortunately need to exhaustively match each case of fst and snd. Note the multicase match for all the non-beating results: they all map to isFalse.

We could use a more clever solution, using the first combinator to handle pairs case-by-case. But this is less instructive:

instance : DecidableRel beats := fun fst snd => by
  cases fst <;> cases snd <;>
    first
    | exact isTrue True.intro
    | exact isFalse (fun h => h)

It Works

With our new Decidable definition of beats in hand, we can now both prove theorems:

theorem paper_beats_rock : beats .paper .rock := by
  decide

as well as use it in executable programs:

#eval decide (beats .rock .paper) -- false

or even just:

#eval beats .rock .paper -- false

Decidable gives us the needed bridge between the universe of proofs and theorems, and the universe of data and programs. Lean internally distinguishes and marks functions and definitions that are noncomputable. Using Decidable provides the resolution.

We’ve stumbled onto the differences between classical and constructivist mathematics. This turns out to be a profound distinction!

Why Lean?

I have taken a recent interest in Lean for a few reasons.

For one, I want to more deeply understand the functional programming paradigm, and Lean is a step beyond even Haskell.

Additionally, I see Lean as a new frontier in mathematical computing. It includes an advanced, academic-quality, dependent type system that puts the language into a class of its own.

Projects currently underway are the previously mentioned Mathlib, as well as PhysLib. Veil is a project for formally verifying distributed protocols, similar to TLA+. Aeneas is building formal verification for Rust. And Lean has even been “used in anger” for policy verification at AWS.

Some folks are even trying to “compile” Fermat’s Last Theorem!

Going Forward

Lean is very capable as a full functional programming language. That does tend to come secondary to its theorem-proving capability. But personally I find the syntax to be more friendly to my eyes than Haskell.

The formal methods are the killer feature. Provably correct, bug-free software? That is the dream!

In the new era of LLM and AI enhanced development, the correctness and well defined properties of our systems are ever more important. We might all be more comfortable with AI-generated software if we can know it is provably correct and verified.

Programming, though, is just an aside from becoming a codified “lingua franca” for modern mathematics. The frontier is open for pull requests.

Lean might not be the final system for expressing math and philosophy. But it sure seems like a precursor and an inspiration.

Give Lean a try!

Here is a playground link for our examples from the post, but for the “full experience” try out the LSP inside an IDE.