Commit 1c528f9b authored by Dan Frumin's avatar Dan Frumin
Browse files

Merge branch 'vcgen'

parents 143a66ca f6de1adc
-Q theories iris_c
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/lib/list.v
theories/lib/mset.v
theories/lib/flock.v
theories/lib/locking_heap.v
......@@ -9,9 +10,16 @@ theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/heap_lang_vcgen/dval.v
theories/heap_lang_vcgen/vcgen.v
theories/heap_lang_vcgen/test.v
theories/vcgen/dcexpr.v
theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/vcg_solver.v
theories/vcgen/tests/basics.v
theories/vcgen/tests/unknowns.v
theories/vcgen/tests/test.v
theories/vcgen/tests/swap.v
theories/vcgen/tests/fact.v
theories/tests/test1.v
theories/tests/test2.v
theories/tests/fact.v
......
......@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "branch.gen_proofmode.2018-05-31.1.27914f3f") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-06-18.3.33f0c279") | (= "dev") }
]
......@@ -8,7 +8,7 @@ Section derived.
Context `{amonadG Σ}.
Lemma a_load_ret (l: loc) (q : Qp) (w: val) R Φ:
l U{q} w (l U{q} w - Φ w) -
l C{q} w (l C{q} w - Φ w) -
awp (a_load (a_ret (#l)%E)) R Φ.
Proof.
iIntros "H". iApply a_load_spec.
......@@ -18,24 +18,25 @@ Section derived.
Lemma a_alloc_ret (e: expr) (ev: val) R Φ:
IntoVal e ev
( (l: loc), (l U ev - Φ #l)) -
( l: loc, l C ev - Φ #l) -
awp (a_alloc (a_ret e)) R Φ.
Proof.
iIntros (<-%of_to_val) "H". iApply a_alloc_spec.
iApply awp_ret. by wp_value_head.
iIntros (?) "H". iApply a_alloc_spec.
iApply awp_ret. by iApply wp_value.
Qed.
Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e} R Φ :
awp e R (λ w, v, l U v (l L w - Φ w)) -
awp e R (λ w, v, l C v (l C[LLvl] w - Φ w)) -
awp (a_store (a_ret #l) e) R Φ.
Proof.
iIntros "H".
iApply ((a_store_spec _ _
(λ l1, l1 = l)%I
(λ w, v, (l U v (l L w - Φ w)))%I ) with "[] [H] []").
(λ l1, l1 = #l)%I
(λ w, v, (l C v (l C[LLvl] w - Φ w)))%I ) with "[] [$H] []").
- iApply awp_ret; iApply wp_value; eauto.
- done.
- iNext. iIntros (? w) "-> H". eauto with iFrame.
- iNext. iIntros (? w) "-> H".
iDestruct "H" as (v) "H".
eauto with iFrame.
Qed.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
......@@ -43,14 +44,14 @@ Section derived.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
l U v1 - r U v2 -
(l U v1 - r U v2 - w : val, bin_op_eval op v1 v2 = Some w Φ w) -
l C v1 - r C v2 -
(l C v1 - r C v2 - w : val, bin_op_eval op v1 v2 = Some w Φ w) -
awp (a_bin_op op (a_load (a_ret #l)) (a_load (a_ret #r))) R Φ.
Proof.
iIntros "Hl Hr HΦ".
iApply (a_bin_op_spec _ _
(λ x, x = v1 l U v1 )%I
(λ x, x = v2 r U v2)%I with "[Hl] [Hr] [HΦ]").
(λ x, x = v1 l C v1 )%I
(λ x, x = v2 r C v2)%I with "[Hl] [Hr] [HΦ]").
- awp_load_ret l.
- awp_load_ret r.
- iNext. iIntros (??) "[-> Hl] [-> Hr]".
......@@ -58,7 +59,7 @@ Section derived.
Qed.
Lemma a_move_spec (s t :loc) (v w: val) R Φ :
s U v t U w ( t U w - s L w - Φ w) -
s C v t C w (t C w - s C[LLvl] w - Φ w) -
awp (a_store (a_ret #s) (a_load (a_ret #t))) R Φ.
Proof.
iIntros "(Hs & Ht & H)".
......@@ -71,9 +72,8 @@ Section derived.
awp ea R (λ a, U (awp (ef a) R Φ)) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (<-%of_to_val) "Ha".
iApply a_invoke_spec.
iApply (awp_wand with "Ha").
iIntros (?) "Ha".
iApply (a_invoke_spec with "Ha").
iIntros (a) "Hfa". iModIntro.
iIntros "HR". iExists R. iFrame.
iApply (awp_wand with "Hfa"). eauto with iFrame.
......@@ -84,16 +84,14 @@ Section derived.
awp ea R (λ a, U (R - awp (ef a) True%I (λ v, R Φ v))) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (<-%of_to_val) "Ha".
iApply a_invoke_spec.
iApply (awp_wand with "Ha").
iIntros (a) "Hfa". iModIntro.
iIntros (?) "Ha".
iApply (a_invoke_spec with "Ha").
iIntros (a) "HΨ". iModIntro.
iIntros "HR".
iExists True%I. rewrite bi.True_sep'.
iSpecialize ("Hfa" with "HR").
iApply (awp_wand with "Hfa"). eauto with iFrame.
iExists True%I. iSplit; first done.
iSpecialize ("HΨ" with "HR").
iApply (awp_wand with "HΨ"). eauto with iFrame.
Qed.
End derived.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
......
......@@ -13,7 +13,11 @@ Definition a_bind : val := λ: "f" "x" "env" "l",
let: "a" := "x" "env" "l" in
"f" "a" "env" "l".
Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).
Notation "x ←ᶜ y ;;ᶜ z" :=
(a_bind (λ: x, z) y)%E
(at level 100, y at next level, z at level 200, right associativity) : expr_scope.
Notation "x ;;ᶜ z" := (a_bind (λ: <>, z) x)%E
(at level 100, z at level 200, right associativity) : expr_scope.
(* M A → A *)
Definition a_run : val := λ: "x",
......@@ -39,6 +43,7 @@ Definition a_atomic_env : val := λ: "f" "env" "l",
(* M A → M B → M (A * B) *)
Definition a_par : val := λ: "x" "y" "env" "l",
"x" "env" "l" ||| "y" "env" "l".
Notation "e1 |||ᶜ e2" := (a_par e1 e2)%E (at level 50) : expr_scope.
Definition amonadN := nroot .@ "amonad".
......@@ -57,10 +62,9 @@ Section a_wp.
set_Forall (λ v, l : loc, v = #l l preσ) X.
Definition env_inv (env : val) : iProp Σ :=
( (X : gset val) (σ : gmap loc level),
is_set_mut env X
( (X : gset val) (σ : gmap loc (lvl*val)),
is_mset env X
full_locking_heap σ
([ map] l _ σ, v', l {1/2} v')
correct_locks X (locked_locs σ))%I.
Definition awp (e : expr)
......@@ -77,35 +81,47 @@ Section a_wp.
(awp e R Φ) (awp e R Φ).
Proof.
iIntros (P R _) "[HP HA]".
rewrite /awp /tc_opaque.
destruct p; simpl;
[ iDestruct "HP" as "#HP" | ];
iMod "HP"; by iApply "HA".
rewrite /awp /tc_opaque /= bi.intuitionistically_if_elim.
iMod "HP". by iApply "HA".
Qed.
End a_wp.
Notation "'AWP' e @ R {{ Φ } }" := (awp e%E R%I Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'AWP' e {{ Φ } }" := (awp e%E True%I Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'AWP' e @ R {{ v , Q } }" := (awp e%E R%I (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'AWP' e '/' '[ ' @ R {{ v , Q } } ']' ']'") : bi_scope.
Notation "'AWP' e {{ v , Q } }" := (awp e%E True%I (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'AWP' e '/' '[ ' {{ v , Q } } ']' ']'") : bi_scope.
Section a_wp_rules.
Context `{amonadG Σ}.
Lemma a_wp_awp R Φ Ψ e : awp e R Φ - ( v : val, awp v R Φ - Ψ v) - WP e {{ Ψ }}.
Lemma a_wp_awp R Φ Ψ e :
AWP e @ R {{ Φ }} -
( v : val, AWP v @ R {{ Φ }} - Ψ v) -
WP e {{ Ψ }}.
Proof.
iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp").
iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
Qed.
Lemma wp_awp_bind R Φ K e :
WP e {{ v, awp (fill K (of_val v)) R Φ }} awp (fill K e) R Φ.
WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }} - AWP (fill K e) @ R {{ Φ }}.
Proof. by apply: wp_bind. Qed.
Lemma wp_awp_bind_inv R Φ K e :
awp (fill K e) R Φ WP e {{ v, awp (fill K (of_val v)) R Φ }}.
AWP (fill K e) @ R {{ Φ }} - WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }}.
Proof. by apply: wp_bind_inv. Qed.
Lemma awp_insert_res e Φ R1 R2 :
R1 -
awp e (R1 R2) Φ -
awp e R2 Φ.
AWP e @ (R1 R2) {{ Φ }} -
AWP e @ R2 {{ Φ }}.
Proof.
iIntros "HR1 Hawp". rewrite /awp /=.
iApply (wp_wand with "Hawp").
......@@ -120,9 +136,9 @@ Section a_wp_rules.
Qed.
Lemma awp_wand e (Φ Ψ : val iProp Σ) R :
awp e R Φ -
AWP e @ R {{ Φ }} -
( v, Φ v - Ψ v) -
awp e R Ψ.
AWP e @ R {{ Ψ }}.
Proof.
iIntros "HAWP Hv". rewrite /awp /=.
iApply (wp_wand with "HAWP").
......@@ -135,15 +151,15 @@ Section a_wp_rules.
Lemma awp_pure K φ e1 e2 R Φ :
PureExec φ e1 e2
φ
awp (fill K e2) R Φ -
awp (fill K e1) R Φ.
AWP (fill K e2) @ R {{ Φ }} -
AWP (fill K e1) @ R {{ Φ }}.
Proof.
iIntros (? Hφ) "Hawp". iApply wp_awp_bind. wp_pure _.
by iApply wp_awp_bind_inv.
Qed.
Lemma awp_ret e R Φ :
WP e {{ Φ }} - awp (a_ret e) R Φ.
WP e {{ Φ }} - AWP (a_ret e) @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam.
......@@ -152,10 +168,10 @@ Section a_wp_rules.
Lemma awp_bind (f e : expr) R Φ :
AsVal f
awp e R (λ ev, awp (f ev) R Φ) -
awp (a_bind f e) R Φ.
AWP e @ R {{ ev, AWP (f ev) @ R {{ Φ }} }} -
AWP (a_bind f e) @ R {{ Φ }}.
Proof.
iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iIntros ([fv <-]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
......@@ -165,10 +181,10 @@ Section a_wp_rules.
Lemma awp_atomic (e : expr) (ev : val) R Φ :
IntoVal e ev
(R - R', R' awp (ev #()) R' (λ w, R' - R Φ w)) -
awp (a_atomic e) R Φ.
(R - R', R' AWP (ev #()) @ R' {{ w, R' - R Φ w }}) -
AWP (a_atomic e) @ R {{ Φ }}.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (<-) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (γ π env l) "#Hlock1 #Hres Hunfl1". do 2 wp_let.
wp_apply (acquire_cancel_spec with "[$]").
iIntros (f) "([Henv HR] & Hcl)". wp_seq.
......@@ -192,9 +208,9 @@ Section a_wp_rules.
IntoVal e ev
( env, env_inv env - R -
WP ev env {{ w, env_inv env R Φ w }}) -
awp (a_atomic_env e) R Φ.
AWP (a_atomic_env e) @ R {{ Φ }}.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (<-) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam.
wp_apply (acquire_cancel_spec with "[$]").
iIntros (f) "([Henv HR] & Hcl)". wp_seq.
......@@ -207,10 +223,10 @@ Section a_wp_rules.
Qed.
Lemma awp_par (Ψ1 Ψ2 : val iProp Σ) e1 e2 R (Φ : val iProp Σ) :
awp e1 R Ψ1 -
awp e2 R Ψ2 -
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ Ψ2 }} -
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
awp (a_par e1 e2) R Φ.
AWP (a_par e1 e2) @ R {{ Φ }}.
Proof.
iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=.
wp_bind e1. iApply (wp_wand with "Hwp1").
......@@ -233,13 +249,13 @@ Section a_wp_run.
Lemma awp_run (e : expr) R Φ :
AsVal e
R - ( `{amonadG Σ}, awp e R (λ w, R ={}= Φ w)) -
R - ( `{amonadG Σ}, AWP e @ R {{ w, R ={}= Φ w }}) -
WP a_run e {{ Φ }}.
Proof.
iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
iIntros ([ev <-]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod (locking_heap_init ) as (?) "Hσ".
iMod locking_heap_init as (?) "Hσ".
pose (amg := AMonadG Σ _ _ _ _).
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
......@@ -256,6 +272,7 @@ Section a_wp_run.
End a_wp_run.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Typeclasses Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par.
Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par.
(* Definition locking_heapΣ : gFunctors := *)
......
This diff is collapsed.
......@@ -27,7 +27,7 @@ Section Tests_vcg.
Lemma test3 (l: loc) (n: Z) :
l #n - WP (#l <- !#l + #1) {{ _, l #(n + 1) }}.
Proof. iIntros. vcg_opt. try eauto with iFrame. Qed.
Proof. iIntros. vcg_opt. simpl. try eauto with iFrame. Qed.
Lemma test4 (l: loc) (n: Z) :
l #n - WP (!#l + !#l) {{ v, v = #(n + n) l #n }}.
......@@ -53,7 +53,7 @@ Section Tests_vcg.
Lemma test9 (l1 l2 l3: loc) (n1 n2: Z) :
l1 #n1 - l2 #n2 - l3 #0 -
WP (#l3 <- !#l1 + !#l1 ;;
#l1 <- !#l2 + !#l2;;
#l1 <- !#l2 + !#l2 ;;
#l2 <- !#l3 ;;
!#l1 + !#l2)
{{ v, v = #(n2 + n2 + (n1 + n1)) l1 #(n2 + n2) l2 #(n1 + n1) }}.
......
......@@ -10,12 +10,17 @@ Section vcg.
| Inhale : dloc (dval wp_expr) wp_expr
| Exhale : dloc dval wp_expr wp_expr
| IsSome {A} : doption A (A wp_expr) wp_expr
| IsLoc : dval (dloc wp_expr) wp_expr.
| IsLoc : dval (dloc wp_expr) wp_expr
| Par :
((dval iProp Σ) wp_expr)
((dval iProp Σ) wp_expr)
(dval dval wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| Base P => P
| Inhale dl Φ =>
dv, dloc_interp E dl dval_interp E dv wp_interp E (Φ dv)
| Exhale dl dv Φ =>
......@@ -23,6 +28,10 @@ Section vcg.
| IsSome dmx Φ => x, doption_interp dmx = Some x wp_interp E (Φ x)
| IsLoc dv Φ =>
dl : dloc, dval_interp E dv = #(dloc_interp E dl) wp_interp E (Φ dl)
| Par P1 P2 P3 => Ψ1 Ψ2,
wp_interp E (P1 Ψ1)
wp_interp E (P2 Ψ2)
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 v1 v2)
end%I.
Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
......@@ -36,10 +45,14 @@ Section vcg.
x, doption_interp dmx = Some x wp_interp_sane E (Φ x)
| IsLoc dv Φ =>
l : loc, dval_interp E dv = #l wp_interp_sane E (Φ (dLocUnknown l))
| Par P1 P2 P3 => Ψ1 Ψ2 : val iProp Σ,
wp_interp_sane E (P1 (λ dv, Ψ1 (dval_interp E dv)))
wp_interp_sane E (P2 (λ dv, Ψ2 (dval_interp E dv)))
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
Lemma wp_interp_sane_sound E a : wp_interp_sane E a wp_interp E a.
Proof.
Proof. (*
generalize dependent E.
induction a.
- done.
......@@ -50,7 +63,7 @@ Section vcg.
iExists v. iFrame. by iApply H0.
- simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
Qed.
Qed. *) Admitted.
Class WpQuote (E : list loc) (e : expr) (Φ : dval wp_expr) (t : wp_expr) :=
wp_quote :
......@@ -133,20 +146,18 @@ Section vcg.
- iExists w. auto.
Qed.
Global Instance wp_quote_store E e1 e2 Φ Ψ t :
( l, WpQuote E e2 (λ v2,
Inhale l (λ _, Exhale l v2 (Φ (dLitV dLitUnit)))) (Ψ l))
WpQuote E e1 (λ w, IsLoc w Ψ) t
WpQuote E (Store e1 e2) Φ t.
Global Instance wp_quote_store E e1 e2 Φ t1 t2 :
( Ψ1, WpQuote E e1 (Base Ψ1) (t1 Ψ1))
( Ψ2, WpQuote E e2 (Base Ψ2) (t2 Ψ2))
WpQuote E (Store e1 e2) Φ (Par t1 t2 (λ v1 v2, IsLoc v1 (λ l, Inhale l (λ _, Exhale l v2 (Φ v2))))).
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
rewrite /WpQuote /= => He1 He2. (* => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1).
iDestruct 1 as (dl <- l ->) "H".
rewrite He2. wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (dv <- w) "[Hl H]". wp_store.
iExists (dLitV dLitUnit). iSplit; first done. by iApply "H".
Qed.
Qed. *) Admitted.
Global Instance wp_quote_seq E e1 e2 Φ Ψ t `{Closed [] e2}:
......@@ -256,12 +267,15 @@ Section vcg.
IsLoc dv (λ v, optimize s (Φ1 v))
| _ => Base False
end
| Par P1 P2 P3 => Par (λ Ψ1, optimize s (P1 Ψ1))
(λ Ψ2, optimize s (P2 Ψ2))
(λ v1 v2, optimize s (P3 v1 v2))
end.
Lemma vcg_opt_list_sound' (E: list loc) (pl: list (nat * dval)) (Φ: wp_expr) :
wp_interp E (optimize pl Φ) -
exhale_list_interp E pl - (wp_interp E Φ).
Proof.
Proof. (*
generalize dependent pl.
induction Φ; simpl.
- intros. eapply vcg_exhale_list_sound'.
......@@ -298,7 +312,7 @@ Section vcg.
rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
+ iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
Qed.
Qed. *) Admitted.
Import environments.
Import env_notations.
......@@ -409,4 +423,4 @@ Section vcg.
iIntros (v) "H". by iDestruct "H" as (dv) "[-> H2]".
Qed.
End vcg.
\ No newline at end of file
End vcg.
......@@ -3,14 +3,14 @@ From iris.algebra Require Import frac.
From iris_c.lib Require Import locking_heap.
From iris.proofmode Require Import modalities classes.
Section contents.
Section U.
Context `{heapG Σ, locking_heapG Σ}.
(** * Unlocking modality *)
Definition U (P : iProp Σ) : iProp Σ :=
( ls : list (loc*(frac*val)),
([ list] x ls, x.1 L{x.2.1} x.2.2)
(([ list] x ls, x.1 U{x.2.1} x.2.2) - P))%I.
( ls : list (loc * (frac * val)),
([ list] x ls, x.1 C[LLvl]{x.2.1} x.2.2)
(([ list] x ls, x.1 C{x.2.1} x.2.2) - P))%I.
Lemma U_mono P Q : (P Q) U P U Q.
Proof.
......@@ -20,10 +20,7 @@ Section contents.
Qed.
Lemma U_intro P : P U P.
Proof.
iIntros "HP". iExists [].
rewrite !big_sepL_nil. eauto.
Qed.
Proof. iIntros "HP". iExists []. eauto. Qed.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Lemma U_sep_2 P Q : U P U Q U (P Q).
......@@ -31,12 +28,19 @@ Section contents.
iIntros "[HP HQ]".
iDestruct "HP" as (ls1) "[HP1 HP2]".
iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
iExists (ls1 ++ ls2). iFrame.
iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
- by iApply "HP2".
- by iApply "HQ2".
Qed.
Global Instance U_monoid_morphism : MonoidHomomorphism bi_sep bi_sep (flip ()) U.
Proof. split. split; try apply _. solve_proper. apply U_sep_2. apply U_intro. Qed.
Lemma U_big_sepL {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) U ([ list] ix l, Φ i x))%I.
Proof. apply big_opL_commute, _. Qed.
Lemma U_stength P Q : P U Q U (P Q).
Proof. by rewrite {1}(U_intro P) U_sep_2. Qed.
......@@ -50,7 +54,7 @@ Section contents.
iApply ("HP2" with "HP1").
Qed.
Lemma U_unlock l q v : l L{q} v U (l U{q} v).
Lemma U_unlock l q v : l C[LLvl]{q} v U (l C{q} v).
Proof.
iIntros "Hl". iExists [(l,(q,v))]. iIntros "/= {$Hl} [$ _]".
Qed.
......@@ -60,7 +64,8 @@ Section contents.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
Global Instance into_unlock_id P : IntoUnlock P P | 10.
Proof. apply U_intro. Qed.
Global Instance into_unlock_unlock l q v : IntoUnlock (l L{q} v)%I (l U{q} v)%I | 0.
Global Instance into_unlock_unlock l q v :
IntoUnlock (l C[LLvl]{q} v)%I (l C{q} v)%I | 0.
Proof. apply U_unlock. Qed.