(a, b) < (c, d) from a ≤ c and b < d

Stream: Is there code for X?

[Violeta Hernández]

I hope I'm not going crazy, because I don't think we actually have this theorem for Prod.Lex

[Violeta Hernández]

That's the relation termination_by (a, b) uses by default, so the lack of this result is a large annoyance

[Violeta Hernández]

This for instance doesn't work

import Mathlib.Order.Basic
import Mathlib.Data.Nat.Defs

theorem recursion (a b : Nat) : True := by
  let (c, d) := (0, 0)
  have : c ≤ a := sorry
  have : d < b := sorry
  exact recursion c d -- failed to prove termination
termination_by (a, b)

[Violeta Hernández]

Oddly enough, we have docs#Prod.Lex.right', but only when the first argument is a natural

[Violeta Hernández]

On a related note, is there any way to tell termination_by to just use the product order instead?

[Violeta Hernández]

Do we not have (a, b) < (c, d) → Prod.Lex _ _ (a, b) (c, d) either?

[Daniel Weber]

Violeta Hernández said:

Do we not have (a, b) < (c, d) → Prod.Lex _ _ (a, b) (c, d) either?

There's docs#Prod.Lex.toLex_strictMono

[Joachim Breitner]

Violeta Hernández said:

On a related note, is there any way to tell termination_by to just use the product order instead?

With docs#WellFounded.wrap you can specify a different order

[Violeta Hernández]

I guess I should mention my actual use case. I can't get this proof to work without the termination_by syntax.

[Violeta Hernández]

Without it, four of the five recursive applications work, but the fifth one (which has the form of the title) doesn't

[Joachim Breitner]

This might be due to the default decreasing_tactic only trying Prod.lex.left and Prod.lex.right but not Prod.lex.right'. Also see https://github.com/leanprover/lean4/issues/3906. Maybe just use termination_by and move on :)