1
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ Can you supply the section number and exercise number? $\endgroup$
    – Jason Rute
    Sep 8, 2023 at 12:31
  • $\begingroup$ Without knowing more about the exercise, I can only guess what the author meant, but I’m pretty sure he didn’t mean to create a natural number-like inductive type which is isomorphic to the evens, where you need those conversion functions. Did the book really say “class” or did it say “type”. If “class”, then use class to define Even, i.e. class Even (n : Nat) with …. If “type”, then I assume he wants a Prop type Even : Nat -> Prop. $\endgroup$
    – Jason Rute
    Sep 8, 2023 at 12:34
  • $\begingroup$ Ignore my above comment. I misunderstood the exercise. $\endgroup$
    – Jason Rute
    Sep 8, 2023 at 14:28

1 Answer 1

1
$\begingroup$

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.)

$\endgroup$
3
  • $\begingroup$ The [OfNat Even n] is what I was missing! I'm still not sure if the author meant me to use inferInstance, since that wasn't introduced yet, but after doing some research I don't know how else to create an instance. $\endgroup$
    – Nate Glenn
    Sep 9, 2023 at 3:59
  • $\begingroup$ @NateGlenn I've edited my answer. $\endgroup$
    – Jason Rute
    Sep 9, 2023 at 13:28
  • $\begingroup$ Thank you for the edits! Both of the options you added were really good learning moments for me. And yes, I will probably write at the repository at some point; the treatment of recursive type class resolution was too cursory to get a good understanding of. $\endgroup$
    – Nate Glenn
    Sep 9, 2023 at 19:26

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.