Draft: Add simplification machinery for ✓ and ≼.

This merge request partially addresses issue #251 .

Concretely, this merge request adds an iCombineOwn tactic. In the following environment:

"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)

executing iCombineOwn "Hγ1 Hγ2" as "Hγ" gives %[Hq HE] should replace "Hγ1" and "Hγ2" with a new hypothesis "Hγ" : own γ (q1 + q2, GSet (E1 ∪ E2)) and two pure hypotheses: Hq : q1 + q2 ≤ 1 and HE : E1 ## E2.

The "as" clause is optional. This is especially useful when you want to combine validity information for a ● and a ◯. In the following environment:

"Hγ1" : own γ (◯ (Some (q1, GSet E1)))
"Hγ2" : own γ (● (Some (q2, GSet E2)))

executing iCombineOwn "Hγ1 Hγ2" gives %H should give you a new pure hypotheses H : q1 ≤ q2 ∧ E1 ⊆ E2 ∧ ((q1 < q2) ∨ (q1 ≡ q2 ∧ E1 ≡ E2)).

It works by adding three typeclasses, IsValidOp, IsValidGives and IsIncluded, which try to determine an iProp that simplifies ✓ or ≼. Since we are looking for an iProp, not a pure proposition, this approach also works for higher-order ghost state.

Some current issues:

• Does not simplify equivalences. If directly using rewrites in introduction patterns, may cause slowdowns. Currently an explicit %leibniz_equiv on the equality is needed for faster rewrites.
• Some lemmas I used on validity and equivalence of views are still lying around in an awkward place.
• Documentation is missing
• Does not yet have instances for all CMRA building blocks provided in iris/algebra, but at least supports the ones used inside the iris repository, and some others I have used in the past.

Feedback is most welcome! I wasn't really sure where to place some of this stuff, so it currently resides in iris/base_logic/.

added 1 commit

• 35684b41 - Fix some lazy use of auto-naming.

Compare with previous version

added 1 commit

• f6a14a2b - Fix more problems caused by auto-naming.

Compare with previous version

added 1 commit

• a039c632 - Even more problems from auto-naming, that my local 8.14.1 does not have?.

Compare with previous version

added 1 commit

• 49e1b1a5 - Added instances to better handle dfrac_agree, more auto-naming fixes.

Compare with previous version

added 1 commit

• ee20565e - Fixing mono_nat problems from auto-naming.

Compare with previous version

mentioned in merge request !759 (merged)

Maybe prod_included_merge must be applied via an Hint Extern ... => apply: prod_included_merge : typeclass_instances. instead of being an instance?

Yes, that would work. The current approach is I think easier for debugging the output of Set Typeclasses Debug.

I'm not sure what is best here

changed this line in version 7 of the diff

Usually the 'classes' file should only contain the classes, so this seems more like material for the 'instances' file. I would also suggest naming them more specifically to be about the combine-own infrastructure. And finally they should probably be in the 'lib' subfolder since these are all derived construction, not base logic primitives (and since base_logic should never import from base_logic.lib, only the other way around).

changed this line in version 7 of the diff

All these classes should come with brief documentation explaining what they mean and do.

Also given that this is the main tactic driving the iCombineOwn tactic, I wonder if it shouldn't be called something that reflects that.

changed this line in version 7 of the diff

This sounds really cool, thanks a lot. :) Unfortunately I am quite swamped currently and this is a lot of TC magic to review -- I sure hope we can get @robbertkrebbers to help here since I would not trust my judgment when it comes to designing TCs for automation. ;)

I think I have one high-level concern about the UI here: the fact that iCombineOwn returns vastly different things depending on the input does not seem great. Sometimes it returns a conjunction of own and validity information, sometimes it just returns the validity (in particular for auth-frag combination, where we do not have a nice way to write the composite form). I don't think this should be the same tactic, so I wonder if it makes sense to have two tactics?

