OfNat Pos (n+1)

Stream: lean4

[Mike Schneeberger]

In the functional programming in lean tutorial, the instance of OfNat for positive numbers is implemented as follows:

instance : OfNat Pos (n + 1) where
  ofNat :=
    let rec natPlusOne : Nat → Pos
      | 0 => Pos.one
      | k + 1 => Pos.succ (natPlusOne k)
    natPlusOne n

Based on this example, I'm trying to define an inductive type like Nat, but which only contains numbers that are greater than a certain number n.

For example, (5 : GNat 3) should work, while (2 : GNat 3) should not work.

Here is how I implemented it:

inductive GNat : Nat → Type where
  | zero : (n : Nat) → GNat n
  | succ : {n : Nat} → GNat n → GNat n

instance : OfNat (GNat n) (n + m) where
  ofNat :=
    let rec natPlusM : Nat → GNat n
    | Nat.zero => GNat.zero n
    | Nat.succ k => GNat.succ (natPlusM k)
    natPlusM m

#check (5 : GNat 3)   -- failed to synthesisze instance OfNat (GNat 3) 5

Why do I get this error message? Is there another way to make this work?

[François G. Dorais]

Try this:

instance [OfNat (GNat n) m] : OfNat (GNat n) (m + 1) where
  ofNat := GNat.succ (OfNat.ofNat m)

instance : OfNat (GNat n) (n) where
  ofNat := GNat.zero n

#check (5 : GNat 3)

[Mike Schneeberger]

Fantastic! That looks even more elegant than the solution from the tutorial. Thanks!