Draft: Overlay for PR#15518

This is an overlay for Coq PR #15518: moving apply to the evar-based unifier. This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q when applying a P <-> Q hypothesis. I think the rest is backwards compatible: mostly about using eapply in places where new existential are created, which the new apply forbids (rightfully).

changed the description

Why do you suggest we change the lemma statement here?

Because the PR also fixes the fact that apply foo when foo : P <-> Q will try P -> Q first now, and in the use cases in stdpp it seems to be better in this order.

The way we resolve this in std++ is by having _1 and _2 variants of the lemma.

Written as an equivalence, I think the current statement makes more sense -- it is called NoDup_fmap, so I would expect fmap to appear on the LHS.

Alright

Also the current statement is way better for rewriting; there you typically want to have difficult = simple (where we have for = in this case).

Right that makes sense. I'll revert the fix to apply, it's too impactful and unrelated but I'll keep this in mind for the new overlay.

changed this line in version 1 of the diff

Is it possible to use rewrite here instead? We usually prefer rewriting with over explicit projN.

It's a conjunction so that wouldn't work in this case I think.

changed this line in version 1 of the diff

This seems to have broken the proof on stable Coq.

That's surprising

changed this line in version 1 of the diff

This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q when applying a P <-> Q hypothesis.

Especially considering the NoDup_fmap example and the inconsistency with rewrite, I'm not sure what's the "right" direction to try first. What's the reason why you favor left-to-right first over right-to-left first?

The main issue I see is that if you apply R A B when R is a record the projections are tried in left to right order, while when R is only an inductive type with a single constructor they are tried right to left. It's just an unnecessary discrepancy in apply's code. But let's leave it to another PR :) The new overlay doesn't change this anymore.

added 1 commit

• 5619246d - Overlay for Coq PR#15518

Compare with previous version

Ok, sounds like a good idea to leave that (discussion) for later.

What's the status of this MR? It's marked as "Draft". Does this mean it's blocked on the Coq PR? For what it is worth, the changes seem fine to me on a quick look.

changed the description

@mattam82 it is not clear to us what the status of this MR is, but it doesn't seem to be immediately actionable on our side? We are going to close the MR, but feel free to reopen when you get back to this.

closed