• iCombine can be used to do the fancy combining and simplification of ownership (it might even already do that to some extend?)
• iValid "H" as "Hval" (name up for bikeshedding) exploits validity of H: own \gamma a. Hval is always persistent so we can offer the sugar iValid "H1 H2" as "Hval" which first iCombines H1 H2 and then exploits validity, but leaves the context unchanged.

I guess the one thing this does not handle well is fractions/agreement, where we might want to put two owns together but also learn about the equality. So maybe this is not a good idea after all, but I do think we want something more predictable than what you describe. Maybe iCombineOwn "H1 H2" as "Hown" with "Hvalid" and then we have syntactic variants without the Hown which always preserve the original owns? The underlying primitive IsValidOp, if I understand correctly, already has this structure (always producing a 'normalized' combined RA element plus a validity proposition), we just have to figure out how to best expose this -- I think the user should make the choice of whether the owns are combined to one or not, not the tactic. This would also let us have a variant like iCombineOwn "H1 H2" as "Hown" with %Hvalid where one can directly use all Coq intro patterns.

Thanks for taking a look!

I agree with you on the UI part - the users should choose whether to combine the owns or just get validity info. I like your idea of iCombineOwn "H1 H2" as "Hown" with "Hvalid" with optional as "Hown", that should be easy to implement given the current the definition of IsValidOp. This could then also be used to for combining an auth part with a frag part: one would then just do iCombineOwn "H● H◯" with "Hvalid". I have an idea on how to make this work in a way that would also support, for example, the compatibility conditions of gmap_view.

I'll try to tackle this and the other comments somewhere soon. I'm also meeting with @robbertkrebbers next Monday, to see how to best proceed with this MR.

Edit: maybe iCombineOwn "H1 H2" as "Hown" gives "Hvalid" is more intuitive, especially when you leave out as "Hown"

added 1 commit

• 7ef30690 - iCombineOwn now takes as and gives arguments, makes behaviour more predictable for the user.

Compare with previous version

changed the description

@robbertkrebbers and me talked about this MR today. One of the things which is currently missing is a way to combine abstracted versions of own, like ↦, ghost_var, ghost_map, and other things from base_logic.lib.

The current typeclass setup works with explicit cmra elements, so supporting this would require a layer of abstraction above the current IsValidOp class. This would be something like CombineSep P1 P2 P R := P1 ∗ P2 ⊢ P ∗ □R. Then things from base_logic.lib could give their own instances, and instances for explicit owns could be derived from IsValidOp instances. The tactic should then no longer be called iCombineOwn, maybe iCombineSimpl.

So why not go further and replace iCombine with iCombineSimpl? Well, me and @robbertkrebbers seemed to agree that we do not want to combine things that do not simplify, like owned ● and ◯ elements. This means in particular that we cannot have an instance CombineSep P1 P2 (P1 ∗ P2) True, so this would break existing uses of iCombine. On the other hand, most (all?) uses of iCombine that we found will be obsolete once we have this improved combination tactic. So that might be okay.

There are thus two ways to proceed:

• Replace iCombine with a generalized version of what this MR proposes. This could be chopped up into 3 merge requests:

  1. Change FromSep to only be used for iSplit{L,R}, change iCombine to rely on new typeclass CombineSep
  2. Add optional "gives" argument to iCombine, "as" is still required.
     • Add intuitionistic conclusion to CombineSep (definition as above)
     • Give instances for base_logic.lib, mapsto
  3. Give general instance for own (= current MR), make "as" argument optional
     • Add typeclass like CombineSepGives P1 P2 R := P1 ∗ P2 ⊢ □ R
     • Remove ability to combine hypotheses that do not simplify
     • New classes for merging camera elements, and instances of those classes for all cameras

  We could ofcourse choose to keep a (dumbed-down) version of iCombine as iCombineDumb.

