Add Fractional instance for AsFractional

AsFractional admits a very obvious Fractional instance in the case where it's of the form AsFractional (Φ q) Φ q. This commit defines that instance, which would help simplify proofs in #923.

Search issue

This loops with as_fractional_fractional in cases where the typeclass search can't progress in any better way. I've tried to figure out how to prevent it, and the most obvious way would be to remove the typeclass coercion on as_fractional_fractional.

I think doing so makes sense: the only case where the user would want this kind of coercion (and indeed the only place in the Iris codebase where it is used, AFAIK), is when there's an AsFractional in the environment and the user doesn't want to manually destruct it to apply the Fractional inside. I wouldn't expect to go from a Fractional goal backwards to an AsFractional with some evars, for example - but maybe this search behaviour is secretly necessary somewhere?

I would expect that the above case can somehow be handled with a less aggressive hint that doesn't allow for evars, but I couldn't figure out how to define it.

I guess it makes sense that if you have Fractional for an abstract predicate in your context you don't want to give an AsFractional instance.

Declaring this instance using Hint Immediate might be better. (But, there are some issues with Hint Immediate).

Could we have a timing CI run to see this does not cause spurious Fractional searches that slow things down.

Future timing result links:

• examples
• lambda-rust
• gpfsl
• iron

The lambda-rust job diverged. Looks like we do have infinite TC search indeed.

This loops with as_fractional_fractional in cases where the typeclass search can't progress in any better way. I've tried to figure out how to prevent it, and the most obvious way would be to remove the typeclass coercion on as_fractional_fractional.

I guess the question is, when do we need that Fractional instance? We could make it Local to that file. I don't know when it is needed outside, e.g. ↦ has its own Fractional instance so we wouldn't want it to use as_fractional_fractional.

It took me some time to understand the problem in the merge request, but yes, the current MR's approach of having instances for Fractional -> AsFractional and vice versa is bad. My suggestion to use a Hint Immediate for the new Fractional -> AsFractional instance would solve that.

Removing as_fractional_fractional could also be an option. It will break proofs such as:

  Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
    IntoSep P P1 P2.
  Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.

(These instances should not also have a Fractional premise, that would cause redundant search.)

I think proofs such as the above can easily be fixed by having as_fractional_fractional as a local instance, or just destructing AsFractional. (I prefer the latter.)

I guess the question is whether we ever want the as_fractional_fractional instance outside of this file. We have an entire Hint Mode line dedicated only to making that instance work -- indicating that it is a somewhat odd instance.

So the most minimal solution (in terms of change size) is to take out the coercion on as_fractional_fractional and replace it with a Local Hint Immediate to maintain the proofs in the file.

Interestingly, the Hint Mode is intended for as_fractional_fractional, but also affects some other proofs. Marking it Local breaks at least ghost_var_combine_as in iris/base_logic/lib/ghost_var.v, which seems to not progress on typeclass instances because it doesn't match the only other Hint Mode for AsFractional.

That file is also interesting because it manually declares an AsFractional instance based on a Fractional one, just slightly simplified i.e. the type has a Fractional (λ q, Φ q) instance, and also an AsFractional (Φ q) (λ q, Φ q) q instance (compare to AsFractional ((λ q, Φ q) q) (λ q, Φ q) q from fractional_as_fractional.) Removing the manually-declared AsFractional instance also breaks the proof.

I've pushed an updated version using Hint Immediate for review, but I'm happy to write up another approach if there's a better one.

added 2 commits

• 43912cb3 - Add Fractional instance for AsFractional
• a9eb0808 - Add test of fractional_as_fractional

Compare with previous version

The comment still seems relevant if the hint stays, even if as_fractional_fractional no longer is an instance?

Should the hint be made Local?

EDIT: I saw you wrote that breaks other proofs. That means we need to investigate.

Looks like this instance here also relies on using AsFractional 'backwards'

  Global Instance combine_sep_fractional_bwd P P1 P2 Φ q1 q2 :
    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) →
    CombineSepAs P1 P2 P | 50.

Specifically the third premise has a known Φ and q1+q2 and tries to compute the P.

This could in principle use Φ (q1 + q2) as the solution but I guess that also doesn't always work. But experience also says using the same typeclass forwards and backwards will cause problems long-term...

Cc @robbertkrebbers @snyke7

Looking at the AsFractional instances, I think using Φ (q1 + q2) here should be fine. I agree that it is probably better to only use AsFractional forwards.

Also, if backwards is still wanted, I think it should have Hint Mode AsFractional - - + !? Since the q is also used as an input for computing P.

The more restrictive hint mode breaks the mapsto_evar_iSplit test, which relies on a backwards search with an unknown q. Why it's not in head-normal form in that test, I'm not exactly sure.

That test is the only example in the codebase which is affected by restricting the hint mode in this way.

Also, if backwards is still wanted, I think it should have Hint Mode AsFractional - - + !? Since the q is also used as an input for computing P.

Yeah, good point. This is further evidence that AsFractional was not meant to be used backwards.

!928 (merged) should remove our reliance on backwards AsFractional.

Why? What if there's an AsFractional instance without a Fractional instance, and there's a search for Fractional? In fact, exporting both AsFractional and Fractional for a predicate seems an anti-pattern.

Nevermind, I must be missing something: duplicating the Fractional instance seems the regular pattern (also in our codebase). This change will break clients who have Local Instance ... : Fractional Foo ... Global Instance AsFractional (Foo q) Foo q or the like, but they don't seem common.

A lot of the duplication seems to be redex-elimination in the head of AsFractional, that is of the form:

Instance my_pred_fractional : Fractional (λ q, Φ q) := ...
Instance my_pred_as_fractional : AsFractional (Φ q) (λ q, Φ q) q := ...

