Recursive type class for OfNat Even

Question

I'm working my way through Functional Programming in Lean. There's an exercise to create an Even class to represent even natural numbers.

I was able to define addition, multiplication, and toNat, but defining using recursive instance search to define OfNat for Even has me stumped. Here's my basic scaffolding for Even:

inductive Even : Type where
  | zero
  | succ : Even → Even

def Even.toNat : Even → Nat
  | Even.zero => 0
  | Even.succ n => 2 + n.toNat

instance : ToString Even where
  toString n := toString n.toNat

For OfNat, I have the base case figured out:

instance : OfNat Even 0 where
  ofNat := Even.zero

def zeroEven : Even := 0

The book says I need Nat.zero, but 0 worked just fine.

My code for the recursive case does not compile; it's my best guess so far, but the book has not taught inferInstance yet, so there's probably a simpler solution that doesn't use it:

instance : OfNat Even (n + 2) where
  ofNat := Even.succ (inferInstance : OfNat Even n).ofNat

The error message is on inferInstance and says failed to synthesize instance OfNat Even n. I believe the basic idea is right, though; I need to synthesize an Even for n+2 by taking the successor of a synthesized Even for n, and so on with 0 as the base case.

What am I doing wrong? How do I synthesize Even via recursive instance search?

Answer 1

You are close! In order to show n+2 is even, you first have to assume n is even. You do this by adding the instance implicit argument [OfNat Even n] to the second instance:

instance : OfNat Even 0 where
  ofNat := Even.zero

instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.succ (inferInstance : OfNat Even n).ofNat

What instance search does when it encounters, say, OfNat Even 8 is that it first checks if 8 is 0, which is is not, since that would match the first instance. Otherwise, based on the second instance it checks if 8 can be syntactically manipulated into the form n + 2 for some n (in this case 6). If so, then it repeats that process for n until it reaches the base case of 0 or it gives up. That why these work:

#check (0 : Even)
#check (2 : Even)
#check (4 : Even)
#check (250 : Even)

but these fail:

#check (1000 : Even)
#check (0+0 : Even)

---

Edit: I used inferInstance just to copy your current approach, but like you said, it is not ideal. To understand what to use in place, it is important to understand how type class inference works. By adding the instance implicit argument [OfNat Even n] to the arguments of the instance, we make our instance of OfNat Even n available to any function in the body of our instance which also takes in an implicit instance argument of form [OfNat Even n].

The most general such function is inferInstance which has type:

#check inferInstance
--  inferInstance.{u} {α : Sort u} [i : α] : α

so it can take in an available instance for any type α including OfNat Even n.

But in your case all you want to do is access the field ofNat of your instance inst : OfNat Even n. There are two ways to do this.

First, you can just reference inst by name as in

instance [inst : OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.succ (inst.ofNat)

Second, the fields of a class like OfNat are themselves functions which take instance implicit arguments.

#check OfNat.ofNat
--  OfNat.ofNat.{u} {α : Type u} (x✝ : Nat) [self : OfNat α x✝] : α

(Note Lean only makes you directly supply the x : Nat and not α : Type u since the latter is inferred by the output type. So you can call OfNat.ofNat n to indirectly access the available instance of OfNat Even n as in:

instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.succ (OfNat.ofNat n)

---

Edit: If this exercise was particularly confusing to you, you might want to file an issue in the book's repo. The author seems very response to user feedback.

---

Edit: Another good resource for type class inference in Lean is the Type Classes chapter of Theorem Proving in Lean 4. (Even if you just want to use Lean for programming, this chapter is a great resource.)