Why can't recursion be used directly within the theorem?

Stream: general

[Asei Inoue]

The following is part of a proof showing that every number in MyNat (a custom-defined natural number type) has a prime factor.

Here, I use induction n using strongRecOn with, but the same proof can be written without induction when using the built-in Nat type.

However, if I try to imitate that in MyNat, I get a “failed to show termination” error.

What is my MyNat missing?

namespace MyNat

/-- Prime number: a number greater than 1 that is not divisible by anything other than itself and 1. -/
@[simp]
def IsPrime (n : MyNat) : Prop :=
  n > 1 ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n

theorem not_lt_zero (n : MyNat) : ¬n < 0 := by grind

theorem le_of_succ_le_succ {n m : MyNat} : n.succ ≤ m.succ → n ≤ m := by
  induction n with grind

def lt_wfRel : WellFoundedRelation MyNat where
  rel := (· < ·)
  wf := by
    apply WellFounded.intro
    intro n
    induction n with
    | zero =>
      apply Acc.intro 0
      intro y h
      apply absurd h (MyNat.not_lt_zero _)
    | succ n ih =>
      apply Acc.intro (MyNat.succ n)
      intro m h
      have : m = n ∨ m < n := MyNat.eq_or_lt_of_le (MyNat.le_of_succ_le_succ (by grind))
      match this with
      | Or.inl e => subst e; assumption
      | Or.inr e => exact Acc.inv ih e

noncomputable def strongRecOn.{u}
    {motive : MyNat → Sort u}
    (n : MyNat)
    (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n :=
  MyNat.lt_wfRel.wf.fix ind n

/-- Every number greater than 1 has a prime factor. -/
theorem exists_prime_factor (n : MyNat) (hgt : 1 < n) :
  ∃ k, IsPrime k ∧ k ∣ n := by
  induction n using strongRecOn with
  | ind n ih =>
    -- Case split depending on whether `n` is prime or not.
    by_cases hprime : IsPrime n
    case pos =>
      -- If `n` is prime, the claim is clear.
      grind

    -- Now assume that `n` is not prime.
    -- Since `n` is not prime, it must have a proper divisor less than `n`.
    have ⟨k, _, _, _⟩ : ∃ k, 1 < k ∧ k < n ∧ k ∣ n := by
      simp_all

    -- By induction, we may assume `k` has a prime factor.
    have := ih k ‹k < n› ‹1 < k›

    -- Since `k ∣ n`, if `k` has a prime factor, so does `n`.
    grind

end MyNat

[Kenny Lau]

Please include the definition of MyNat to make this an #mwe, i.e. so that other people can run your code without any issues.

My guess is that you need to make lt_wfRel an instance (not itself, but a related IsWellFounded instance)

[Asei Inoue]

@Kenny Lau

sorry my code is here: https://github.com/lean-ja/lean-by-example/tree/main/Playground/MyNat

[Kenny Lau]

that's not a file that anyone here can just run

[Asei Inoue]

here is mwe (too long to copy-paste)

Single.lean

[Asei Inoue]

My guess is that you need to make lt_wfRel an instance

Thank you but adding @[instance] does not work