Skip to content
Snippets Groups Projects
Commit 5a3fc21a authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'atomic-flip' into 'master' 

Flip atomic updates quantifiers compared to atomic triples

See merge request iris/iris!750
parents bfb57e8b 08d1fac0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
CHANGELOG.md
+ 5
− 0
View file @ 5a3fc21a
......@@ -22,6 +22,11 @@ lemma.
* Change statement of `affinely_True_emp` to also remove the affinely modality.
* Rename `absorbingly_True_emp` to `absorbingly_emp_True` and make statement
consistent with `affinely_True_emp`: `<absorb> emp ⊣⊢ True`.
* Change the notation for atomic updates and atomic accessors (`AU`, `AACC`) to
swap the quantifiers: the first quantifier is logically an existential, the
second a universal, so let's use the appropriate notation. Also use double
quantifiers (`∀∀`, `∃∃`) to make it clear that these are not normal
quantifiers (the latter change was also applied to logically atomic triples).
**Changes in `proofmode`:**
......
iris/bi/lib/atomic.v
+ 12
− 12
View file @ 5a3fc21a
......@@ -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 @ 5a3fc21a
......@@ -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 @ 5a3fc21a
......@@ -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 @ 5a3fc21a
......@@ -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 @ 5a3fc21a
......@@ -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 @ 5a3fc21a
......@@ -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