Is recursive checking not always true?

Stream: lean4

[luong doan]

I have a simple Inductive like the following, but it says error is in the function smaller (I have checked with #eval! but not found any error):

inductive Nat2 where
| zero: Nat2
| next (n: Nat2) : Nat2
#eval Nat2.next Nat2.zero

def Nat2.from_nat (value: Nat) : Nat2 :=
  if value = 0
    then Nat2.zero
    else Nat2.next (Nat2.from_nat (value-1))

def Nat2.to_nat (self: Nat2) : Nat :=
  match self with
  | zero => 0
  | next n => n.to_nat + 1

def Nat2.pre (self: Nat2) : Nat2 :=
  match self with
  | zero => Nat2.zero
  | next n => n

def Nat2.is_zero (self: Nat2) : Bool :=
  match self with
  | zero => true
  | next _ => false

def Nat2.smaller (self: Nat2) (other: Nat2) : Bool :=
  if self.is_zero
    then not other.is_zero
  else self.pre.smaller other.pre

#eval! (Nat2.from_nat 1).smaller (Nat2.from_nat 5)

[Kenny Lau]

nothing is "simple" when you've deviated from the standard matching patterns

[Kenny Lau]

in this case, Lean doesn't know that self.pre is smaller than self

[Kenny Lau]

you should use addition building up instead of subtraction building down, at least that's the general philosophy with lean

[luong doan]

Oh, thank you for helping me figure it out. I will reread the docs.

[Chris Bailey]

For defining recursive functions, you're generally going to get better results matching on the constructors directly when you can:

def Nat2.smaller (self: Nat2) (other: Nat2) : Bool :=
  match self with
  | zero => not other.is_zero
  | next self' => self'.smaller other.pre

#eval! (Nat2.from_nat 1).smaller (Nat2.from_nat 5)

[Kenny Lau]

I mean, you already did it in the three functions above, so it seems like you already know how to do it

[luong doan]

Yeah, I know the basics, but I didn't know why it error

[luong doan]

Anyway, thanks again for your help, guys