Move equality sections out of Tactics chapter. #13892

jfehrle · 2021-03-02T23:56:59Z

As discussed in #13707.

Zimmi48 · 2021-04-20T10:03:59Z

@jfehrle I've updated your PR to do the usual git dance to preserve the history. I've preserved your changes to these sections and they are now highlighted as part of the last commit (this will also ease the review). Content-wise, this current version is identical to what you had pushed except that the file is now called equality.rst (more in line with its title and its content) and that the two new sections have been split apart (one at the very beginning and one at the very end). The rationale for this is that this new first section contains some basic and essential tactics, while the new last section contains much less common, advanced tactics.

Now on to the actual review (~~though this will be for another day~~).

Add an HTML redirection from rewriting to equality.

doc/sphinx/proofs/writing-proofs/equality.rst

jfehrle · 2021-04-20T16:39:51Z

Is there a simpler way to fetch your changes than this? I don't like having to delete and recreate the branch. Also not sure I need the -f.

git fetch -f origin move_equality_section
git checkout origin/move_equality_section
git branch -D move_equality_section
git checkout -b move_equality_section

SkySkimmer · 2021-04-20T17:21:47Z

Something like this should work

git fetch origin move_equality_section
git checkout move_equality_section
git reset --hard origin/move_equality_section

(the first 2 commute)
Local changes will be lost.

jfehrle · 2021-04-20T17:30:20Z

I'm having trouble rebasing this on master or even just trying to squash it down to 2 commits. For the former, I have a weird conflict on the step that removes things from tactics.rst and then the final commit shows the additions to equality.rst as 2 large blocks, losing the detail.

When I tried to squash, my IDE tool for resolving the conflict--which is quite reliable--can't access the conflicting files for some reason.

Perhaps you could experiment with these and see if it works for you? For the first one in particular, it seems like that might be a recurring problem.

(I started on rebasing because fullGrammar was out of date. I suppose I could skip rebasing for now.)

WDYT?

Zimmi48 · 2021-04-20T19:26:16Z

I'm having trouble rebasing this on master or even just trying to squash it down to 2 commits.

This is expected. You shouldn't try any of the two. The point of all these commits in particular the merge commits is to preserve the git history and it is lost if you rebase or squash. If we really need to rebase, I will have to redo all this work.

(I started on rebasing because fullGrammar was out of date. I suppose I could skip rebasing for now.)

You should probably just regenerate an up-to-date fullGrammar without rebasing.

jfehrle · 2021-04-20T19:56:22Z

The idea is that we avoid rebasing unless it's necessary, and if so, do it just before the PR is merged? This won't create a problem for others later rebasing on a master that includes this PR?

jfehrle · 2021-04-20T19:57:20Z

Updated.

Zimmi48 · 2021-04-21T09:15:08Z

The idea is that we avoid rebasing unless it's necessary, and if so, do it just before the PR is merged?

Yes.

This won't create a problem for others later rebasing on a master that includes this PR?

No, these just are merge commits: hard to rebase but easy to rebase on top.

Zimmi48

Regarding the title of the first section, I don't like using an enumeration that feels exhaustive when it isn't. If you don't like my initial proposal (I understand that "basic" is too vague) what about "Tactics for goals that are equalities"? This would still not be fully precise (symmetry can also be used in a hypothesis and "equality" is too specific) but this would properly encompass most actual use cases of these tactics.

doc/tools/docgram/common.edit_mlg

doc/sphinx/proofs/writing-proofs/equality.rst

jfehrle · 2021-04-21T15:59:12Z

Updated.

jfehrle · 2021-04-21T16:04:11Z

what about "Tactics for goals that are equalities"?

Um, "Tactics for simple equalities"?

jfehrle · 2021-04-24T16:27:29Z

Did this fall through a crack? I think it only needs only a few minutes' attention from you. And would be best to get it merged before some other change forces this to be rebased (which would be a problem because of the history preservation dance).

Zimmi48 · 2021-04-24T17:11:43Z

Ah, I didn't realize that you had pushed a new update. I just thought you had asked some questions. Let me have a look.

doc/sphinx/addendum/micromega.rst

doc/sphinx/proofs/writing-proofs/equality.rst

Zimmi48 · 2021-04-24T17:24:45Z

doc/sphinx/proofs/writing-proofs/equality.rst

+   then :n:`simplify_eq @ident` first introduces the hypothesis in the local
+   context using :n:`intros until @ident`.
+
+.. tacn:: esimplify_eq {? @destruction_arg }


Is it plan to document what destruction_arg is?

I'll put it here for now. All the other tactics that use it are in tactics.rst (and out of date).

