Excercise solutions for "Functional Programming in Lean"

Stream: new members

[Anton Daneyko]

Hi folks, I am an FP newbie, working my way through "Functional Programming in Lean" and I feel I got stuck with a particular exercise (OfNat for an Even class). I wonder if there are any solutions out there. I found some https://github.com/leanprover/fp-lean/tree/master/examples/Examples, but not for the problem that I currently stuck with in particular.

[Derek Rhodes]

Hi Anton, I'm still a Lean4 newbie (and probably will be for awhile!) But this is my stab at it:

import Mathlib
namespace even_nums

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

open Ev

def natToEv : ℕ → Ev
| Nat.zero => zero
| Nat.succ x => succ (natToEv x) (natToEv x)

instance : OfNat Ev n where
  ofNat := natToEv n

-- Add and ToString
def evToNat : Ev → Nat
| zero => Nat.zero
| (succ x _) => 2 + evToNat x


instance : ToString Ev where
  toString ev := toString (evToNat ev)

#eval toString (succ 0 0)

instance : Add Ev where
  add x y := match y with
    | zero => x
    | (succ _ _) => succ x (succ zero zero)

#eval evToNat zero -- => "0"
#eval evToNat (succ 0 0) -- => "2"
#eval toString ((succ 0 0) + (succ 0 0)) -- => "4"
#eval toString (5 : Ev) -- => "10"


end even_nums

I made the choice to essentially double the Nat as shown in the last #eval, where 5 is mapped to 10, otherwise 5 could be represented. Maybe there is a much better way to do it - perhaps odd nats could be rounded down to nearest even, that seems like it would more closely match user expectations.

[Anton Daneyko]

Hi @Derek Rhodes , thanks for chiming in. I am glad to find someone I could ping-pong about the book. And thank you for your solution. Let me share a few thoughts about what I think is required in the exercise. Recall the task:

Write an instance of OfNat for the even number datatype from the previous section's exercises that uses recursive instance search. For the base instance, it is necessary to write OfNat Even Nat.zero instead of OfNat Even 0.

The second task also hints to the recursive applications of OfNat:

There is a limit to how many times the Lean compiler will attempt a recursive instance search. This places a limit on the size of even number literals defined in the previous exercise. Experimentally determine what the limit is.

My Even is a different from yours: it's essentially a Nat, but the addition and multiplication are defined in a different way:

inductive Even : Type :=
  | zero : Even
  | succ (n : Even) : Even

def Even.add : Even → Even → Even
  | zero, n => n
  | n, zero => n
  | succ a, n => succ (add a n)

def Even.mul : Even → Even → Even
  | zero, _ => zero
  | _, zero => zero
  | succ a, n => add n (add n (mul a n))

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

instance : Add Even where
  add := Even.add

instance : Mul Even where
  mul := Even.mul

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

-- Some checks
def two := Even.succ Even.zero
def four := Even.succ (Even.succ Even.zero)
def six := Even.succ (Even.succ (Even.succ Even.zero))
def six' := Even.add two four
def eight := Even.mul two four
#eval six -- prints 6
#eval six' -- prints 6
#eval eight -- prints 8

Now going back to the task of defining recursive OfNat, I can do something like this, unwinding a few recursive steps manually:

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

instance : OfNat Even 2 where
  ofNat := Even.succ (OfNat.ofNat 0)

instance : OfNat Even 4 where
  ofNat := Even.succ (OfNat.ofNat 2)

#eval (4 : Even) -- prints 4

The (4 : Even) calls (OfNat.ofNat 4 : Even), which in turn calls (OfNat.ofNat 2 : Even), etc. I cannot, however, figure out how to generalize it. If I try:

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

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

I get an error that I fail to interpret trying to #eval (4 : Even):

cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

BTW, I found another solution out there, which does what you suggest with rounding. My expectations as a user, however that writing something like (3 : Even) would be a compile-time error failing to synthesize an instance in the same way it is shown for the LT4 type here: https://docs.lean-lang.org/functional_programming_in_lean/type-classes/pos.html#literal-numbers.

[Derek Rhodes]

(3 : Even) would be a compile-time error

Yes, Absolutely! Thank you for taking the time to point that out. I
still have not discovered how to utilize dependent types very well.
However, I think I tracked a solution from the Author's github:

https://github.com/leanprover/fp-lean/blob/7eefe73cba60f23ab60cd1ad194c08d254e5ce42/examples/Examples/Classes/Even.lean#L4

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

It does give a nice error when trying to use odd numbers.

[Anton Daneyko]

Hey @Derek Rhodes, that's great! I was looking in the repo of the book as well, but missed that file. Thanks a lot for digging it out!