From 5c1b38c5bb939f7cd2d2b5b72ef6fe1f2280ce6a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 9 Nov 2021 17:41:11 +0100
Subject: [PATCH] Flip quantifiers for atomic updates, and double them up

---
 iris/bi/lib/atomic.v             | 24 +++++------
 iris/program_logic/atomic.v      | 12 +++---
 iris_heap_lang/lib/atomic_heap.v | 14 +++----
 iris_heap_lang/lib/increment.v   |  8 ++--
 tests/atomic.ref                 | 70 ++++++++++++++++----------------
 tests/atomic.v                   | 20 ++++-----
 6 files changed, 74 insertions(+), 74 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 7b65aa8ef..5750a4609 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -99,7 +99,7 @@ Global Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
 (** Notation: Atomic updates *)
 (* The way to read the [tele_app foo] here is that they convert the n-ary
 function [foo] into a unary function taking a telescope as the argument. *)
-Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AU' '<<' ∃∃ x1 .. xn , α '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
                  (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                  Eo Ei
@@ -112,9 +112,9 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'C
                         ) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AU' '<<' ∃∃ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
                  (TB:=TeleO)
                  Eo Ei
@@ -123,9 +123,9 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
                  (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO)
                  (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                  Eo Ei
@@ -134,7 +134,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
                  (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO) (TB:=TeleO)
@@ -147,7 +147,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
    format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Notation: Atomic accessors *)
-Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' ∃∃ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -161,9 +161,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .
                      ) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' ∃∃ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleO)
               Eo Ei