Sorry, I should have noticed it earlier but since esimply_eq can be seen as a variant of simplify_eq, it would make sense to indent it and to put the prodn for destruction_arg below simplify_eq.

Now, its definition is so simple, I wonder whether it wouldn't make sense to splice @destruction_arg into {| @one_term_with_bindings | @natural }. In any case, reversing the order of the two productions (since one_term_with_bindings seems to be the main variant) would probably make sense.

jfehrle · 2021-04-24T20:03:06Z

Updated.

Zimmi48

Now that I read the section "Equality and inductive sets" more carefully, considering my proposal to also split out a page dedicated to tactics for inductive types from the tactics chapter, I realize that it would make more sense in such a page than in the one on equality (in particular, it would be presented together with discriminate and injection).

Sorry for seeing this only now. I'll try to see if I can rework things with git to preserve all your changes to this section without doing the move (done, see below).

All my new comments apply to this section only, so you may consider this PR ready from your point of view.

Zimmi48 · 2021-04-25T13:48:31Z

doc/sphinx/proofs/writing-proofs/equality.rst

+   Let :n:`@term` be the proof of a statement with the conclusion :n:`@term__1 = @term__2`.
+   If :n:`@term__1` and :n:`@term__2` are structurally different (in the sense
+   described for the tactic :tacn:`discriminate`), then the tactic
+   ``simplify_eq`` behaves as :n:`discriminate @term`, otherwise it behaves as
+   :n:`injection @term`.
+
+   If the current goal has form :g:`t1 <> t2`, it behaves as
+   :n:`intro @ident; simplify_eq @ident`.
+
+   :n:`simplify_eq @natural` is equivalent to :n:`intros until @natural` then
+   :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last
+   introduced hypothesis.
+
+   If :n:`@bindings` are provided in :n:`@destruction_arg`, they are used to
+   instantiate parameters or hypotheses of :n:`@term`.


Since term doesn't appear anymore in the syntax shown above, we must clarify what it is. Something like:

Suggested change

Let :n:`@term` be the proof of a statement with the conclusion :n:`@term__1 = @term__2`.

If :n:`@term__1` and :n:`@term__2` are structurally different (in the sense

described for the tactic :tacn:`discriminate`), then the tactic

``simplify_eq`` behaves as :n:`discriminate @term`, otherwise it behaves as

:n:`injection @term`.

If the current goal has form :g:`t1 <> t2`, it behaves as

:n:`intro @ident; simplify_eq @ident`.

:n:`simplify_eq @natural` is equivalent to :n:`intros until @natural` then

:n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last

introduced hypothesis.

If :n:`@bindings` are provided in :n:`@destruction_arg`, they are used to

instantiate parameters or hypotheses of :n:`@term`.

Let :n:`@one_term` be the proof of a statement with the conclusion :n:`@term__1 = @term__2`.

If :n:`@term__1` and :n:`@term__2` are structurally different (in the sense

described for the tactic :tacn:`discriminate`), then the tactic

:n:`simplify_eq @one_term` behaves as :n:`discriminate @one_term`, otherwise it behaves as

:n:`injection @one_term`.

If the current goal has form :g:`t1 <> t2`, it behaves as

:n:`intro @ident; simplify_eq @ident`.

:n:`simplify_eq @natural` is equivalent to :n:`intros until @natural` then

:n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last

introduced hypothesis.

If :n:`@bindings` are provided in :n:`@destruction_arg`, they are used to

instantiate parameters or hypotheses of :n:`@one_term`.

Zimmi48 · 2021-04-25T13:49:55Z

doc/sphinx/proofs/writing-proofs/equality.rst


-   If the current goal has form :g:`t1 <> t2`, it behaves as
-   :n:`intro @ident; simplify_eq @ident`.
+   This works the same as :tacn:`simplify_eq` but if the type of :n:`@term` or the


This term should also become one_term with my suggestion above.

Zimmi48 · 2021-04-25T13:51:07Z

doc/sphinx/proofs/writing-proofs/equality.rst


-   This tactic applies to any goal. If :n:`@ident` has type
+   If :n:`@ident` has type


Suggested change

If :n:`@ident` has type

If :n:`@one_term` has type

Zimmi48 · 2021-04-25T13:52:31Z

doc/sphinx/proofs/writing-proofs/equality.rst

   :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
   :n:`@term` of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic


Suggested change

:g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each

:n:`@term` of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic

:g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each

side of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic

Zimmi48 · 2021-04-25T14:56:56Z

