undocumented core tactics

Stream: general

[Kevin Buzzard]

I'm thinking about documenting core tactics. Below are some core tactics, with no docstrings, and I have no idea what any of them do. Is an end user ever supposed to use any of them? I propose not adding them to the community docs. I suspect many are intermediate constructions which are not supposed to be used by the end user (but on the other hand all of them are in tactic.interactive...). Is anyone's favourite interactive tactic on this list?

cases_arg_p,
cases_core,
concat_tags,
constructor_matching,
exacts._main,
existsi._main,
get_rule_eqn_lemmas,
guard_expr_eq,
propagate_tags,
rsimp,
rw_rule,
rw_rule.cases_on,
rw_rule.has_reflect,
rw_rule.mk,
rw_rule.mk.inj,
rw_rule.mk.inj_arrow,
rw_rule.no_confusion,
rw_rule.no_confusion_type,
rw_rule.pos,
rw_rule.rec,
rw_rule.rec_on,
rw_rule.rule,
rw_rule.symm,
rw_rule_p,
rw_rules,
rw_rules_t,
rw_rules_t.cases_on,
rw_rules_t.end_pos,
rw_rules_t.has_reflect,
rw_rules_t.mk,
rw_rules_t.mk.inj,
rw_rules_t.mk.inj_arrow,
rw_rules_t.no_confusion,
rw_rules_t.no_confusion_type,
rw_rules_t.rec,
rw_rules_t.rec_on,
rw_rules_t.rules,
simp_core,
simp_core_aux,
to_expr',

[Mario Carneiro]

propagate_tags is somewhat useful but it's primarily meant for non-interactive use. The only one there that is an actual end user tactic is rsimp

[Mario Carneiro]

constructor_matching too I think

[Kevin Buzzard]

Just to note that this follows from a conversation here

[Kevin Buzzard]

Do you fancy telling me docstrings for these tactics?

[Mario Carneiro]

rsimp is simp but more... robust?

[Mario Carneiro]

propagate_tags propagates tags

[Johan Commelin]

rintro is intro but more... robust?

[Johan Commelin]

rsimp is simp but more... recursive?

[Rob Lewis]

A lot of those are misplaced in the tactic.interactive namespace.

[Kevin Buzzard]

I guessed.

[Johan Commelin]

Let's fix this in Lean 3.8.1 (-;

[Kevin Buzzard]

But now would be a good time for someone to write a docstring for any tactic they want to save on this list.

[Rob Lewis]

At some point in the doc gen stuff I wanted to enforce that every declaration in tactic.interactive had a doc string and would get displayed.

[Rob Lewis]

But there was way too much junk in the namespace to do this.

[Mario Carneiro]

guard_expr_eq is actually an interactive tactic

[Mario Carneiro]

it looks useful for testing

[Mario Carneiro]

although it's a bit odd that the first argument is an expr and the second is parsed

[Mario Carneiro]

actually scratch that, I think the main intended use of this function is via guard_target and guard_hyp

[Mario Carneiro]

propagate_tags is a noninteractive tactic

[Mario Carneiro]

Here's an example of constructor_matching:

example : true ∧ true ∧ true ∨ true ∧ true :=
begin
  constructor_matching* [_∧_, _∨_]; trivial,
end

[Mario Carneiro]

rsimp is something I would love to read a doc string about. It uses smt stuff internally, it probably does some cc inside it, and it strangely has no space for lemma inputs like simp; I think it relies entirely on annotations and things in the context

[Patrick Massot]

I think rsimp is documented in the Lean 3 meta-programing paper.

[Kevin Buzzard]

If someone who understands something about any of the tactics listed above could just give me a docstring sentence while I fix up all the other issues I've run into, that would be great. Anything in the above list which we don't get a sentence for will not be included because I know 99% of us can live without all of them

[Johan Commelin]

@Kevin Buzzard Do you have a branch where you collect them? Or do you want people to post in this thread?

