tactic wishlist

Stream: general

[Koundinya Vajjha]

Not sure if there's something like this in another stream - apologies if there is. What tactics would you like to see written? (By tactics I also include broader metaprogramming constructs, not necessarily those which you would use to discharge proof obligations.)

[Koundinya Vajjha]

@Seul Baek told me he wanted to see a tactic to list lemmas in your current file which are unused by other lemmas. This helps in building theories which avoid spurious lemmas.

[Mario Carneiro]

The big missing tactics for me are metis and omega. metis is important for sledgehammer like operation, and is also useful as a standalone tool for fiddly goals. For omega there are various versions of cooper by Seul that can fill this role, but there is some work to be done to make them usable without a complicated setup and/or a PhD

[Mario Carneiro]

Most of the little tactics I can think of are already written and in mathlib

[Mario Carneiro]

Simon and I have been discussing the possibility of global analysis for linting and things, which could address your unused lemmas example

[Mario Carneiro]

but we are somewhat limited by what lean will give us here, unless we use an external tool like the olean viewer

[Koundinya Vajjha]

How about documentation generation? Is there something for that?

[Mario Carneiro]

I'm not entirely sure what the story is there. @Sebastian Ullrich Lean has some support for a leandoc tool but it's not all there; do you know what the commandline option actually does currently? Is lean 4 any different here?

[Sebastian Ullrich]

I've never used it. This should really be an external tool written in Lean in Lean 4.

[Joseph Corneli]

How about a tactic to convert term-style proofs into tactic style proofs?

[Johan Commelin]

The recent move of mathlib removed the old community-wiki on github. I don't know where to find it now, but it contained a couple of such wishlists.

[Simon Hudon]

Are you referring to this: https://github.com/leanprover-fork/mathlib-backup/wiki

[Simon Hudon]

I think we could move it to leanprover-community

[Johan Commelin]

Aaah, yes that's it. Should we just copy-paste it? Or is there some history that can/should be preserved?

[Simon Hudon]

It can be preserved, I don't know if we want to. @Mario Carneiro You seem to have authored a wiki page with nothing on it on leanprover-community/mathlib. Do you mind if we overwrite it with the one we have in the backup?

[Mario Carneiro]

That's news to me. Go ahead and overwrite it, I don't think I have touched the wiki

[Simon Hudon]

Thanks! I just did. @Johan Commelin you should be able to see what you had before. Let me know if there's anything else to move from the old leanprover-community/mathlib (now located at leanprover-fork/mathlib-backup) to the new leanprover-community/mathlib (formerly leanprover/mathlib)

[Johan Commelin]

Here are another idea:
symmetry at H — replace the equality H with H.symm in the context

[Johan Commelin]

I know this can be done with replace, but I think that it is intuitive to try this with symmetry, and it might be nice for beginners.

[Patrick Massot]

This one is a really nice exercise for you: read the tactic writing tutorial and write it

[Johan Commelin]

I agree. So let me try it once I finish my bureaucracy tomorrow.

[Johan Commelin]

Hmmm, I guess there is a little bit of trouble, namely that symmetry is locked into core.

[Chris Hughes]

Call it symm

[Kenny Lau]

spoilers
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
import tactic.interactive

namespace tactic.interactive
open expr tactic interactive lean.parser

meta def symm (h : parse (tk "at" *> ident)) : tactic unit :=
do env ← get_env,
   exp ← get_local h,
   typ ← infer_type exp,
   let r := get_app_fn typ,
   match environment.symm_for env (const_name r) with
   | (some symm) := do r ← mk_const symm, replace h none ``(%%r %%exp) >> return ()
   | none := fail $ "symmetry' failed, target is not a relation with symmetry."
   end

end tactic.interactive

example (H : 1 = 3) : true :=
begin
  symm at H,
end

[Mario Carneiro]

now make it work with arbitrary locs

[Kenny Lau]

what does that mean?

[Patrick Massot]

potentially several assumptions at the same time, and also the goal

[Kenny Lau]

oh man

[Patrick Massot]

it's not difficult

[Kevin Buzzard]

I always felt bad that I could not teach Chris and Kenny (or indeed anyone at Imperial) tactics, but they seem to have picked it up for themselves. Chris PR'ed a tactic last week :D

[Chris Hughes]

I wouldn't say I've picked it up that well. It was a very straightforward tactic. I hope to do something less trivial at some point.

[Kenny Lau]

and I basically copied my tactic from the original one and modified it a tad

[Kevin Buzzard]

That's how these things start.

[Patrick Thomas]

Would it be useful to have a tactic that transforms a quantified expression into prenex normal form? Is that feasible?

[Chris Hughes]

It's probably just a bunch of the right simp lemmas. Shouldn't be very hard at all. You can set up a prenex simp attribute and simp with prenex should put things in that form. You just have to work out the lemmas to use.

[Patrick Thomas]

I was thinking of doing it from scratch as an exercise, but it is good to know it is feasible first :)