Moving general-purpose rapply from Programs to Init

[herbelin]

Who has experience with rapply? Shouldn't it be at some time the default apply (or, at least, unifall would lead to identify apply and rapply, right?)?

There is an alternative definition of rapply in TLC (and Software Foundations) which seems currently broken. Since there is a version of rapply already in Coq, maybe should we just rely on this one??

• Added changelog (?)
• Updated documentation.

[andres-erbsen]

I believe rapply and apply also differ in elaboration order and handling of /\ in hypotheses (and maybe lemmas). @JasonGross probably knows

[JasonGross]

I'm in favor.

I agree that the implementation of apply should be moved to the refine engine (ideally while keeping the current behavior of decomposing single-constructor inductives). However, the distinction between apply and eapply should be kept, and the move should be done in OCaml, not Ltac, I think.

[herbelin]

I realize that Program's rapply tries maximal application first, so that it may encounters limits of unification and fail on non atomic goals with flexible head variables, as in:

Require Import Program.
Axiom A : forall R:nat -> Prop,  forall x, R x.
Goal forall R:nat -> Prop,  forall x, R x.
Fail rapply A. (* Unable to unify "?Goal ?Goal0" with "forall (R : nat -> Prop) (x : nat), R x" *)

I guess that the motivation to start with maximal application is efficiency, so I don't know what to think.

This can be addressed if moved to OCaml though.

[Alizter]

I would prefer an OCaml implementation for rapply since we are paying attention to it. I'm also of the non-blocking opinion that the prelude should be reduced not increased. i.e. If a tactic is considered built-in, then it should be built-in.

[herbelin]

I would prefer an OCaml implementation for rapply

I made an experimental branch at https://github.com/herbelin/github-coq/pull/new/master+native-rapply so that we can discuss what to do with it, based on concrete code.

It provides rapply and erapply and supports destructing single-constructor. The rapply in and erapply in are still to be done though.

[gares]

@coqbot run full CI

[SkySkimmer]

@coq/stdlib-maintainers this has been stalled for a while, please take a decision (eg merge / close / say that something specific needs to be done before merge)

If you merge before the branch you can put back the milestone.

[SkySkimmer]

ping @coq/stdlib-maintainers

[andres-erbsen]

I am in favor of merging one implementation or the other. The Ltac one looks good to me despite limitations; if we want the OCaml one somebody else should review in detail. I don't have a particular preference for it being in prelude, so if those opposing that placement could offer an alternative that might be better indeed.

[JasonGross]

I am a fan of moving this to Init. I think probably an OCaml variant might be better, but I'm happy to have this merged and defer the decision on the OCaml implementation to later.

[andres-erbsen]

Hearing no suggested changes, I intend to merge this PR next time I look at it.

[andres-erbsen]

@coqbot run full ci

it's been almost a year

[andres-erbsen]

@coqbot merge now