[Johan Commelin]

I don't think I've ever used any of the tactics on that list

[Mario Carneiro]

I think rsimp and constructor_matching are the only two that need documentation

[Mario Carneiro]

the rest are just non-interactive tactics and should be documented elsewhere

[Kevin Buzzard]

Can someone confirm that the core docstrings for cases_matching and cases_type are incorrect? They both seem to make the claim in their example that they will do something to the goal, but in experiments I can only make these tactics do something to do hypotheses.

[Kevin Buzzard]

Currently the docstring for cc is Tries to prove the main goal using congruence closure.. I remember this being no help to me whatsoever as a beginner. Does anyone have any better suggestions, e.g. a reference?

[Kevin Buzzard]

congr has no docstring. Should the docstring be "This tactic is broken -- use congr'"?

[Kevin Buzzard]

Are we happy with dsimp documentation "dsimp is similar to simp, except that it only uses definitional equalities."?

[Mario Carneiro]

cases_matching and cases_type are more automated variants of cases, and have a similar effect on the goal

[Kevin Buzzard]

Does cases have any effect on a goal?

[Rob Lewis]

Kevin Buzzard said:

Can someone confirm that the core docstrings for cases_matching and cases_type are incorrect? They both seem to make the claim in their example that they will do something to the goal, but in experiments I can only make these tactics do something to do hypotheses.

I think both use "goal" to refer to the context + target, not just the target.

[Kevin Buzzard]

!

[Rob Lewis]

They change the context, which you could argue is part of the goal. But "goal" is used differently in e.g. tactic.get_goals

[Kevin Buzzard]

That's it for now, although I could mention that the iterate docstring displays with one of those "error while executing interactive.param_desc" errors. Is this something which can be fixed now?

[Rob Lewis]

Kevin Buzzard said:

congr has no docstring. Should the docstring be "This tactic is broken -- use congr'"?

If congr' isn't in core, then no, it shouldn't be.

[Mario Carneiro]

it's small_nat causing problems again

[Rob Lewis]

Kevin Buzzard said:

Currently the docstring for cc is Tries to prove the main goal using congruence closure.. I remember this being no help to me whatsoever as a beginner. Does anyone have any better suggestions, e.g. a reference?

There's a pretty good tactic doc that we add for cc in mathlib already.

[Kevin Buzzard]

Oh gosh, are some of these things in already??

[Rob Lewis]

Kevin Buzzard said:

Are we happy with dsimp documentation "dsimp is similar to simp, except that it only uses definitional equalities."?

I mean, it could definitely be improved...

[Rob Lewis]

The only core tactics with doc entries (that are tagged with the core label, anyway) are cc, simp, and conv.

[Kevin Buzzard]

That's great news about conv because this has no docstring.

[Kevin Buzzard]

So I can just delete cc, simp and conv from my list I guess?

[Kevin Buzzard]

In fact I have to delete simp, running add_tactic_doc gives the error invalid object declaration, environment already has an object named 'tactic_doc._2018668402'. That's clever. Is some hashing going on?

[Scott Morrison]

Ideally you could transport the doc entries for cc, simp and conv from mathlib into doc strings in core?

[Rob Lewis]

If you're planning to make a PR to core adding doc strings, maybe you could use the first few sentences of the doc entries for those tactics? They're all pretty detailed entries, probably too much for doc strings.

[Rob Lewis]

Kevin Buzzard said:

In fact I have to delete simp, running add_tactic_doc gives the error invalid object declaration, environment already has an object named 'tactic_doc._2018668402'. That's clever. Is some hashing going on?

Yes, this is because there's already a doc entry with the name simp.

[Rob Lewis]

(The error reporting could be improved.)

[Scott Morrison]

Was your list above of undocumented tactics exhaustive? If so, perhaps we should go through removing most of them from the interactive namespace.

[Rob Lewis]

Scott Morrison said:

