[WIP] Add macro based tactics.

[bollu]

@arthurpaulino I don't have many ideas for how to use macros for tactics. If you do, I'd be happy to add them.

[hargoniX]

I think it would be nicer if we could have some ties back to the syntax chapter here, especially to this part https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/lean/main/syntax.lean#L87-L90, should we add the tactic category here? We should definitely explain at the latest in this chapter that tactic is a syntax category as well even if it should be obvious to the reader at this point, stating it explicitly is better than assuming people understand it.

Regarding custom tactics we can show off a bit here:

• you can demonstrate how to build extensible tactics like trivial: https://github.com/leanprover/lean4/blob/d13fac6f458bd1efd772424066f2a85f8c8ba32a/src/Init/Tactics.lean#L370 or rfl https://github.com/leanprover/lean4/blob/d13fac6f458bd1efd772424066f2a85f8c8ba32a/src/Init/Tactics.lean#L158-L163
• based on this custom trivial tactic you could e.g. add a tactic that does all trivial induction proofs by resolving to induction $n <;> simp_all!
• based on rfl one could imagine adding support for rfl also referring to Iff.rfl instead of just definitional equality

[bollu]

I'm writing the second part that shows off building tactics via macros. Thanks for the examples, I'll incorporate them and send a PR tomorrow.

On Wed, 25 May, 2022, 23:25 Henrik Böving, @.***> wrote:

I think it would be nicer if we could have some ties back to the syntax chapter here, especially to this part https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/lean/main/syntax.lean#L87-L90, should we add the tactic category here? We should definitely explain at the latest here that tactic is a syntax category as well even if it should be obvious to the reader at this point, stating it explicitly is better than assuming people understand it.

Regarding custom tactics we can show off a bit here:

• you can demonstrate how to build extensible tactics like trivial: https://github.com/leanprover/lean4/blob/d13fac6f458bd1efd772424066f2a85f8c8ba32a/src/Init/Tactics.lean#L370 or rfl https://github.com/leanprover/lean4/blob/d13fac6f458bd1efd772424066f2a85f8c8ba32a/src/Init/Tactics.lean#L158-L163
• based on this custom trivial tactic you could e.g. add a tactic that does all trivial induction proofs by resolving to induction $n <;> simp_all!
• based on rfl one could imagine adding support for rfl also referring to Iff.rfl instead of just definitional equality

— Reply to this email directly, view it on GitHub https://github.com/arthurpaulino/lean4-metaprogramming-book/pull/16#issuecomment-1137901875, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAM5ZDNOKCGX7PICH2B55GTVL2SG5ANCNFSM5W6MYUYQ . You are receiving this because you authored the thread.Message ID: @.***>

[arthurpaulino]

I think Mathlib4's iterate is a good target for an "advanced" macro tactic