## Stream: general

### Topic: undocumented core tactics

#### Kevin Buzzard (Apr 09 2020 at 09:55):

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 (Apr 09 2020 at 09:56):

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 (Apr 09 2020 at 09:57):

constructor_matching too I think

#### Kevin Buzzard (Apr 09 2020 at 09:57):

Just to note that this follows from a conversation here

#### Kevin Buzzard (Apr 09 2020 at 09:57):

Do you fancy telling me docstrings for these tactics?

#### Mario Carneiro (Apr 09 2020 at 09:57):

rsimp is simp but more... robust?

#### Mario Carneiro (Apr 09 2020 at 09:58):

propagate_tags propagates tags

#### Johan Commelin (Apr 09 2020 at 09:58):

rintro is intro but more... robust?

#### Johan Commelin (Apr 09 2020 at 09:58):

rsimp is simp but more... recursive?

#### Rob Lewis (Apr 09 2020 at 09:58):

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

I guessed.

#### Johan Commelin (Apr 09 2020 at 09:59):

Let's fix this in Lean 3.8.1 (-;

#### Kevin Buzzard (Apr 09 2020 at 09:59):

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 (Apr 09 2020 at 09:59):

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 (Apr 09 2020 at 09:59):

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

#### Mario Carneiro (Apr 09 2020 at 09:59):

guard_expr_eq is actually an interactive tactic

#### Mario Carneiro (Apr 09 2020 at 10:00):

it looks useful for testing

#### Mario Carneiro (Apr 09 2020 at 10:01):

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

#### Mario Carneiro (Apr 09 2020 at 10:02):

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

#### Mario Carneiro (Apr 09 2020 at 10:03):

propagate_tags is a noninteractive tactic

#### Mario Carneiro (Apr 09 2020 at 10:07):

Here's an example of constructor_matching:

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


#### Mario Carneiro (Apr 09 2020 at 10:11):

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 (Apr 09 2020 at 10:16):

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

#### Kevin Buzzard (Apr 09 2020 at 11:19):

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 (Apr 09 2020 at 11:21):

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

#### Johan Commelin (Apr 09 2020 at 11:21):

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

#### Mario Carneiro (Apr 09 2020 at 11:23):

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

#### Mario Carneiro (Apr 09 2020 at 11:23):

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

#### Kevin Buzzard (Apr 09 2020 at 11:48):

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 (Apr 09 2020 at 11:48):

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 (Apr 09 2020 at 11:49):

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

#### Kevin Buzzard (Apr 09 2020 at 11:50):

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

#### Mario Carneiro (Apr 09 2020 at 11:51):

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

#### Kevin Buzzard (Apr 09 2020 at 11:51):

Does cases have any effect on a goal?

#### Rob Lewis (Apr 09 2020 at 11:51):

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.

!

#### Rob Lewis (Apr 09 2020 at 11:52):

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 (Apr 09 2020 at 11:52):

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 (Apr 09 2020 at 11:53):

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 (Apr 09 2020 at 11:53):

it's small_nat causing problems again

#### Rob Lewis (Apr 09 2020 at 11:54):

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 (Apr 09 2020 at 11:54):

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

#### Rob Lewis (Apr 09 2020 at 11:54):

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 (Apr 09 2020 at 11:55):

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

#### Kevin Buzzard (Apr 09 2020 at 11:56):

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

#### Kevin Buzzard (Apr 09 2020 at 11:56):

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

#### Kevin Buzzard (Apr 09 2020 at 11:57):

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 (Apr 09 2020 at 11:58):

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

#### Rob Lewis (Apr 09 2020 at 11:58):

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 (Apr 09 2020 at 11:58):

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 (Apr 09 2020 at 11:58):

(The error reporting could be improved.)

#### Scott Morrison (Apr 09 2020 at 11:59):

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 (Apr 09 2020 at 12:01):

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 (Apr 09 2020 at 12:01):

mathlib makes a mess of the interactive namespace too.

#### Kevin Buzzard (Apr 09 2020 at 12:02):

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

#### Kevin Buzzard (Apr 09 2020 at 12:15):

/-- 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 (Apr 09 2020 at 12:24):

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

#### Kevin Buzzard (Apr 09 2020 at 12:27):

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. -/
{ name       := "ac_refl",
category   := doc_category.tactic,
decl_names := [tactic.interactive.ac_refl],
tags       := ["core", "lemma application"] }

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


#### Johan Commelin (Apr 09 2020 at 12:27):

/-- 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 (Apr 09 2020 at 12:45):

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 (Apr 09 2020 at 12:47):

Like this?

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


#### Kevin Buzzard (Apr 09 2020 at 12:47):

I don't understand the back ticks in decl_names

#### Kevin Buzzard (Apr 09 2020 at 12:47):

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 (Apr 09 2020 at 12:52):

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 (Apr 09 2020 at 12:54):

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 (Apr 09 2020 at 12:57):

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.
-/
{ name       := "rw",
category   := doc_category.tactic,
decl_names := [tactic.interactive.rw, tactic.interactive.rewrite],
tags       := ["core", "basic"] }


? Have I understood correctly?

#### Rob Lewis (Apr 09 2020 at 12:57):

Yep, that's perfect.

#### Rob Lewis (Apr 09 2020 at 12:58):

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 (Apr 09 2020 at 12:59):

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

#### Kevin Buzzard (Apr 09 2020 at 13:02):

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 (Apr 09 2020 at 13:06):

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

#### Rob Lewis (Apr 09 2020 at 13:10):

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 (Apr 09 2020 at 13:26):

#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 (Apr 09 2020 at 13:31):

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 (Apr 09 2020 at 13:32):

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

#### Scott Morrison (Apr 09 2020 at 13:35):

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 (Apr 09 2020 at 13:36):

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

#### Scott Morrison (Apr 09 2020 at 13:37):

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 (Apr 09 2020 at 13:37):

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 (Apr 09 2020 at 13:48):

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 (Apr 09 2020 at 13:58):

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 (Apr 09 2020 at 13:59):

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

#### Rob Lewis (Apr 09 2020 at 14:00):

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 (Apr 09 2020 at 14:11):

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 (Apr 09 2020 at 14:25):

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 (Apr 09 2020 at 14:25):

(tauto is also tagged "logic")

#### Bryan Gin-ge Chen (Apr 09 2020 at 14:28):

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 (Apr 12 2020 at 11:18):

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 (Apr 12 2020 at 11:18):

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

#### Kevin Buzzard (Apr 12 2020 at 11:22):

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 (Apr 12 2020 at 12:50):

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

#### Reid Barton (Apr 12 2020 at 12:50):

Seems pretty helpful to me :upside_down:

#### Patrick Massot (Apr 12 2020 at 13:46):

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

Last updated: May 08 2021 at 04:14 UTC