Alternate definitions of rapply

[patrick-nicodemus]

This PR introduces two commits which define slightly different and weaker versions of the rapply tactic.

The first commit is intended to behave the same way as the original rapply wherever it succeeds, but it only succeeds if nrapply succeeds.

The second commit has a simpler definition but behaves slightly differently. In particular it has different shelving/unshelving behavior for subgoals, so most changes in the second commit are goal renumberings. It is also apparently slightly weaker due to the fact that typeclasses eauto is called on each typeclass goal individually, not all goals together.

The "unify" tactic in Ltac apparently fails if it does not instantiate all existential variables, so it is not applicable here.

[jdchristensen]

The first commit is pretty good. But I think we should introduce tapply defined exactly like the old rapply, so that the code changes can be just a single letter change without extra parentheses and underscores. (However, there are a few cases where the changed code in the first commit is better than it was before. E.g. if rapply can be changed to exact without any other changes to the term, then that's better.)

[jdchristensen]

BTW, if we go ahead with this, we need to adjust rapply', srapply and srapply' as well. (But note that the primed versions are not used anywhere, so to test the changes, you'd need to temporarily add primes in a few places.)

[patrick-nicodemus]

As suggested, I have added primes to a half dozen instances of these tactics to check that the new primed versions work correctly where the original primed versions work correctly.

[jdchristensen]

This is looking very clean. Besides optionally seeing if Jason's suggestions work for us, my only other thought is that we might rename nrapply to napply (and snrapply to snapply). Then the pattern is a bit more clear: napply, rapply and tapply, each with an optional s. If we do this, it should be a separate commit, because it will be big. I could go either way.

[patrick-nicodemus]

I have force pushed the branch.

1. The first commit is identical to what it was before except that we use Jason's 3rd definition. Jason's 3rd definition is identical in behavior to the one I originally proposed, and it is more readable. There are no other changes to the first commit other than redefining rapply and the other tactics.
2. The second commit uses Jason's first definition and fixes all breakages over the first commit. The first definition has slightly different shelving behavior, it is less powerful in some places but more powerful in others because of the call to typeclasses eauto, I suppose. As a result, some proofs in this commit become longer and others become shorter (a few occurrences of exact _ are removed.) It has the performance advantage of not wasting time by calling nrefine and refine on the same goal. Also, the keyword simple does not perform any beta reduction when trying to unify with the goal, so we have to add cbv beta explicitly in a few places.

I noticed that leq is declared as a Class and some commonly used inequalities are used as Instances. This seems like a clever use of the typeclass system, but I broke some of these. Some inequalities are proved by rapply leq_trans. to solve a goal without any other parameters being fed to leq_trans, i.e., refine ?x ?y ?z ?x<=y ?y<=z. Now, of course x,z can be solved by unification with the goal, but then you still have to instantiate refine x ?y z ?(x<=y) ?(y<=z). Since ?x<=y is a typeclass, we can use typeclass search to guess it, which involves instantiating y. Since instances which are arguments/hypotheses of the current goal are of high priority, it looks like the typeclass search tends to choose inequalities in the context, which tends to work well. I'm a little concerned that reading the code becomes a bit more confusing if readers don't understand how or why rapply is automatically instantiating all the missing variables it needs.

[jdchristensen]

Both versions seem fine to me. Do you have a preference?

If we go with Jason's first definition, I think things can be rewritten so that some tactics build on others. For example, I think rapply can be simply srapply; shelve_unifiable, right?

With Jason's first definition, the meaning of the s prefix would be slightly different between rapply and the other two (nrapply and tapply), if I understand correctly, so that's one (very minor) argument against it.

[patrick-nicodemus]

I don't know.
I like that calling typeclasses eauto makes some of the proofs shorter; I assume that typeclasses eauto takes very little time on holes that are not typeclasses, so I'm not concerned about performance.
Regarding the meaning of the "s" prefix, I find this annoying, because IMO it would be nice to have a hierarchy of three tactics napply < rapply < tapply which differ only in the typeclass behavior and not with respect to unrelated things like whether beta reduction is employed in unification or shelving behavior. So, I will lean towards the original definition (Jason's third definition) because I think that that linear hierarchy is easy to understand, and the "simple" prefix is orthogonal, which makes it easier to incorporate.

[jdchristensen]

Going with Jason's third definition (using assert_succeeds) seems like a good choice.

@Alizter What do you think about renaming nrapply to napply? Then a single letter n, r or t selects the strength of the typeclass search, and an optional s affects the shelving behaviour.

[Alizter]

Going with Jason's third definition (using assert_succeeds) seems like a good choice.

@Alizter What do you think about renaming nrapply to napply? Then a single letter n, r or t selects the strength of the typeclass search, and an optional s affects the shelving behaviour.

Seems good to me.

[patrick-nicodemus]

I have reorganized and rewritten the comments in Basic/Tactics to present the tactics in the order: napply, rapply, tapply, snapply, srapply, stapply, where we first explain what napply does, then how rapply builds on it, then how tapply builds on rapply.

[jdchristensen]

LGTM modulo one change in STYLE.md

[Alizter]

I'm in favour of merging #2245 before this. There are a few things left in this PR that I would like to change, and it makes more sense for #2245 to be merged before.

[jdchristensen]

@Alizter What else are you thinking of changing in this PR?

[Alizter]

@jdchristensen There were a few lines where tapply was introduced but napply could be used with a bit of tweaking. Some of them were finishing rapplys which is why the other PR will solve some of them.

[Alizter]

FYI I will attempt to rebase this now.

[Alizter]

My rebase has scrubbed your ownership of the commits @patrick-nicodemus. I will rebase again and add you as the main author.

[Alizter]

I'm not sure what I am doing wrong. @jdchristensen do you remember how to give ownership of a commit?

[jdchristensen]

I'm not sure what I am doing wrong. @jdchristensen do you remember how to give ownership of a commit?

I thought that by default an interactive rebase would preserve the commit author. I'm not sure how to fix it, but it must be a common thing to need to adjust so I imagine there's a way.

[jdchristensen]

My tool (magit) provides a keystroke to set the commit author during a rebase, so I can try to fix these if you want.

[Alizter]

@jdchristensen That would be great, thanks!

[Alizter]

Actually, it looks like the ownership information is correct. Just that the GitHub interface is only showing my picture. Weird.

[Alizter]

@jdchristensen If you do rebase, you might need to do so on top of #2248.

[jdchristensen]

I agree that the git log info looks correct, so I won't do a rebase.

[Alizter]

I will rebase this again.

[Alizter]

That's all rebased, and all comments addressed. Merging now.

[Alizter]

Thanks @patrick-nicodemus, great work as always.