how to use `decreasing_by`

Stream: lean4

[Simon Hudon]

When using decreasing_by, the default tactics seem to get disabled. Is there an idiomatic way to keep it enabled and just specify and finishing tactic? Or is there a way to invoke (part of) the default tactic?

[Mario Carneiro]

The default tactic has a name, you can just call it

[Mario Carneiro]

decreasing_tactic

[Sebastian Ullrich]

Unfortunately it just fails if the current heuristics are not sufficient, so it's not really possible to "enhance" it. But you can always just copy and override it; for example, this one crudely takes care of many inequations generated by "almost-structural recursion" while we're waiting for linarith.

macro_rules
| `(tactic| decreasing_tactic) =>
 `(tactic|
   (simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
    simp [Nat.add_comm (n := 1), Nat.succ_add, Nat.mul_succ]
    try apply Nat.lt_succ_of_le
    repeat apply Nat.le_step
    first
    | repeat first | apply Nat.le_add_left | apply Nat.le_add_right_of_le
    | assumption
    all_goals apply Nat.le_refl
))

[Mario Carneiro]

Yeah, I think what you really want for those sizeof bounds is to be able to prove a < b where a and b are sums such that every element of a + 1 is in b

[Mario Carneiro]

Do you think that such a tactic should go in core? I can see how to write it

[Sebastian Ullrich]

Would that be preferable to linarith in some way? Leo is already working on the latter.

[Mario Carneiro]

it's likely to be significantly faster

[Mario Carneiro]

good to know that leo is writing linarith though

[Mario Carneiro]

also 100% of the autogenerated well founded subgoals that I have seen are either in that grammar (after unfolding a bunch of definitions) or linarith would not have helped anyway

[Simon Hudon]

Thanks! That should do nicely for now