How to make a recursively defined function "reducible"?

Stream: lean4

[Mario Weitzer]

Below is the definition of gcd from mathlib for which the example below works using decide, but if I copy the exact definition to define my_gcd, the same example fails (obviously because of @[extern "lean_nat_gcd"]). How do I make decide work for my_gcd?

/-
@[extern "lean_nat_gcd"]
def gcd (m n : @& Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m
  decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
-/

def my_gcd (m n : @& Nat) : Nat :=
  if m = 0 then
    n
  else
    my_gcd (n % m) m
  termination_by m
  decreasing_by simp_wf; apply Nat.mod_lt _ (Nat.zero_lt_of_ne_zero _); assumption

example : Nat.gcd 10 7 = 1 := by
  decide

example : my_gcd 10 7 = 1 := by
  decide

/-
Tactic `decide` failed for proposition
  my_gcd 10 7 = 1
because its `Decidable` instance
  instDecidableEqNat (my_gcd 10 7) 1
did not reduce to `isTrue` or `isFalse`.
-/

[Junseong O]

As far as I know, what decide tactic do is applying decidability to produce a proof if it exists. Thus you have to prove decidability of your predication if you want to use this. You can find the definition of decidability in mathlib index page.

[Aaron Liu]

@[extern "lean_nat_gcd"] isn't doing anything for reducibility here

[Kyle Miller]

(@Junseong O The error here is indicating that it was able to synthesize a Decidable instance, and that the problem was that the instance failed to reduce. The Decidable instance exists.)

[Aaron Liu]

the actual reason is that Lean has special support for Nat.gcd and 13 other constants that directly computes them when applied to Nat literals (instead of having to reduce)

[Kyle Miller]

@Mario Weitzer The issue is that using termination_by causes it to not be reducible. (I have to go for a moment, but I'm sure someone will give tips.)

[Aaron Liu]

that it doesn't compute without this special support is probably a problem?

[Junseong O]

@Kyle Miller Thanks for correcting

[Aaron Liu]

I guess it's fine if we have special support for reducing Nat.gcd since that doesn't cause any problems

[Aaron Liu]

you can mark your my_gcd as @[semireducible] if you want it to reduce in the elaborator

[Aaron Liu]

or you can decide +kernel to bypass the elaborator and go straight to the kernel

[Kyle Miller]

Or you could use "gas" to make it structural recursion, which makes it readily reducible.

def my_gcd (m n : Nat) : Nat :=
  go (m + n + 1) m n
where
  go (gas : Nat) (m n : Nat) : Nat :=
    match gas with
    | 0 => 0
    | gas' + 1 =>
      if m = 0 then
        n
      else
        go gas' (n % m) m

example : my_gcd 10 7 = 1 := by
  decide

[Joachim Breitner]

Since https://github.com/leanprover/lean4/pull/7965 it's no longer needed to transform to using fuel manually, and you should be able to mark the function as semireducible … as Aaron says

[Kyle Miller]

Oh right, that's already been released! It's available in v4.27.0 (the most recent version).

[Mario Weitzer]

Thank's everybody, the @[semireducible] suggestion was the easiest solution for my problem!