Avoid many lemmas to implement a tactic

Stream: new members

[Thomas Vigouroux]

Hi there,
I'd like to have help/review of a problem I have in a project.

I have a lemma like the following that has a lot of variables: https://git.sr.ht/~vigoux/busybeaver/tree/master/item/Busybeaver/Partial.lean#L688

I'd like to build a tactic that exploits that lemma, but in order for it to work, I had to specialize it to a huge number of cases for simplification: https://git.sr.ht/~vigoux/busybeaver/tree/master/item/Busybeaver/Partial.lean#L738

Is there a better way around ? Mainly I'd like to have the tactic attempt to simplify the goal as much as possible towards simpler subgoal.

[Thomas Vigouroux]

Actually, maybe a [simp] lemma would help ?

[Eric Wieser]

It looks like your code has changed since you linked to it - can you permalink to a specific revision to avoid the line numbers shifting?

[Thomas Vigouroux]

Here is the currnet lemma: https://git.sr.ht/~vigoux/busybeaver/tree/efcc02e741ec73acf5ee7a95055d13d6fc1e7e0b/item/Busybeaver/Partial.lean#L817
The many lemmas start here: https://git.sr.ht/~vigoux/busybeaver/tree/efcc02e741ec73acf5ee7a95055d13d6fc1e7e0b/item/Busybeaver/Partial.lean#L867

And my version of the tactic is here: https://git.sr.ht/~vigoux/busybeaver/tree/efcc02e741ec73acf5ee7a95055d13d6fc1e7e0b/item/Busybeaver/Partial.lean#L933

[Kyle Miller]

Potentially solve_by_elim could help you. It's for repeatedly applying lemmas.

Could you reformulate these as simp lemmas instead? If it's possible, that seems like a better approach.

[Thomas Vigouroux]

Is it possible to have simp lemmas that are implications?

Do you have documentation for solve_by_elim?