• Have a separate iCombineSimpl tactic, which generalizes what this MR proposes.

  1. Add CombineSep(Gives) class as above, give instances for base_logic.lib, mapsto
  2. Make this MR produce instances of CombineSep(Gives)

Let me know what you think!

One of the things which is currently missing is a way to combine abstracted versions of own, like ↦, ghost_var, ghost_map, and other things from base_logic.lib.

I am not convinced that we really want this. The way I view it, this is entirely an RA feature. It is primarily motivated because RAs are typically used in a nested way, so to reason about composition, validity, and updates one has to go through all these nested layers, as each lemma only handles a single layer. Experience shows this can be quite tricky even for people that have ample Iris experience and intuition (and in particular when it comes to auth an agreement, I sometimes struggle with this myself).

The same motivation simply does not arise for logical abstractions, since those cannot be nested. IOW, ghost_map already provides (or should provide) all the lemmas one might need, making it easy enough to use.

So, I think we should focus on the main use case of making RAs easier to work with in Iris, and not unnecessarily expand this feature by also covering logic-level RA wrappers.

Note that the current tactic is hardcoded to Iris's own. This means that it cannot be used for other logics like gpfsl or Iron since they don't use the own connective directly, but use it under an embedding and modality (possibly in some abstracted form).

To support that, I think you need to have something like CombineSep P1 P2 P R := P1 ∗ P2 ⊢ P ∗ □ R, that Ike noticed in the message above. Then you can also have instances that go below modalities and embeddings, so as to support own logics like Iron and gpfsl.

As a coincidental side-effect, once you have something like this CombineSep class, the instances for ↦ and friends are actually entirely trivial (there's no recursive search).

First of all, none of this responds to my main argument that IMO we do not want a complicated swiss army knife typeclass and tactic, but something targeted and precise for reasoning about RAs. I think we should design this from the perspective of the UI (for tactic users and people writing TC instances), not some incidental implementation details.

Secondly:

To support that, I think you need to have something like CombineSep P1 P2 P R := P1 ∗ P2 ⊢ P ∗ □ R, that Ike noticed in the message above

I don't think so. Rather, we need a way to have own and valid in any PROP -- something that already came up in earlier discussions, so this is something we would probably want anyway.

Given that, the automation typeclass and tactic can be stated logic-independently while still targeting RAs, not logic-level abstractions.

How should we best proceed here? I can personally see the value in being able to use the same tactic for ↦ and other logical abstractions - one no longer needs to remember/lookup the correct lemma names. But it also adds more complexity to the current MR.

Whatever the preferred approach turns out to be (add a CombineSep abstraction layer/have own and valid work in any PROP), I think the current proposed changes will be useful and will not require much changes for adapting to the preferred approach. The CombineSep approach would require two new instances and a change to the tactic. For the other approach one needs to change the definition of IsValidOp and friends to be parametrized by the thing which makes valid work in a given PROP. All the instances should stay the same.

@robbertkrebbers @snyke7 Let's plan to talk about this at the Iris Workshop hackathon?

+1

As per our discussion today, this is blocked on first landing an MR that generalizes iCombine to also provide some "observed" persistent facts. Once that exists we can wire in this machinery to make clever observations.

added S-blocked label

mentioned in issue #460

!872 (merged) has landed. :) What are the plans for this MR? Is there still value in keeping this MR open? I assume the next step will be a new MR anyway, so the only question is whether there's discussion above that needs to be preserved.

The plans are to implement the proposals from this MR using the new machinery from !872 (merged). I think the majority of the code from this MR can be reused to fit on top of !872 (merged).

Issue #460 also describes the plan, and contains the conclusions of the discussion above. I'd be fine with closing this MR, and opening a new one when I get to rebasing, or keeping it open until then.

I think the discussions above are all resolved by the design laid out in !872 (merged), so it seems better to start a new MR. Hence I am closing this one.

closed

mentioned in merge request !930 (closed)