I've pushed a proposal at https://github.com/Zimmi48/coq/tree/mv-rewriting. I suggest force-pushing commit f41ebd5 to this PR and keeping cbfbe5e for another PR or for later when we do move this section to a new page (just after this PR is merged). My comments to this section should be kept for this other PR.

Zimmi48 · 2021-04-25T15:37:19Z

To clarify what I mean: IMHO this PR is ready, with just the move of the first Equality section. If you agree, you can just force-push commit f41ebd5 from my branch (or I can take care of it) and I will immediately merge. Then, we can start working on a new page on tactics for inductive types with sections coming from the tactics chapter. And at that point we can reuse your changes to the "Equality and inductive sets" section that I've preserved in commit cbfbe5e.

jfehrle · 2021-04-25T18:33:23Z

Ah, OK, provided you create the new page for inductives ASAP--otherwise too many details to remember, too likely to get lost.

I pulled f41ebd5 and then updated fullGrammar, so this ready to go.

Zimmi48

@coqbot merge now

Zimmi48 · 2021-04-26T09:27:33Z

I have created a new branch: https://github.com/Zimmi48/coq/tree/inductive_page
It includes your changes to the "Equality and inductive sets" section and it consolidates the relevant tactics from the tactic chapter with the proof schemes chapter into a new page on "Reasoning with inductive types". For now, this is only cut-and-paste and it does not include any change to the content. Also, for now, there is no git dance to preserve the history.
I propose that you fetch the contents of this branch and that you focus on this new page for your next prodn conversion. Then we can review your PR and rebase it as often as needed. I will apply the history-preserving git dance to the PR only when it is fully reviewed and ready to merge.

Some notes regarding this new page:

The "detailed example of tactics" chapter contains a section on dependent destruction and dependent induction that would make sense to move to this new page. I didn't do it, leaving it to you to decide whether to do it now or later. (The rest of this chapter is an example of autorewrite that could also be moved close to the documentation of this tactic, and then we would get rid of this strange chapter.)
IMHO discriminate and injection should be moved at the beginning of the section on "Equality and inductive sets". I would also get rid of the word "sets" in this title. Either, replace it with "types" or change the section title to just "Equality" or something like "Equality between inductive terms".
That being said, I don't know how to clearly draw the line between the "Case analysis and induction" section and the "Equality between inductive objects" section. In particular, inversion seems to be in the middle. Maybe @JasonGross has an opinion.

JasonGross · 2021-04-26T12:15:07Z

That being said, I don't know how to clearly draw the line between the "Case analysis and induction" section and the "Equality between inductive objects" section. In particular, inversion seems to be in the middle. Maybe @JasonGross has an opinion.

I think inversion belongs in the equality section, though I agree that it's sort-of in the middle. (Don't forget about inversion_sigma, also.) The line I'm drawing here is that the "case analysis and induction" section should be about tactics which replace occurrences of the given variable with occurrences of their constructors, which I believe inversion does not do. Hence if we generalize a bit, the more accurate (though more-confusing-to-beginners) chapter titles become "(recursively) splitting a variable of (co)inductive type into its constructors" and "extracting useful information from the indices of a variable of inductive type based on the type's constructors and the constructors used in the indices", and then inversion more clearly falls in the latter.

jfehrle · 2021-04-26T17:15:45Z

Thanks for the review and merge. I plan to update the new branch within a few days.

jfehrle · 2021-04-26T19:38:53Z

We need a different name for writing_proofs/inductive.rst because there is already a core/inductive.rst, giving potential for confusion. I can rename the file when I submit it. (I've already spent an hour or two pulling in changes from tactics.rst in another branch, I don't want to repeat that.)

Zimmi48 · 2021-04-27T08:54:43Z

We need a different name for writing_proofs/inductive.rst because there is already a core/inductive.rst, giving potential for confusion.

The symmetry between the two was on purpose. I didn't realize this could create problems. It's a bit sad if the use of directories doesn't allow reusing file names.

Zimmi48 · 2021-04-27T08:55:47Z

I've already spent an hour or two pulling in changes from tactics.rst in another branch, I don't want to repeat that.

Sorry about that, I should have tried doing it for you before the split.

jfehrle · 2021-04-27T19:19:29Z

The problem is that when I'm editing the doc, I'm constantly navigating to files by the last part of the path names. So far they've been unique. If they're not unique, it becomes way too easy to open the wrong file and waste time. And requires more thinking. Any suggestion for a different name?

Zimmi48 · 2021-04-28T17:56:26Z

No good idea. Let's just avoid making the name too long.

Zimmi48 · 2021-04-28T17:57:26Z

The unfortunate thing is that the filename will become the final part of the URL. So its choice should only be based on developers' convenience.

