Search code examples
dependent-typeformal-verificationlean

Defining the predecessor function (with pred 0 = 0) for the natural numbers in Lean

I'm learning the Lean proof assistant. An exercise in https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html is to define the predecessor function for the natural numbers. Can someone help me with that?

Solution

  • You are probably familiar with pattern-matching from Lean or some functional programming language, so here is a solution that uses this mechanism:

    open nat

definition pred : ℕ → ℕ
| zero     := zero
| (succ n) := n

    Another way of doing this is using a recursor like so:

    def pred (n : ℕ) : ℕ :=
  nat.rec_on n 0 (λ p _, p)

    Here, 0 is what we return if the argument is zero and (λ p _, p) is an anonymous function that takes two arguments: the predecessor (p) of n and the result of recursive call pred p. The anonymous function ignores the second argument and returns the predecessor.