Zulip Chat Archive

Stream: general

Topic: undocumented core tactics


view this post on Zulip 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',

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:57):

constructor_matching too I think

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:57):

Just to note that this follows from a conversation here

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:57):

Do you fancy telling me docstrings for these tactics?

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:57):

rsimp is simp but more... robust?

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:58):

propagate_tags propagates tags

view this post on Zulip Johan Commelin (Apr 09 2020 at 09:58):

rintro is intro but more... robust?

view this post on Zulip Johan Commelin (Apr 09 2020 at 09:58):

rsimp is simp but more... recursive?

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:58):

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

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:58):

I guessed.

view this post on Zulip Johan Commelin (Apr 09 2020 at 09:59):

Let's fix this in Lean 3.8.1 (-;

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:59):

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

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:59):

guard_expr_eq is actually an interactive tactic

view this post on Zulip Mario Carneiro (Apr 09 2020 at 10:00):

it looks useful for testing

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2020 at 10:03):

propagate_tags is a noninteractive tactic

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 09 2020 at 10:16):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 09 2020 at 11:21):

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

view this post on Zulip Mario Carneiro (Apr 09 2020 at 11:23):

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

view this post on Zulip Mario Carneiro (Apr 09 2020 at 11:23):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 11:49):

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

view this post on Zulip 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."?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 11:51):

Does cases have any effect on a goal?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 11:51):

!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 09 2020 at 11:53):

it's small_nat causing problems again

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 11:54):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 11:56):

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

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 11:56):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 11:58):

(The error reporting could be improved.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 12:01):

mathlib makes a mess of the interactive namespace too.

view this post on Zulip 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).

view this post on Zulip 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.-/

view this post on Zulip Johan Commelin (Apr 09 2020 at 12:24):

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

view this post on Zulip 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. -/
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"] }

view this post on Zulip 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.-/

view this post on Zulip 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.

view this post on Zulip 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"] }

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 12:47):

I don't understand the back ticks in decl_names

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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."

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

? Have I understood correctly?

view this post on Zulip Rob Lewis (Apr 09 2020 at 12:57):

Yep, that's perfect.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 12:59):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 13:06):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 13:32):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 09 2020 at 13:36):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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."

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 09 2020 at 14:25):

(tauto is also tagged "logic")

view this post on Zulip 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.

view this post on Zulip 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").

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 12 2020 at 12:50):

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

view this post on Zulip Reid Barton (Apr 12 2020 at 12:50):

Seems pretty helpful to me :upside_down:

view this post on Zulip 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