Skip to content

Flip atomic updates quantifiers compared to atomic triples

Paolo G. Giarrusso requested to merge Blaisorblade/iris:atomic-flip into master

Originally suggested by Gregory Malecha (a while ago), and recently discussed with @haidang.

Quantifiers in atomic triples make perfect sense, but AUs and AAUUs are more confusing when used directly: there, actually means , and viceversa.

In this proposal, <<< ∀ x, P x >>> e <<< ∃ y, Q x y, RET f x y >>> expands to ∀ Φ, AU << ∃ x, P x >> ... << ∀ y, Q x y COMM Φ (f x y) >> -* WP e {{ Φ }}; then the quantifiers in AUs match the definition and convey the right intuition.

One might fear this is inconsistent. But expanding triples moves quantifiers to the left of a wand, so flipping their polarity follows the tradition from (dependent) currying: (∀ x, P x -∗ Q) ⊣⊢ ((∃ x, P x) -∗ Q).

(Tested locally with dune and Coq 8.13.2).


FWIW, @swasey and @haidang also brought up arguments about caller/callee views, and about the TaDa logic. However, this MR preserves the notation for atomic triples (which agrees with TaDa), and TaDa rules seem to have similar quantifier flipping from a very superficial look (but no, I don't understand everything in flight). Finally, existentials are existentials both at introduction and elimination time; I think the only polarity flip is the one above — atomic triples use AUs in negative position.

image image

Edited by Paolo G. Giarrusso

Merge request reports