using_well_founded gets stuck on s < s.succ

Stream: general

[Eric Wieser]

Is this behavior expected?

def foo : Π (s b : ℕ), ℕ
| 0 0 := 1
| (nat.succ s) 0 := foo s 0 + 1  -- ⊢ s < s.succ
| 0 (nat.succ b) := foo 0 b + 1  -- ⊢ b < b.succ
| (nat.succ s) (nat.succ b) := foo s.succ b + foo s b.succ  -- ⊢ s < s.succ, ⊢ b < b.succ
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, (f.1 + f.2))⟩] }

Shouldn't docs#well_founded_tactics.trivial_nat_lt be handling this?

[Kevin Buzzard]

What's failing is stuff like

default_dec_tac failed
state:
foo : (Σ' (s : ℕ), ℕ) → ℕ,
b : ℕ
⊢ 0 + b < 0 + b.succ

I see. So your question is really whether this should fail:

example (b : ℕ) : 0 + b < 0 + b.succ :=
begin
  well_founded_tactics.trivial_nat_lt, -- fails
end

Hmm. That tactic appears to have no docstring :-/

[Kevin Buzzard]

That tactic appears to have no docstring, but it looks like meta code I can kind of guess what it does:

meta def trivial_nat_lt : tactic unit :=
comp_val
<|>
`[apply nat.zero_lt_one_add]
<|>
assumption
<|>
(do check_target_is_value_lt,
    (`[apply nat.lt_add_right] >> trivial_nat_lt)
    <|>
    (`[apply nat.lt_add_left] >> trivial_nat_lt))
<|>
failed

None of nat.zero_lt_one_add, nat.lt_add_right, nat.lt_add_left and assumption can close 0+b<0+b.succ so perhaps it's not surprising that it fails?

[Eric Wieser]

https://github.com/leanprover-community/lean/blob/b35d4695da88139a9168f2ad7acf0782e66dc4f0/library/init/meta/well_founded_tactics.lean#L205 runs docs#well_founded_tactics.cancel_nat_add_lt first

[Eric Wieser]

So

example (b : ℕ) : b < b.succ :=
begin
  well_founded_tactics.cancel_nat_add_lt,
  well_founded_tactics.trivial_nat_lt, -- fails
end

is more accurate

[Alex J. Best]

The question of is this expected seems a bit hard to answer as these things are all lacking much documentation, some of these tactics are even implemented in C. The MWE is

def foo : Π (s : ℕ), ℕ
| 0 := 1
| (nat.succ s) := foo s + 1
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf id⟩] }

and this fails even in lean 3.4.2 so this isn't some mathlib-induced regression it seems.
For comparison the Lean 4 analogue

def foo : (s : Nat) → Nat
  | 0 => 1
  | (Nat.succ t) => foo t + 1
termination_by foo s => s

works out of the box

[Eric Wieser]

I made lean#710 to add this lemma

[Eric Wieser]

Given that docs#nat.lt_succ_self is basically half the definition of lt, I think it can be argued to be "trivial" enough for trivial_nat_lt.