FPIL Even Number Literals

Stream: new members

[Josha Dekker]

While working through FPIL, I tried to do the first exercise in section 4.2, which tells me to write an OfNat instance for Even (which we had to write in section 4.1). My attempt at this was the following:

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

instance : OfNat Even (2*n) where
  ofNat :=
    let rec natEven : Nat → Even
      | Nat.zero => Even.zero
      | n+1 => Even.succ (natEven n)
    natEven n

-- Check OfNat Even works
#eval (0 : Even)

but the latter fails with

failed to synthesize instance
  OfNat Even 0

What obvious thing am I missing?

[Josha Dekker]

The section hints that I need something from that section so I'm probably doing something wrong, as I don't think I'm using anything from that section, but I could be wrong

[Nathan Taylor]

Hi Josha,

My implementation of Even looks pretty similar to yours: two hints I might suggest:

1) The point of needing recursive instance search is to say "supposing that OfNat is defined on Even n, here's how to define it on Even (n + 2) - in order to state that assumption, you have to make use of an instance implicit in your instance. (The syntax confounded me for a long while, but, by cribbing off the "Supposing that \alpha has an Add instantiation, here's how to Add a Pos \alpha" example in 4.2, I was able to random-walk my way to the correct solution.)

2) Since the instance you define in 1) depends on a recursive instance search, you need to specify a base case for the search to terminate. As a result, I, at least, have two separate instance declarations for OfNat Even. (As I'm only a bit ahead of you in fpinlean I have not yet learned enough Lean to know if you can do both in a single instance as you were trying to do.)

Hope that points you in the right direction,
Nathan

[Josha Dekker]

Hi, could you explain why you would use Even (n+2) here?

[Nathan Taylor]

My particular definition of Even was an inductive datatype similar to Nat, except instead of one discriminant representing one more than another Nat, it represents two more than another Even. So, Lean needs to resolve an instance of "an Even two less than Even (n+2). (Are you sure that odd numbers are unrepresentable in your construction?)