Zulip Chat Archive

Stream: lean4

Topic: how to use `decreasing_by`


Simon Hudon (Feb 22 2022 at 00:13):

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 (Feb 22 2022 at 08:56):

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

Mario Carneiro (Feb 22 2022 at 09:00):

decreasing_tactic

Sebastian Ullrich (Feb 22 2022 at 09:10):

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 (Feb 22 2022 at 09:12):

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 (Feb 22 2022 at 09:14):

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

Sebastian Ullrich (Feb 22 2022 at 09:27):

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

Mario Carneiro (Feb 22 2022 at 09:34):

it's likely to be significantly faster

Mario Carneiro (Feb 22 2022 at 09:34):

good to know that leo is writing linarith though

Mario Carneiro (Feb 22 2022 at 09:36):

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 (Feb 23 2022 at 00:45):

Thanks! That should do nicely for now


Last updated: Dec 20 2023 at 11:08 UTC