Importing breaks recursive function

Stream: general

[Niels Voss]

This question is more for my curiosity rather than practical need, but if I have this recursive function

def myfun : ℕ → ℕ
| 0 := 0
| 1 := 3
| (n + 2) := have h : (n + 2) / 2 < n + 2 := sorry,
  myfun ((n + 2) / 2)

As soon as I add import data.nat.basic at the top it fails to prove termination

import data.nat.basic
def myfun : ℕ → ℕ
| 0 := 0
| 1 := 3
| (n + 2) := have h : (n + 2) / 2 < n + 2 := sorry,
  myfun ((n + 2) / 2) -- failed to prove recursive application is decreasing

However, I can prove termination after importing data.nat.basic by providing a proof that (n / 2).succ < n + 2
I assume is has to do with some definition in mathlib taking priority over the core definition, but is there a reason that before importing data.nat.basic the goal is prove (n + 2) / 2 < n + 2 and afterwards the goal is to prove (n / 2).succ < n + 2?

[Junyan Xu]

Maybe the equation compiler uses tactic#simp somewhere, since

example (n : ℕ) : (n + 2) / 2 = (n / 2).succ := by simp

works if data.nat.basic is imported and doesn't work if it's not.

[Niels Voss]

So, in other words, importing data.nat.basic adds extra simp lemmas, changing the goal generated by the equation compiler? That would explain the difference in goals. Does this mean that proving well-founded recursion essentially relies on a non-terminal simp?

[Eric Wieser]

docs#well_founded_tactics.default_dec_tac

[Eric Wieser]

Yes