OfNat Even (n * 2)

Stream: lean4

[Michiel Peeters]

I'm following the FP in Lean 4 book and one of the exercises is to create an even numbers type and define some type class instances for it. One of them is OfNat to overload the (even) numeric literals. The first example the book gave was for strict positive integers called Pos and the type class instance was defined as OfNat Pos (n + 1). In this case, lean is smart enough to deconstruct (n + 1), disallowing 0 and this only provide an OfNat instance for strict positive integers.

I thought to do something similar for Even: OfNat Even (n * 2), I thought that lean was maybe able to do something similar, disallowing odd numbers like this because they can't be written as 2 * n for some n. However this does not work and I can't seem to find why exactly. My gut says it has something to do with Nat being defined as successors, so + is easier to deconstruct somehow, but I can't find any substantial evidence for that claim.

I would love if someone could tell or show me what kind of expressions are allowed in OfNat declarations and how they are deconstructed. Thanks!

[Floris van Doorn]

I believe that the Lean elaborator has special support to solve n =?= ?k +1, but not for n =?= ?k * 2.
I don't know if it's possible to add this yourself without changing Lean (unification hints do something similar, but I don't know if they can do this).

The following works a little bit, but it's not ideal (you have to write OfNat.ofNat, the resulting term actually has nested ofNat's, and it doesn't work for 6, only for _ * 2).

import Mathlib.Algebra.Ring.Parity

instance (n : ℕ) : OfNat { k : ℕ // Even k } (n * 2) :=
  ⟨n * 2, even_two.mul_left n⟩

#check (OfNat.ofNat (3 * 2) : { k : ℕ // Even k })

This is also possible, but probably a very bad idea :-)

instance (n : ℕ) : OfNat { k : ℕ // Even k } n :=
  ⟨n * 2, even_two.mul_left n⟩

#eval (7 : { k : ℕ // Even k }) -- 14

[Daniel Weber]

You can also do

instance (n : ℕ) : OfNat { k : ℕ // Even k } n :=
  if hn : Even n then ⟨n, hn⟩ else ⟨0, even_zero⟩

or even

instance : Inhabited { k : ℕ // Even k } := ⟨⟨0, even_zero⟩⟩

instance (n : ℕ) : OfNat { k : ℕ // Even k } n :=
   ⟨if hn : Even n then ⟨n, hn⟩ else panic "Error: number not even"⟩