GuessLex confused by decreasing_by proof that fails on “wrong” measures

[nomeata]

In #4522 an innocent change broke GuessLex in the sense that the GuessLexTricky.lean test case broke, even though giving the termination measure explicitly the decreasing_by proof works (and it starts with all_goals). I’d expect GuessLex to work there.

See 390943f (if it isn’t merged already), or here:

macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.le_refl)
macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.succ_lt_succ; decreasing_trivial)
macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.sub_le)
macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.div_le_self)

syntax "search_lex " tacticSeq : tactic

macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
    solve
    | apply Prod.Lex.right'
      · $ts
      · search_lex $ts
    | apply Prod.Lex.left
      · $ts
    | $ts
    ))

-- uncomment this to make it work
-- attribute [-simp] Nat.sub_le 

-- set_option trace.Elab.definition.wf true in
mutual
def prod (x y z : Nat) : Nat :=
  if y % 2 = 0 then eprod x y z else oprod x y z
-- termination_by (y, 1, 0)
decreasing_by
  all_goals
    simp_wf
    search_lex solve
      | decreasing_trivial
      | apply Nat.bitwise_rec_lemma; assumption

def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
-- termination_by (y, 0, 1)
decreasing_by
  simp_wf
  search_lex solve -- wrapping this in try makes GuessLex work
      | decreasing_trivial
      | apply Nat.bitwise_rec_lemma; assumption

def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
-- termination_by (y, 0, 0)
decreasing_by
  simp_wf
  search_lex solve
    | decreasing_trivial
    | apply Nat.bitwise_rec_lemma; assumption

end

This isn’t high priority, but at some point I’d like to get to the bottom of this.

Versions

4.10.0-nightly-2024-06-19

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

It looks like this got fixed with #5016. Probably the problem was that simp_wf was unexpectedly closing a goal somewhere?