RFC: handle well a reused variable after `match` in `decreasing_by`

Current state

Currently, reusing a variable after match often leads to an unsolvable termination goal, for example

def f (a : Nat) := match a with
| 0 => 1
| a1+1 => f (a-1)
termination_by a
decreasing_by

Proof state:

a a1 : Nat
⊢ a - 1 < a1.succ

Proposal

The proof state should be either

a a1 : Nat
⊢ a1.succ - 1 < a1.succ

or

a a1 : Nat
h : a = a1 + 1
⊢ a - 1 < a1.succ

Benefit

match is very common in defining recursive functions, and it is sometimes useful to reuse an argument again. It is true that it can be circumvented with a@(a1+1) which actually include the appropriate equation but without such "hack", it is virtually impossible to reuse a matched variable, which is confusing especially for beginners.

decreasing_by already captures conditions in an if / then / else, so it should not be a significant change to handle match correctly as well.

Community Feedback

I see this as a borderline between a bug, and a feature request, so I haven't discussed on Zulip so far but am happy to do so if it turns out to be difficult / controversial.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No implementation files or tests are named. Start by running the reproducer in the issue and inspect the decreasing_by proof state after the reused variable in match; done means the state includes the refined value or an equality such as a = a1 + 1.