rsuffices?

Stream: general

[Yury G. Kudryashov]

I'm writing a long proof, and it would help to have a tactic rsuffices that relates to suffices as obtain to have. Is it hard to add?

[Yury G. Kudryashov]

I'm using suffices : ∃ a, p a, { rcases this with ⟨a, ha⟩, } for now.

[Kyle Miller]

Maybe this?

import tactic

namespace tactic
namespace interactive
setup_tactic_parser

meta def rsuffices (p : parse obtain_parse) : tactic unit :=
obtain p >> tactic.swap

end interactive
end tactic

You'd use it like rsuffices ⟨a, ha⟩ : ∃ a, p a, { sorry },

[Kyle Miller]

That's taking how suffices works and replacing have in it with obtain.

[Kyle Miller]

(Side question: should we rename obtain to rhave?)

[Yaël Dillies]

Oh please no, correct semantical meaning is my hammer argument for using obtain over rcases :laughing:

[Kyle Miller]

It would be interesting if instead of having all these r-variations we could systematically override builtin tactics. I'm not very serious about this since now's probably not the time for a large change, but, spitballing a design, the way interactive tactics work could be through the attributes system -- a tactic becomes interactive by giving it, say, the @[tactic "foo"] attribute, where you can override previously added tactics. Then, for example, mathlib could supply an "intro" that's implemented by tactic.interactive.rintro.

[Yury G. Kudryashov]

I like the idea of replacing basic tactics with mathlib versions but IMHO this can wait till lean 4.

[Arthur Paulino]

In Lean 4 it's possible to expand a tactic syntax with new behavior without replacing the original one