Well founded relations involving inaccessible terms

Stream: general

[Mario Weitzer]

When I try to define the function

set_option pp.implicit true
set_option pp.notation false

def test : nat × nat → nat × nat
| (0,   f) := (0, f)
| (k+1, f) :=
  have h : prod.lex has_lt.lt has_lt.lt (k, f) (k + 1, f), from
    prod.lex.left f f (nat.lt_succ_self k),
  test (k, f)

Lean (3) asks me to provide a term of type

@prod.lex nat nat (@has_lt.lt nat nat.has_lt) (@has_lt.lt nat nat.has_lt) (@prod.mk nat nat k f)
  (@prod.mk .nat .nat (@has_add.add .nat .nat.has_add k 1) f)

even though h has type

@prod.lex nat nat (@has_lt.lt nat nat.has_lt) (@has_lt.lt nat nat.has_lt) (@prod.mk nat nat k f)
  (@prod.mk nat nat (@has_add.add nat nat.has_add k 1) f)

I really don't get the problem. How would I even provide a term of this type?

[Alex J. Best]

This is indeed very confusing, it looks like something in the default decreasing tactic is failing in a bad way before it tries assumption at all, so even though your term should work its not even tried. I'm not sure if we should expect this to work as is, but fortunately the fix in this example is simple, just tell lean not to be clever, and only try assumption!

def test : nat × nat → nat × nat
| (0,   f) := (0, f)
| (k+1, f) :=
  have h : prod.lex has_lt.lt has_lt.lt (k, f) (k + 1, f), from
    prod.lex.left f f (nat.lt_succ_self k),
  test (k, f)
using_well_founded {dec_tac := `[assumption]}

[Mario Weitzer]

Perfect, thank you!