# Verifying a basic function with Lean4

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.

• The split tactic (or the practically identical split_ifs tactic) can help when your goal state contains ifs
– Eric
Commented Dec 23, 2023 at 2:02
• While your original function contains p.age + 1 <= p.lifespan, it would probably make your life easier to use the equivalent p.age < p.lifespan. (Otherwise, since this is a special property of natural numbers that these are the same, you have to find the lemma which converts from one form to the other, which looks to just be the definition of Nat.lt. Then you can rewrite with this lemma.) Commented Dec 23, 2023 at 15:51
• @JasonRute - Thanks! I've edited the question. I appreciate the simplification. Commented Dec 23, 2023 at 23:30

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!