don't make frame_fractional an instance

Instead, just add a concrete instance for ↦. This prevents TC search from trying AsFractional framing everywhere.

Let us see how much performance removing that instance brings, and how much convenience it costs. On Iris itself, this speeds up heap_lang.lib by 0.8%. iris/examples results can be found here.

Fixes #351 (closed)

changed the description

I suspect I'm because this is too clever and not always what you want, but it might be worth advertising this instance in proof_mode.md since it's so useful when you do want it, and the comment you added does not make it discoverable enough.

examples results are in: 0.9% speedup overall; 3.2% in theories/logatom/elimination_stack. So I think this confirms the "performance" hypothesis.

On the other hand, this also confirms the "convenience" hypothesis -- RDCSS and conditional_increment required some porting. I suspect I might want to enable the instance for those files, if we decide to land this MR. That will reduce the perf benefit, of course.

On the other hand, this also confirms the "convenience" hypothesis -- RDCSS and conditional_increment required some porting. I suspect I might want to enable the instance for those files, if we decide to land this MR. That will reduce the perf benefit, of course.

Maybe we can do the following: when framing you can give a level: 0 (default) means to not do fancy stuff, and higher means to do more fancy stuff like the fractional framing or disjunctions.

We of course need proper syntax for iFrame and the various framing options in intro/spec patterns.

Aside from settling on syntax, I think what I suggested is trivial to implement.

Yeah that sounds good! Implementation-wise I think I am only concerned about how you want to disable the "fancy" rules for low levels. I assume it will be something like adding 2 ≤ level as the first assumption -- but won't that mean many attempts to prove these trivial inequalities, and even having the result embedded in the proof term in case the rule is actually applied?

In terms of syntax, a few strawman proposals:

(* similar to eauto *)
iFrame 10.
iFrame 10 "pat".
(* or an explicit keyword *)
iFrame level 10.
iFrame "pat" level 10.
(* or another explicit keyword *)
iFrame at 10.
iFrame "pat" at 10.

I am a bit worried the 2nd option might make level impossible as a variable name though.

For frame patterns, iDestruct (foo with "[$10]") as "[Hbar $5]" seems like the obvious choice.

mentioned in merge request !742 (closed)

Something came to my mind:

The reason why fractional framing is so slow, is probably because the Frame instance does not have any constraints on the shape of the goal. The instance can pretty much be applied in every node of the proof search, only the search for AsFractional will fail later.

Wouldn't it be an idea to disable fractional framing by default, but manually add instances for things like ↦?

That would probably help, yeah -- though we should benchmark it. Ideally we'd have some kind of macro 'add fractional framing for this iProp pattern', but Coq doesn't have a suitable macro language for this...

mentioned in merge request !737 (merged)

added 78 commits

• 998b8484...255341dd - 77 commits from branch master
• 5bae01cc - perf experiment: dont make frame_fractional an instance

Compare with previous version

added 1 commit

• 30208bd5 - add back explicit framing instance for ↦

Compare with previous version

marked this merge request as ready

changed the description

mentioned in issue #442

resolved all threads

added 43 commits

• 30208bd5...f85824ee - 40 commits from branch master
• ea51b43b - perf experiment: dont make frame_fractional an instance
• fd49bcbe - add back explicit framing instance for ↦
• d38ec11e - changelog

Compare with previous version

enabled an automatic merge when the pipeline for d38ec11e succeeds

@iris-users this could break uses of iFrame

• Make frame_fractional not an instance any more; instead fractional propositions that want to support framing are expected to register an appropriate instance themselves. HeapLang and gen_heap ↦ still support framing, but the other fractional propositions in Iris do not.

If you are defining your own fractional connective and need framing support, you can declare an instance like this:

  Global Instance frame_mapsto p l v q1 q2 RES :
    FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
    Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
  Proof. apply: frame_fractional. Qed.

merged

mentioned in commit 901016fc