writing tactics - quickstart info

Stream: new members

[Joseph Corneli]

I'm aware of Programming in Lean. Googling just now I found a tech report Meta-programming with the Lean proof assistant. Are there any other guides along these lines for someone starting out writing tactics?

[Kevin Buzzard]

Didn't Patrick write something in the mathlib docs directory?

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md

[Kevin Buzzard]

yes

[Kevin Buzzard]

and that's all I know about.

[Kevin Buzzard]

or at least all I can remember right now

[Joseph Corneli]

thanks for the link!

[Pieter Cuijpers]

I'm starting to play around writing my own tactics as well, but the links provided here are not of much help yet to me. I'm using Lean4, which seems to go about writing tactics a bit differently than Lean3 (at least, the examples provided don't work). I have seen one very very basic example in the Lean4 manual, basically writing a simple macro, but when I try to rework that into my own examples I fail miserably.

Maybe someone can help me get started if I give a small example?

This piece of code works fine in my own context, where I've defined what a Frame is properly.
Also, I've managed to write the proof in a generic way, so that it also works on a number of other theorems if I copy paste it.
So... next step would be to write a macro tactic for it. But how?
Ideally, F is a parameter to that macro.

   try intros
   apply F.antisymmetric
   repeat all_goals try apply (F.meet_def _ _).right.right _ ; constructor
   repeat all_goals
      try apply F.reflexive _
      try apply (F.meet_def _ _).left
      try apply (F.meet_def _ _).right.left
      try apply F.transitive _ _ _ (F.meet_def _ _).left (F.meet_def _ _).left
      try apply F.transitive _ _ _ (F.meet_def _ _).right.left (F.meet_def _ _).left
      try apply F.transitive _ _ _ (F.meet_def _ _).left (F.meet_def _ _).right.left
      try apply F.transitive _ _ _ (F.meet_def _ _).right.left (F.meet_def _ _).right.left

Any suggestions?

[Heather Macbeth]

@Pieter Cuijpers Feel free to ask this kind of question in #metaprogramming / tactics for more visibility. A quick idea: tactic#apply_rules might help encapsulate this logic. It takes a list of lemmas, or an attribute with which several lemmas have been tagged, and it tries applying all these lemmas to the goal until none of them is applicable any longer.

[Heather Macbeth]

In your case, it looks like F is an equivalence relation, and F.meet_def a b contains some pieces .left, .right.left, and .right.right which are identities featuring that equivalence relation. Is that right? If so, it seems to have similarities to things which are well-studied. For example, maybe you could pass to the quotient by F, and then use the powerful tactic tactic#cc.

[Pieter Cuijpers]

Thanks for the response, I'll ask again in the right stream. Your answer is interesting, but seems inapplicable to Lean4?

[Heather Macbeth]

@Pieter Cuijpers You're right that I linked to Lean 3 documentation, but apply_rules has already been ported to Lean 4, and cc is expected to be ported.

[Pieter Cuijpers]

Ah, I'll dig a bit deeper then.
Still wondering how to write my own though...

[Adam Langley]

(deleted)