chore(*): remove well_founded_tactics.default_dec_tac

[bryangingechen]

I had to add a bunch of ugly well-founded proofs here.

Related Zulip threads:

• Mario's suggestion in "moving algebra out of core",
• "well founded tactics"

[gebner]

It's too late now, but it's ok to make leanpkg meta. There's nothing we gain from it being non-meta.

[digama0]

I think we need a means to set the well founded tactic (locally or globally), perhaps using a user attribute. Currently, I think well_founded_tactics.default is magic, being used directly as the default well founded generator if nothing is specified. Since both dec_tac and rel_tac are tactics, we could use a def_replacer setup so that the default is editable, but this would require the default tactic here to evaluate some user attribute (which we can set to run assumption in core).

Alternatively, we can have the magic constant be a tactic well_founded_tactics, that is, we have a tactic that returns a well_founded_tactics that is the default if none is specified (the components of which are themselves tactics which might do various things). This can be similarly set up as a def_replacer defaulting to well_founded_tactics.default.

If we don't do something like this, it seems that tests like mutual_sizeof.lean will be significantly degraded since we will have to specify using_well_founded all the time, even if we move the test to mathlib where we can use much more sophisticated automatic dec tacs like linarith.

[bryangingechen]

Removing the need to add using_well_founded everywhere would be great. def_replacer is in mathlib though, so what should we do here? Is there a set up somewhere I can refer to / copy? (Feel free to push to this branch if you want.)

[digama0]

def_replacer is in mathlib but the techniques that make it work are not. The basic idea is to use a user attribute whose cache is a tactic, the orelse of all registered tactics (or with other fold operation depending on the application), and when you need to call the tactic on input x, you look up the current value of the attribute, eval_expr it as a tactic of the appropriate type and call it with x.