jfehrle added this to the 8.13.2 milestone Mar 2, 2021

jfehrle requested a review from Zimmi48 March 2, 2021 23:56

jfehrle assigned Zimmi48 Mar 2, 2021

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 8, 2021

jfehrle mentioned this pull request Mar 8, 2021

Convert tactics chapter to prodn, part 1 #13916

Closed

jfehrle force-pushed the move_equality_section branch from ebbe402 to 3677629 Compare March 8, 2021 23:52

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 8, 2021

Zimmi48 removed this from the 8.13.2 milestone Apr 1, 2021

jfehrle added the kind: documentation Additions or improvement to documentation. label Apr 17, 2021

Zimmi48 added this to the 8.14+rc1 milestone Apr 20, 2021

Zimmi48 force-pushed the move_equality_section branch from 3677629 to 1c64547 Compare April 20, 2021 09:57

Zimmi48 reviewed Apr 20, 2021

View reviewed changes

Zimmi48 changed the title ~~Move equality sections to rewriting.rst~~ Move equality sections out of Tactics chapter. Apr 20, 2021

Zimmi48 force-pushed the move_equality_section branch from 1c64547 to c6cf0b8 Compare April 20, 2021 10:40

jfehrle force-pushed the move_equality_section branch 2 times, most recently from 3d6bea2 to 2563967 Compare April 20, 2021 20:07

Zimmi48 reviewed Apr 21, 2021

View reviewed changes

jfehrle marked this pull request as ready for review April 21, 2021 15:59

jfehrle requested a review from a team as a code owner April 21, 2021 15:59

jfehrle force-pushed the move_equality_section branch from dade435 to f9a6d34 Compare April 21, 2021 16:05

Zimmi48 reviewed Apr 24, 2021

View reviewed changes

Zimmi48 reviewed Apr 25, 2021

View reviewed changes

Zimmi48 added 7 commits April 25, 2021 16:09

Extract section on equality from tactics chapter.

bc223ef

Move extracted section to page on equality.

e1e3513

Remove extracted section.

2c078e7

Extract equality section with git history.

d8e2a48

Rename rewriting page.

d86690e

Introduce HTML redirection.

f132e9f

Merge rewriting page and equality section.

325dd54

Improve section imported from tactics chapter.

3e40c15

jfehrle force-pushed the move_equality_section branch from 05579f4 to 3e40c15 Compare April 25, 2021 18:28

Zimmi48 approved these changes Apr 26, 2021

View reviewed changes

coqbot-app bot merged commit f7e0539 into coq:master Apr 26, 2021

jfehrle mentioned this pull request Apr 26, 2021

Convert "Reasoning with inductive types" chapter to prodn. #14179

Merged

Zimmi48 mentioned this pull request May 30, 2021

Explode detailed tactic examples #14410

Merged


		This tactic applies to any goal. If :n:`@ident` has type
		If :n:`@ident` has type

		:g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
		:n:`@term` of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic

Move equality sections out of Tactics chapter. #13892

Move equality sections out of Tactics chapter. #13892

Conversation

jfehrle commented Mar 2, 2021

Zimmi48 commented Apr 20, 2021 • edited

jfehrle commented Apr 20, 2021

SkySkimmer commented Apr 20, 2021

jfehrle commented Apr 20, 2021

Zimmi48 commented Apr 20, 2021

jfehrle commented Apr 20, 2021

jfehrle commented Apr 20, 2021

Zimmi48 commented Apr 21, 2021

Zimmi48 left a comment

Choose a reason for hiding this comment

jfehrle commented Apr 21, 2021

jfehrle commented Apr 21, 2021

jfehrle commented Apr 24, 2021

Zimmi48 commented Apr 24, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Apr 24, 2021

Zimmi48 left a comment • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Zimmi48 commented Apr 25, 2021

Zimmi48 commented Apr 25, 2021

jfehrle commented Apr 25, 2021

Zimmi48 left a comment

Choose a reason for hiding this comment

Zimmi48 commented Apr 26, 2021 • edited

JasonGross commented Apr 26, 2021

jfehrle commented Apr 26, 2021

jfehrle commented Apr 26, 2021

Zimmi48 commented Apr 27, 2021

Zimmi48 commented Apr 27, 2021 • edited

jfehrle commented Apr 27, 2021

Zimmi48 commented Apr 28, 2021

Zimmi48 commented Apr 28, 2021

Zimmi48 commented Apr 20, 2021 •

edited

Zimmi48 left a comment •

edited

Zimmi48 commented Apr 26, 2021 •

edited

Zimmi48 commented Apr 27, 2021 •

edited