Do not use eta-expansion in `into_forall_forall`.

Looking through the file, I assume this has the same issue?

Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.

What about all the IntoPure instances? We have a whole bunch of eta expansion there as well.

Global Instance into_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
Global Instance into_pure_forall `{!BiPureForall PROP}
    {A} (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).

There are probably more cases that I missed.

Good catch. Also for the Persistent/Affine/etc instances we use eta expansions. It seems quite arbitrary when similar tests work and when they do not.

Lemma test1 `{!CmraDiscrete A} : ⊢@{iProp Σ} ∃ x : A, ✓ x.
Proof. iPureIntro. Admitted. 

Lemma test2 `{CmraDiscrete A} : ⊢ bi_exist (@uPred_cmra_valid (iResUR Σ) A).
Proof. iPureIntro. (* fails *)

Lemma test {PROP : bi} (Φ : nat → PROP) :
  (∀ x, Persistent (Φ x)) → Persistent (bi_exist Φ).
Proof. apply _. (* works *)

Perhaps we should have the convention to remove all needless eta expansions in instances. That will require quite some work to fix though.

It seems quite arbitrary when similar tests work and when they do not.

It's probably related to which unification algorithm is used?

Perhaps we should have the convention to remove all needless eta expansions in instances. That will require quite some work to fix though.

Yeah I think that makes sense. We don't have to fix all instances at once, we can open an issue to track the known remaining work.

It seems a lot like the issue is that class_tactics.ml (i.e. typeclass search) disables the modulo_eta flag. That's why

(@IntoForall PROP ?[Goal] (@bi_forall PROP A P) ?[Goal0])

is solved by

apply @class_instances.into_forall_forall

but not by apply _ or

autoapply @class_instances.into_forall_forall with typeclass_instances

.

This is a super weird restriction and AFAICT there is absolutely no reason for it. I asked about it here https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/TC.20search.20and.20modulo_eta but I don't think the reply is going to be substantially different from "no idea, try to change it and see what breaks".

added 63 commits

3533a0d3...06f499e0 - 60 commits from branch master
2af0383f - Do not use eta-expansion in `into_forall_forall`.
9a940748 - Add test case.
92d67959 - Remove more etas.

Compare with previous version

I tried to push through this change in all instances I could find.

@jung Would be good to have a CI run to see both if this does not cause regressions nor timing issues.

Regression builds are started. Timing results will appear at

It shows -0.1%, so that seems noise.

And I got no emails about regressions either.

Might be worth a changelog, other than that LGTM.

What would be a good place to document the choice that we would like to avoid eta expansions in class instances? Maybe we should have a docs/classes.md to document these things?

I don't see how anyone would find that document. I can't think of a good place, unfortunately. It could go into a comment in classes.v?

I don't see how anyone would find that document.

How is that different from any other file in the docs folder?

I think there are many other design choices w.r.t. type classes that are not documented (modes, opacity, backtracking), so this file might be a place to document such things in the future.

I can't think of a good place, unfortunately. It could go into a comment in classes.v?

I now changed it also for classes such as Persistent and Affine; these are part of bi not proofmode.

I think there are many other design choices w.r.t. type classes that are not documented (modes, opacity, backtracking), so this file might be a place to document such things in the future.

sure, give it a try.

Do not use eta-expansion in `into_forall_forall`.

Merge request reports

Activity