@@ -173,9 +173,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'CO
               (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -185,7 +185,7 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'CO
               (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index cc01c234c..9a651a70b 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -25,7 +25,7 @@ Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
 
 (* The way to read the [tele_app foo] here is that they convert the n-ary
 function [foo] into a unary function taking a telescope as the argument. *)
-Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              e%E
@@ -39,10 +39,10 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v
                         ) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv' '<<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
-Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
              e%E
@@ -52,10 +52,10 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
              (tele_app $ λ x1, .. (λ xn, tele_app v%V) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
-   format "'[hv' '<<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              e%E
@@ -65,7 +65,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
              (tele_app $ tele_app (λ y1, .. (λ yn, v%V) .. ))
   )
   (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
-   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
 Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index cb216f66c..0bfa20012 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -29,9 +29,9 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   free_spec (l : loc) (v : val) :
     {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
   load_spec (l : loc) :
-    ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ∅ <<< mapsto l q v, RET v >>>;
+    ⊢ <<< ∀∀ (v : val) q, mapsto l q v >>> load #l @ ∅ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ∅
+    ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ∅
       <<< mapsto l (DfracOwn 1) w, RET #() >>>;
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
@@ -41,7 +41,7 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   [destruct (decide (a = b))] and it will simplify in both places. *)
   cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
+    ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
       <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
@@ -75,7 +75,7 @@ Section derived.
 
   Lemma cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ∅
+    ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ∅
     <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET #if decide (v = w1) then true else false >>>.
   Proof.
@@ -114,7 +114,7 @@ Section proof.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
-    ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
+    ⊢ <<< ∀∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
     <<< l ↦{q} v, RET v >>>.
   Proof.
     iIntros (Φ) "AU". wp_lam.
@@ -123,7 +123,7 @@ Section proof.
   Qed.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ∅
+    ⊢ <<< ∀∀ v, l ↦ v >>> primitive_store #l w @ ∅
     <<< l ↦ w, RET #() >>>.
   Proof.
     iIntros (Φ) "AU". wp_lam. wp_let.
@@ -133,7 +133,7 @@ Section proof.
 
   Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ (v : val), l ↦ v >>>
+    ⊢ <<< ∀∀ (v : val), l ↦ v >>>
       primitive_cmpxchg #l w1 w2 @ ∅
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET (v, #if decide (v = w1) then true else false) >>>.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 639fbf761..9084375be 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -21,7 +21,7 @@ Section increment_physical.
          else "incr" "l".
 
   Lemma incr_phy_spec (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
@@ -52,7 +52,7 @@ Section increment.
   (** A proof of the incr specification that unfolds the definition of atomic
       accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -91,7 +91,7 @@ Section increment.
       prove are in 1:1 correspondence; most logically atomic proofs will not be
       able to use them. *)
   Lemma incr_spec (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -125,7 +125,7 @@ Section increment.
      connective that works on [option Qp] (the type of 1-q). *)
   Lemma weak_incr_spec (l: loc) (v : Z) :
     l ↦{#1/2} #v -∗
-    <<< ∀ (v' : Z), l ↦{#1/2} #v' >>>
+    <<< ∀∀ (v' : Z), l ↦{#1/2} #v' >>>
       weak_incr #l @ ∅
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 8a1562b0f..de749e7a9 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -9,7 +9,7 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
+  AACC << ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
        @ ⊤ ∖ ∅, ∅
        << l ↦{q} v0, COMM Q -∗ Q >>
 "non_laterable"
@@ -24,7 +24,7 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
+  AACC << ∃∃ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
        @ ⊤ ∖ ∅, ∅
        << l ↦{q} v, COMM True >>
 1 goal
@@ -37,7 +37,7 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
+  AACC << ∃∃ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
        @ ⊤ ∖ ∅, ∅
        << l ↦{q} v, COMM True >>
 "printing"
@@ -48,7 +48,7 @@
   heapGS0 : heapGS Σ
   P : val → iProp Σ
   ============================
-  ⊢ <<< ∀ x : val, P x >>> code @ ∅ <<< ∃ y : val, P y, RET #() >>>
+  ⊢ <<< ∀∀ x : val, P x >>> code @ ∅ <<< ∃∃ y : val, P y, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -56,7 +56,7 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
+  "AU" : AU << ∃∃ x : val, P x >> @ ⊤, ∅ << ∀∀ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -66,12 +66,12 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∀ x : val, P x,
-              ABORT AU << ∀ x : val, P x >>
-                       @ ⊤ ∖ ∅, ∅
-                       << ∃ y : val, P y, COMM Φ #() >> >>
-           @ ⊤ ∖ ∅, ∅
-           << ∃ y : val, P y, COMM Φ #() >>
+  _ : AACC << ∃∃ x : val, P x,
+              ABORT AU << ∃∃ x : val, P x >>
+                       @ ⊤, ∅
+                       << ∀∀ y : val, P y, COMM Φ #() >> >>
+           @ ⊤, ∅
+           << ∀∀ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -80,7 +80,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>
+  ⊢ <<< ∀∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -88,7 +88,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
+  "AU" : AU << ∃∃ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -98,8 +98,8 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∀ x : val, l ↦ x,
-              ABORT AU << ∀ x : val, l ↦ x >>
+  _ : AACC << ∃∃ x : val, l ↦ x,
+              ABORT AU << ∃∃ x : val, l ↦ x >>
                        @ ⊤ ∖ ∅, ∅
                        << l ↦ x, COMM Φ #() >> >>
            @ ⊤ ∖ ∅, ∅
@@ -112,7 +112,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -120,7 +120,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << ∀∀ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -133,9 +133,9 @@
   _ : AACC << l ↦ #(),
               ABORT AU << l ↦ #() >>
                        @ ⊤ ∖ ∅, ∅
-                       << ∃ y : val, l ↦ y, COMM Φ #() >> >>
+                       << ∀∀ y : val, l ↦ y, COMM Φ #() >> >>
            @ ⊤ ∖ ∅, ∅
-           << ∃ y : val, l ↦ y, COMM Φ #() >>
+           << ∀∀ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -176,7 +176,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -186,7 +186,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >>
+  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x >>
             @ ⊤ ∖ ∅, ∅
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
@@ -197,9 +197,9 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< ∃ y : val, l ↦ y, RET #() >>>
+    <<< ∃∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -207,9 +207,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
             @ ⊤ ∖ ∅, ∅
-            << ∃ y : val, l ↦ y, COMM Φ #() >>
+            << ∀∀ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -218,9 +218,9 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<< ∀∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
-    <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+    <<< ∃∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
 1 goal
   
@@ -229,9 +229,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+  _ : AU << ∃∃ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
          @ ⊤ ∖ ∅, ∅
-         << ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+         << ∀∀ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
             l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -241,7 +241,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< l ↦ x, RET #() >>>
 1 goal
@@ -251,7 +251,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
             @ ⊤ ∖ ∅, ∅
             << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
@@ -265,7 +265,7 @@
   ============================
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< ∃ y : val, l ↦ y, RET #() >>>
+    <<< ∃∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -276,7 +276,7 @@
   ============================
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
             @ ⊤ ∖ ∅, ∅
-            << ∃ y : val, l ↦ y, COMM Φ #() >>
+            << ∀∀ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -361,9 +361,9 @@
   ============================
   "AU" : ∃ x : val, P x ∗
            (P x ={∅,⊤}=∗
-            AU << ∀ x0 : val, P x0 >>
+            AU << ∃∃ x0 : val, P x0 >>
                @ ⊤ ∖ ∅, ∅
-               << ∃ y : val, P y, COMM Φ #() >>)
+               << ∀∀ y : val, P y, COMM Φ #() >>)
            ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
diff --git a/tests/atomic.v b/tests/atomic.v
index 114ccd8cc..20b83453a 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -53,21 +53,21 @@ Section printing.
   Definition code : expr := #().
 
   Lemma print_both_quant (P : val → iProp Σ) :
-    ⊢ <<< ∀ x, P x >>> code @ ∅ <<< ∃ y, P y, RET #() >>>.
+    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y, RET #() >>>.
   Proof.
-    Show. iIntros (Φ) "AU". Show.
+    Show. iIntros (Φ) "AU". rewrite difference_empty_L. Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_first_quant l :
-    ⊢ <<< ∀ x, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_second_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
@@ -83,31 +83,31 @@ Section printing.
   Check "Now come the long pre/post tests".
 
   Lemma print_both_quant_long l :
-    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpre l :
-    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpost l :
-    ⊢ <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+    ⊢ <<< ∀∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< ∃∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "?". Show.
   Abort.
 
   Lemma print_first_quant_long l :
-    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_second_quant_long l x :
-    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
@@ -133,7 +133,7 @@ Section printing.
   Check "Prettification".
 
   Lemma iMod_prettify (P : val → iProp Σ) :
-    ⊢ <<< ∀ x, P x >>> !#0 @ ∅ <<< ∃ y, P y, RET #() >>>.
+    ⊢ <<< ∀∀ x, P x >>> !#0 @ ∅ <<< ∃∃ y, P y, RET #() >>>.
   Proof.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.
-- 
GitLab