Exercise Functional Programing in Lean4

Stream: lean4

[yannis monbru]

Hi, i am curently reading the book https://leanprover.github.io/functional_programming_in_lean/type-classes/polymorphism.html, and doing some exercise about recursive instance search.

I am in trouble with building the instance OfNat Even. If i am right about the exercise, the goal is to provide a meaning to (n+2:Even) by knowing what is (n:Even). I could not figure out a way to have lean accept my code, and the compiler does not like to have something between instance and :. Could someone explain me what i missed?
Thank you very much.

structure Even where
  times2::
  k:Nat

def Even.Add:Even→ Even→ Even
  |times2 a,times2 b=>times2 (a+b)

instance :Add Even where
  add:=Even.Add

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

instance [OfNat Even n] : OfNat Even (n+2) where
  ofNat:= Even.Add (n:Even) (Even.times2 1)

[Bulhwi Cha]

You might want something like this:

instance [OfNat Even n] : OfNat Even (n+2) where
  ofNat:= Even.Add (Even.times2 n) (Even.times2 1)

[Bulhwi Cha]

#check (2 : Even) results in the following error:

failed to synthesize instance
  OfNat Even 2

[Kyle Miller]

You can use OfNat.ofNat directly to do the conversion:

instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.Add (OfNat.ofNat n) (Even.times2 1)

[Kyle Miller]

I think the only time OfNat.ofNat gets used implicitly is for natural number literals, which is why (n : Even) doesn't work.

[yannis monbru]

Ok, thank you , now the code is accepted but i have another issue the test #check (2:Even) still answer the same thing as below

[yannis monbru]

But then the first solution worked by removing the [OfNat Even n]. so i am not shure about what apened but the issue is solved. Thank you!

[Bulhwi Cha]

yannis monbru said:

But then the first solution worked by removing the [OfNat Even n]. so i am not shure about what apened but the issue is solved. Thank you!

When you remove the instance implicit, what are the outputs of the following #check commands?

#check (3 : Even)
#check (5 : Even)

[yannis monbru]

Oh, i see , it type check corectly...
But then how can i tell it to accpet #check (2:Even) with the solution of Kyle?

[Bulhwi Cha]

I don't know. Can somebody help us?

[David Thrane Christiansen]

Interestingly, I need to write Nat.zero in the base case to get it to work:

inductive Even : Type where
  | times2 : Nat → Even
deriving Repr

def Even.add : Even → Even → Even
  | times2 a, times2 b => times2 (a + b)

instance : Add Even where
  add := Even.add

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

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

#eval (0 : Even)

#eval (22 : Even)

This is probably worth a note.

[David Thrane Christiansen]

Thank you for reading the book!

[yannis monbru]

That's funny. Thank you for the answer (and by the way for writing the book :grinning: )