Verifying a basic function with Lean4

Question

I have this simple structure to represent a person:

structure Person where
  age: Nat
  lifespan: Nat
deriving Repr

This function takes a Person and either (a) returns a "some" person with the age incremented, if they have not exceeded their lifespan, or (b) otherwise returns "none":

def agePerson (p : Person) : Option Person :=
  if p.age < p.lifespan then
    some { p with age := p.age + 1 }
  else
    none

I'd like to validate the function, but am having a hard time applying what I learned proving e.g., Natural Number arithmetic.

I would be grateful for someone to provide a theorem that works.

Answer 1

The most important thing to learn here is that dependent type theory allows you to state conditions which you cannot normally express in a mere programming language.

In the case at hand you should define Person so that it is impossible to create a person whose age is larger than the lifespan. One way to do this is as follows:

structure Person where
  age: Nat
  lifespan: Nat
  young : age <= lifespan
deriving Repr

We added a field young which is a proof of age <= lifespan.

Now if you want to make a person older by one year, you need the assumption that their age is strictly smaller than their lifespan.

Here's the first way to do it with tactics:

def agePerson1 (p : Person) (_ : p.age < p.lifespan) : Person := by
  constructor
  case age => exact (p.age + 1)
  case lifespan => exact p.lifespan
  case young => linarith

A second, more direct way:

def agePerson2 (p : Person) (_ : p.age < p.lifespan) : Person :=
  { age := p.age + 1,
    lifespan := p.lifespan,
    young := (by linarith)
  }

Example of usage:

def joe1 : Person := { age := 5, lifespan := 10, young := (by linarith)} 
def joe2 := agePerson joe1 (by simp)
#eval joe2

A typical programmer's instincts may be that it is "annoying" to have to verify p.age < p.lifespan before you can make a person older. But if you think about it, it's even more annoying to have to deal with some ⋯ vs. none. And by explaining the rules to Lean, Lean will be able to prevent you from making bugs. You simply will not be able to write buggy code (altough you can write buggy rules).

Embrace dependent types!