I don't have a lot of experience with the typeclass machinery, but it seems to be that the second instance should be totally redundant off the back of the first, and there's no clear reason to support a module declaring both.

there's no clear reason to support a module declaring both.

Yes but all existing clients do that. And take more interesting examples like

Instance my_pred_fractional : Fractional (λ q, Φ q v) := ...
Instance my_pred_as_fractional : AsFractional (Φ q v) (λ q, Φ q v) q := ...

or mapsto:

  mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
  mapsto_as_fractional l q v :>
    AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;

Clearly your instance can unify (up to beta-reduction), but would Coq find that solution? And whichever the answer, is that reliable?

Very roughly, unification modulo beta-reduction is undecidable and practical approximations are complex — but Coq does implement some approximation, and AFAIK that's not fully specified (unless you count https://dl.acm.org/doi/10.1145/2784731.2784751 and https://www.cambridge.org/core/journals/journal-of-functional-programming/article/comprehensible-guide-to-a-new-unifier-for-cic-including-universe-polymorphism-and-overloading/19A095CA0645F89A772B7E2B7B3D92B2 — but those describe neither of the two unification algorithms in Coq, just a cleaned up version).

We should decide whether we expect clients to always declare both Fractional and AsFractional instances, and then document that here. From existing practice it seems like the answer is yes we do. @robbertkrebbers you don't happen to remember how this was originally intended?

Note that @jjourdan developed the Fractional interface, see !23 (merged), so I don't remind the original intent.

Since we're all at the Iris workshop this week, let's discuss this in person.

With this new instance, it seems you'd need to remove your own AsFractional instances if fractional_as_fractional triggers, which depends on higher-order unification (HOU). I honestly thought avoiding HOU was the entire point we bothered writing AsFractional instances — even if the boilerplate for the latter is annoying.

Is there a simple and reliable way to test if my own instance is redundant? Is it enough to write the following?

Global Instance ... AsFractional Foo ...
Proof. Fail apply _.

Usually the answer is "obviously yes" but I've never become familiar with HOU's pitfalls (and I venture nobody else has many other Iris users haven't either).

changed this line in version 3 of the diff

it seems you'd need to remove your own AsFractional instances if fractional_as_fractional triggers

Ah yeah, we are risking overlapping instances here... shouldn't it basically be: if your own instances matches the pattern Φ q then don't add it?

This becomes tricky with generic instances though, as per the usual diamond problem. In particular mul_as_fractional_l/r... they keep the P the same so we can try fractional_as_fractional both before and after the mul_ instance, so if P = Φ q there might be duplicated search?

• AsFractional (Φ q) ?Φ' ?q' can have fractional_as_fractional applied, then we search for Fractional Φ
• If that fails we apply mul_as_fractional_l, leading to a new goal AsFractional (Φ q) ?Φ'' (?q'' + ?q'''), which can again have fractional_as_fractional applied (if q unifies with ?q'' + ?q''')
• and then again for mul_as_fractional_r

Though honestly that seems mostly a problem of the mul_ instances? They are not making any progress of the main input to the search (P), hence leading to an exploding search tree.

mul_as_fractional_l/r are already local, and mul_fractional_l/r make progress alright? But you have mul_as_fractional_l and (?q'' + ?q''') in the same sentence and I have no idea what you mean...

Oh, I didn't see that mul_as_fractional_l are local. Never mind then. I wonder what their purpose is then...

added 1 commit

• edff3e1a - Move instance out of scope of looping co-instance

Compare with previous version

My general concern (as a user): this MR reduces boilerplate but risks decreasing reliability with its general AsFractional instance, while Iris usually goes the opposite direction. How big is the risk depends on internals of higher-order unification (HOU) which are intentionally under-specified (and possibly evolving?): will the new instance sometimes unify unexpectedly, or is it limited to unary predicates? If somebody understands the answer, great.

I personally don't understand those details, but I've seen HOU get (seldom) in the way of other solutions, like https://github.com/bedrocksystems/BRiCk/blob/master/theories/lang/bi/spec/frac_splittable.v.

cc @janno I guess.

Basically your concern is that for mapsto l q v, the instance might apply with Φ being inferred as λ q, mapsto l q v -- whereas we only want it to apply when q is the last argument?

Precisely.

mentioned in merge request !932 (merged)

What is the relation between this MR and !928 (merged)?

Is !928 (merged) supposed to subsume this MR?

!928 (merged) contains the (hopefully) non-controversial parts of this MR. The only thing missing there is fractional_as_fractional, where we still have to figure out whether we want that instance or not.

!928 (merged) should go first either way.

Indeed. Since !923 (merged) no longer has a motivating use for fractional_as_fractional, and there seems to be a compelling reason to not add that instance (namely, the HOU issues described above), !928 (merged) exists to divorce the good typeclasses changes from the instance.

I'm leaning towards not adding fractional_as_fractional now, based on the problem with HOU. It seems an annoying footgun to have to remember to declare your own AsFractional instance for your Fractional predicate whenever Coq isn't able to derive it (which is slightly unclear.) The alternative approach where Fractional becomes an alias described here sounds more compelling - there would be no ambiguity on the user side about whether or not to add an instance in that case.

We could trick this instance to only trigger when the predicate is a variable (or an application ?).

mentioned in merge request !923 (merged)

Since the author no longer sees a use in this MR (@ivanbakel writes "I'm leaning towards not adding fractional_as_fractional now"), I am closing it.

If someone wants to experiment with any of the proposals by @jjourdan in !928 (comment 92158) it makes most sense to open a new MR. (I would be interested if someone tries the third option, remove Fractional altogether, but won't have time to try it myself.)

closed