Skip to content
Snippets Groups Projects
Commit 5c1b38c5 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Ralf Jung
Browse files

Flip quantifiers for atomic updates, and double them up

parent bfb57e8b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/bi/lib/atomic.v
+ 12
− 12
View file @ 5c1b38c5
......@@ -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)
......
iris/program_logic/atomic.v
+ 6
− 6
View file @ 5c1b38c5
......@@ -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 '>>>'" :=
......
iris_heap_lang/lib/atomic_heap.v
+ 7
− 7
View file @ 5c1b38c5
......@@ -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) >>>.
......
iris_heap_lang/lib/increment.v
+ 4
− 4
View file @ 5c1b38c5
......@@ -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.
......
tests/atomic.ref
+ 35
− 35
View file @ 5c1b38c5
......@@ -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 }}
tests/atomic.v
+ 10
− 10
View file @ 5c1b38c5
......@@ -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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment