2
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ The split tactic (or the practically identical split_ifs tactic) can help when your goal state contains ifs $\endgroup$
    – Eric
    Commented Dec 23, 2023 at 2:02
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Jason Rute
    Commented Dec 23, 2023 at 15:51
  • $\begingroup$ @JasonRute - Thanks! I've edited the question. I appreciate the simplification. $\endgroup$ Commented Dec 23, 2023 at 23:30

1 Answer 1

1
$\begingroup$

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!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.