Was your list above of undocumented tactics exhaustive? If so, perhaps we should go through removing most of them from the interactive namespace.

It wouldn't hurt, but I think it's a decent amount of effort that is better spent on other things.

[Rob Lewis]

mathlib makes a mess of the interactive namespace too.

[Kevin Buzzard]

It wasn't quite exhaustive -- congr has no docstring (and I still don't know what to write for it).

[Kevin Buzzard]

/-- Basically equivalent to `convert rfl`, the `congr` tactic attempts to identify both
  sides of an equality goal `A = B`, leaving as new goals the subterms of `A` and `B`
  which are not definitionally equal. Note that `congr` can be over-aggressive at times;
  in mathlib the `congr'` tactic provides a more refined approach.-/

[Johan Commelin]

@Kevin Buzzard Note that convert uses congr under the hood.

[Kevin Buzzard]

I was copying docstrings over for unhelpfully-documented tactics such as ac_refl and rw, where the docstring is just "this is an abbreviation for another tactic". But actually, do we really want both ac_refl and ac_reflexivity in our docs? They are the same tactic. Should we just choose one?

/-- Proves a goal with target `s = t` when `s` and `t` are equal up to the associativity and
commutativity of their binary operations. -/
add_tactic_doc
{ name       := "ac_refl",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.ac_refl],
  tags       := ["core", "lemma application"] }

add_tactic_doc
{ name       := "ac_reflexivity",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.ac_reflexivity],
  tags       := ["core", "lemma application"] }

[Johan Commelin]

/-- The `congr` tactic attempts to identify both sides of an equality goal `A = B`,
 leaving as new goals the subterms of `A` and `B` which are not definitionally equal.
 Example: suppose the goal is `x * f y = g w * f z`. Then `congr` will produce two goals:
 `x = g w` and `y = z`.

 Note that `congr` can be over-aggressive at times; in mathlib the `congr'` tactic provides
 a more refined approach, by taking a parameter that limits the recursion depth.-/

[Rob Lewis]

Should we just choose one?

Yes, maybe mention both names in the doc entry, but it doesn't need two entries. You can put multiple names in the decl_names field.

[Kevin Buzzard]

Like this?

add_tactic_doc
{ name       := "rw",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.rw, `tactic.interactive.rewrite],
  tags       := ["core", "basic"] }

[Kevin Buzzard]

I don't understand the back ticks in decl_names

[Kevin Buzzard]

Note also I added a new tag "basic", which we might be able to point beginners to who want to prove basic goals like the exercises in TPIL or the NNG levels.

[Rob Lewis]

Like that. But if my docs for add_tactic_doc are right, you'll have to add one more field in this case: inherit_description_from := `tactic.interactive.rw since it doesn't know which one to take the entry from.

[Rob Lewis]

decl_names is a list of names. If you just wrote tactic.interactive.foo, this could refer to a definition foo : name. The backticks say "parse this thing as a literal name."

[Kevin Buzzard]

If the "description" is the docstring, then I think I'd rather inherit from rewrite because the docstring for rw is useless (it says "an abbreviation for rewrite"). However if I inherit from rewrite then all the examples use rewrite. Can I instead do this:

/--
`rw e` applies identity `e` as a rewrite rule to the target of the main goal. If `e` is preceded by
left arrow (`←` or `<-`), the rewrite is applied in the reverse direction. If `e` is a defined
constant, then the equational lemmas associated with `e` are used. This provides a convenient
way to unfold `e`.

`rw [e₁, ..., eₙ]` applies the given rules sequentially.

`rw e at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses
in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify
the target of the goal.
-/
add_tactic_doc
{ name       := "rw",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.rw, `tactic.interactive.rewrite],
  tags       := ["core", "basic"] }

? Have I understood correctly?

[Rob Lewis]

Yep, that's perfect.

[Rob Lewis]

But honestly, I'd rather just replace the rw doc string with what you just wrote, and inherit the doc entry from that.

[Rob Lewis]

No reason to keep useless doc strings around if you're writing their replacements anyway.

[Kevin Buzzard]

Yes, there is a PR to core in this. But here's my logic: the PR I'm making for mathlib has a whole load of add_tactic_docs with no docstrings, and the few that do have docstrings correspond exactly to the things which need to be changed in core. So I figured I'd do this one first and see if anyone has comments about my modified docstrings, with the advantage being that it can be deployed quickly. When the mathlib PR has gone through the review process I can then PR to core, and when that has gone through and mathlib catches up with core I can then do a third PR removing the docstrings I'm adding in the first PR. There seems to me to be little point in doing them both simultaneously, because then we'll end up with docs which are suboptimal for a few weeks.

[Rob Lewis]

It sounds like extra work for you, but if you're willing, that's fine :)

[Rob Lewis]

How many things would you have to change in core? We just had a 3.8 release and haven't even moved mathlib over yet. If the review isn't too complicated, you could PR those to core now, we can release 3.8.1, and then your mathlib additions can follow at your leisure.

[Kevin Buzzard]

#2371 . I'm so far from my comfort zone right now I don't really want to be making a core Lean PR until other people have had a chance to look at what I already did. When will the API docs change?

[Rob Lewis]

I'll take a look now! For what it's worth, the people looking at core Lean PRs are a strict subset of those looking at mathlib PRs.

[Rob Lewis]

The docs will update about an hour after the PR gets merged.

[Scott Morrison]

Wow, thanks @Kevin Buzzard! I'm also going through this now, and have already learnt two cool tactics, cases_matching and cases_type.

[Scott Morrison]

Can't we combine the doc entries for erw and erewrite into one?

[Scott Morrison]

I'm not certain of the behaviour of add_tactic_doc, but I think you can just list more than one declaration in the decl_names field.

[Scott Morrison]

You might then need to specify which doc string gets used, using the optional inherit_doc_string_from (or something like that) field.

[Kevin Buzzard]

Yes thanks for this, I may well have missed out other duplicate tactics, I genuinely don't know what half of these things do and part of me is tempted to not put a bunch of them into the API docs

[Rob Lewis]

Okay, I left some comments on the top part. Rather than the long list of suggestions on the PR, it'll be easier for me just to push a commit that adds a bunch of tags.

[Rob Lewis]

I don't have time right this sec, so Kevin or others, if you'd like to tag some tactics, feel free!

[Rob Lewis]

Anything that mainly creates/combines hypotheses should be tagged "context management." Stuff like intro, constructor, etc can be "logic." If a tactic fails when it doesn't close the goal, "finishing."

[Johan Commelin]

Too me something like intro and apply sounds like "basic", where with "logic" I would think of tableau provers or something like that...

[Rob Lewis]

They can be "basic" too, tags aren't exclusive. I say "logic" because they're very close to the core syntax of Lean.

[Rob Lewis]

(tauto is also tagged "logic")

[Bryan Gin-ge Chen]

Thanks for doing this Kevin! I just added some suggestions to the PR, mostly "finishing" tags, and I tried to combine erw and erewrite the way you did rw and rewrite.

[Rob Lewis]

See the result of Kevin's hard work here: https://leanprover-community.github.io/mathlib_docs/tactics.html (use the drop down menu on the left to filter for label "core").

[Rob Lewis]

This makes it much easier to notice what's mislabeled and which doc strings need to be updated!

[Kevin Buzzard]

Most of the new docstrings are directly from core. The next step is to see if we want to change any of the core docstrings. I for one will be very pleased to see the back of An abbreviation for rewrite which people who want to see advanced syntax for rw get.

[Reid Barton]

I mean, if not for that docstring, would you even know that rewrite exists?

[Reid Barton]

Seems pretty helpful to me :upside_down:

[Patrick Massot]

Maybe the title of that page needs to be changed now.