Commit 462cc285 authored by Ralf Jung's avatar Ralf Jung

make entailment notation look like entailment

parent 0c0ee757
......@@ -133,11 +133,11 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
(** Internalized properties *)
Lemma agree_equivI {M} a b : (to_agree a to_agree b)%I (a b : uPred M)%I.
Lemma agree_equivI {M} a b : (to_agree a to_agree b) ⊣⊢ (a b : uPred M).
Proof.
uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
Qed.
Lemma agree_validI {M} x y : (x y) (x y : uPred M).
Lemma agree_validI {M} x y : (x y) (x y : uPred M).
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
End agree.
......
......@@ -144,14 +144,14 @@ Qed.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
(x y)%I (authoritative x authoritative y own x own y : uPred M)%I.
(x y) ⊣⊢ (authoritative x authoritative y own x own y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
( x)%I (match authoritative x with
( x) ⊣⊢ (match authoritative x with
| Excl a => ( b, a own x b) a
| ExclUnit => own x
| ExclBot => False
end : uPred M)%I.
end : uPred M).
Proof. uPred.unseal. by destruct x as [[]]. Qed.
(** The notations and only work for CMRAs with an empty element. So, in
......
......@@ -145,16 +145,16 @@ Qed.
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
(x y)%I (match x, y with
(x y) ⊣⊢ (match x, y with
| Excl a, Excl b => a b
| ExclUnit, ExclUnit | ExclBot, ExclBot => True
| _, _ => False
end : uPred M)%I.
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
( x)%I (if x is ExclBot then False else True : uPred M)%I.
( x) ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
......
......@@ -170,9 +170,9 @@ Global Instance map_cmra_discrete : CMRADiscrete A → CMRADiscrete mapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
(** Internalized properties *)
Lemma map_equivI {M} m1 m2 : (m1 m2)%I ( i, m1 !! i m2 !! i : uPred M)%I.
Lemma map_equivI {M} m1 m2 : (m1 m2) ⊣⊢ ( i, m1 !! i m2 !! i : uPred M).
Proof. by uPred.unseal. Qed.
Lemma map_validI {M} m : ( m)%I ( i, (m !! i) : uPred M)%I.
Lemma map_validI {M} m : ( m) ⊣⊢ ( i, (m !! i) : uPred M).
Proof. by uPred.unseal. Qed.
End cmra.
......
......@@ -190,17 +190,17 @@ Proof. intros. by apply frac_validN_inv_l with 0 a, cmra_valid_validN. Qed.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
(x y)%I (match x, y with
(x y) ⊣⊢ (match x, y with
| Frac q1 a, Frac q2 b => q1 = q2 a b
| FracUnit, FracUnit => True
| _, _ => False
end : uPred M)%I.
end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; destruct 1; try constructor.
Qed.
Lemma frac_validI {M} (x : frac A) :
( x)%I (if x is Frac q a then (q 1)%Qc a else True : uPred M)%I.
( x) ⊣⊢ (if x is Frac q a then (q 1)%Qc a else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
......
......@@ -170,9 +170,9 @@ Section iprod_cmra.
Qed.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : (g1 g2)%I ( i, g1 i g2 i : uPred M)%I.
Lemma iprod_equivI {M} g1 g2 : (g1 g2) ⊣⊢ ( i, g1 i g2 i : uPred M).
Proof. by uPred.unseal. Qed.
Lemma iprod_validI {M} g : ( g)%I ( i, g i : uPred M)%I.
Lemma iprod_validI {M} g : ( g) ⊣⊢ ( i, g i : uPred M).
Proof. by uPred.unseal. Qed.
(** Properties of iprod_insert. *)
......
......@@ -138,14 +138,14 @@ Proof. by destruct mx, my; inversion_clear 1. Qed.
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
(x y)%I (match x, y with
(x y) ⊣⊢ (match x, y with
| Some a, Some b => a b | None, None => True | _, _ => False
end : uPred M)%I.
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma option_validI {M} (x : option A) :
( x)%I (match x with Some a => a | None => True end : uPred M)%I.
( x) ⊣⊢ (match x with Some a => a | None => True end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
......
This diff is collapsed.
......@@ -39,9 +39,9 @@ Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
(* Big ops *)
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
Global Instance big_and_proper : Proper (() ==> (⊣⊢)) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
Global Instance big_sep_proper : Proper (() ==> (⊣⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_ne n :
......@@ -51,19 +51,19 @@ Global Instance big_sep_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_perm : Proper ((≡ₚ) ==> ()) (@uPred_big_and M).
Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
Global Instance big_sep_perm : Proper ((≡ₚ) ==> ()) (@uPred_big_sep M).
Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
......@@ -71,26 +71,26 @@ Proof.
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I (Π∧ Ps Π∧ Qs)%I.
Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs)) ⊣⊢ (Π∧ Ps Π∧ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I (Π★ Ps Π★ Qs)%I.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs)) ⊣⊢ (Π★ Ps Π★ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps (Π∧ Ps)%I (Π∧ Qs)%I.
Lemma big_and_contains Ps Qs : Qs `contains` Ps (Π∧ Ps) (Π∧ Qs).
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps (Π★ Ps)%I (Π★ Qs)%I.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps (Π★ Ps) (Π★ Qs).
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
Qed.
Lemma big_sep_and Ps : (Π★ Ps) (Π∧ Ps).
Lemma big_sep_and Ps : (Π★ Ps) (Π∧ Ps).
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
Lemma big_and_elem_of Ps P : P Ps (Π∧ Ps) P.
Lemma big_and_elem_of Ps P : P Ps (Π∧ Ps) P.
Proof. induction 1; simpl; auto with I. Qed.
Lemma big_sep_elem_of Ps P : P Ps (Π★ Ps) P.
Lemma big_sep_elem_of Ps P : P Ps (Π★ Ps) P.
Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *)
......@@ -100,8 +100,8 @@ Section gmap.
Implicit Types Φ Ψ : K A uPred M.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x)
(Π★{map m1} Φ) (Π★{map m2} Ψ).
m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x)
(Π★{map m1} Φ) (Π★{map m2} Ψ).
Proof.
intros HX HΦ. trans (Π★{map m2} Φ)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
......@@ -117,36 +117,36 @@ Section gmap.
apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper m :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
(uPred_big_sepM (M:=M) m).
Proof.
intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
apply big_sepM_ne=> k x; apply equiv_dist, HΦ.
Qed.
Global Instance big_sepM_mono' m :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
Lemma big_sepM_empty Φ : (Π★{map } Φ)%I True%I.
Lemma big_sepM_empty Φ : (Π★{map } Φ) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ (m : gmap K A) i x :
m !! i = None (Π★{map <[i:=x]> m} Φ)%I (Φ i x Π★{map m} Φ)%I.
m !! i = None (Π★{map <[i:=x]> m} Φ) ⊣⊢ (Φ i x Π★{map m} Φ).
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I (Φ i x)%I.
Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ) ⊣⊢ (Φ i x).
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_sepM Φ Ψ m :
(Π★{map m} (λ i x, Φ i x Ψ i x))%I (Π★{map m} Φ Π★{map m} Ψ)%I.
(Π★{map m} (λ i x, Φ i x Ψ i x)) ⊣⊢ (Π★{map m} Φ Π★{map m} Ψ).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepM_later Φ m : ( Π★{map m} Φ)%I (Π★{map m} (λ i x, Φ i x))%I.
Lemma big_sepM_later Φ m : ( Π★{map m} Φ) ⊣⊢ (Π★{map m} (λ i x, Φ i x)).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
......@@ -161,7 +161,7 @@ Section gset.
Implicit Types Φ : A uPred M.
Lemma big_sepS_mono Φ Ψ X Y :
Y X ( x, x Y Φ x Ψ x) (Π★{set X} Φ) (Π★{set Y} Ψ).
Y X ( x, x Y Φ x Ψ x) (Π★{set X} Φ) (Π★{set Y} Ψ).
Proof.
intros HX HΦ. trans (Π★{set Y} Φ)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
......@@ -176,38 +176,38 @@ Section gset.
apply Forall2_Forall, Forall_true=> x; apply HΦ.
Qed.
Lemma big_sepS_proper X :
Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
Proof.
intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
apply big_sepS_ne=> x; apply equiv_dist, HΦ.
Qed.
Lemma big_sepS_mono' X :
Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
Lemma big_sepS_empty Φ : (Π★{set } Φ)%I True%I.
Lemma big_sepS_empty Φ : (Π★{set } Φ) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
x X (Π★{set {[ x ]} X} Φ)%I (Φ x Π★{set X} Φ)%I.
x X (Π★{set {[ x ]} X} Φ) ⊣⊢ (Φ x Π★{set X} Φ).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_delete Φ X x :
x X (Π★{set X} Φ)%I (Φ x Π★{set X {[ x ]}} Φ)%I.
x X (Π★{set X} Φ) ⊣⊢ (Φ x Π★{set X {[ x ]}} Φ).
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I (Φ x)%I.
Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ) ⊣⊢ (Φ x).
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
(Π★{set X} (λ x, Φ x Ψ x))%I (Π★{set X} Φ Π★{set X} Ψ)%I.
(Π★{set X} (λ x, Φ x Ψ x)) ⊣⊢ (Π★{set X} Φ Π★{set X} Ψ).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepS_later Φ X : ( Π★{set X} Φ)%I (Π★{set X} (λ x, Φ x))%I.
Lemma big_sepS_later Φ X : ( Π★{set X} Φ) ⊣⊢ (Π★{set X} (λ x, Φ x)).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
......
......@@ -24,18 +24,18 @@ Module uPred_reflection. Section uPred_reflection.
Notation eval_list Σ l :=
(uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
Lemma eval_flatten Σ e : eval Σ e eval_list Σ (flatten e).
Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //.
Qed.
Lemma flatten_entails Σ e1 e2 :
flatten e2 `contains` flatten e1 eval Σ e1 eval Σ e2.
flatten e2 `contains` flatten e1 eval Σ e1 eval Σ e2.
Proof.
intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
Qed.
Lemma flatten_equiv Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 eval Σ e1 eval Σ e2.
flatten e2 ≡ₚ flatten e1 eval Σ e1 ⊣⊢ eval Σ e2.
Proof. intros He. by rewrite !eval_flatten He. Qed.
Fixpoint prune (e : expr) : expr :=
......@@ -54,7 +54,7 @@ Module uPred_reflection. Section uPred_reflection.
induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
Qed.
Lemma prune_correct Σ e : eval Σ (prune e) eval Σ e.
Lemma prune_correct Σ e : eval Σ (prune e) ⊣⊢ eval Σ e.
Proof. by rewrite !eval_flatten flatten_prune. Qed.
Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
......@@ -86,7 +86,7 @@ Module uPred_reflection. Section uPred_reflection.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' cancel ns e2 = Some e2'
eval Σ e1' eval Σ e2' eval Σ e1 eval Σ e2.
eval Σ e1' eval Σ e2' eval Σ e1 eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
......@@ -100,20 +100,20 @@ Module uPred_reflection. Section uPred_reflection.
| n :: l => ESep (EVar n) (to_expr l)
end.
Arguments to_expr !_ / : simpl nomatch.
Lemma eval_to_expr Σ l : eval Σ (to_expr l) eval_list Σ l.
Lemma eval_to_expr Σ l : eval Σ (to_expr l) ⊣⊢ eval_list Σ l.
Proof.
induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
by rewrite IH.
Qed.
Lemma split_l Σ e ns e' :
cancel ns e = Some e' eval Σ e (eval Σ (to_expr ns) eval Σ e')%I.
cancel ns e = Some e' eval Σ e ⊣⊢ (eval Σ (to_expr ns) eval Σ e').
Proof.
intros He%flatten_cancel.
by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
Qed.
Lemma split_r Σ e ns e' :
cancel ns e = Some e' eval Σ e (eval Σ e' eval Σ (to_expr ns))%I.
cancel ns e = Some e' eval Σ e ⊣⊢ (eval Σ e' eval Σ (to_expr ns)).
Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
......@@ -132,16 +132,16 @@ Module uPred_reflection. Section uPred_reflection.
Ltac quote :=
match goal with
| |- ?P1 ?P2 =>
| |- ?P1 ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
change (eval Σ3 e1 eval Σ3 e2) end end
change (eval Σ3 e1 eval Σ3 e2) end end
end.
Ltac quote_l :=
match goal with
| |- ?P1 ?P2 =>
| |- ?P1 ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
change (eval Σ2 e1 P2) end
change (eval Σ2 e1 P2) end
end.
End uPred_reflection.
......@@ -162,7 +162,7 @@ Ltac close_uPreds Ps tac :=
Tactic Notation "cancel" constr(Ps) :=
uPred_reflection.quote;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
......@@ -172,12 +172,12 @@ Tactic Notation "cancel" constr(Ps) :=
Tactic Notation "ecancel" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Qs => cancel Qs).
(** [to_front [P1, P2, ..]] rewrites in the premise of such that
(** [to_front [P1, P2, ..]] rewrites in the premise of such that
the assumptions P1, P2, ... appear at the front, in that order. *)
Tactic Notation "to_front" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
......@@ -188,7 +188,7 @@ Tactic Notation "to_front" open_constr(Ps) :=
Tactic Notation "to_back" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
......@@ -205,46 +205,46 @@ Tactic Notation "sep_split" "right:" open_constr(Ps) :=
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
to_front Ps; apply sep_mono.
(** Assumes a goal of the shape P Q. Alterantively, if Q
(** Assumes a goal of the shape P Q. Alterantively, if Q
is built of , , with in all branches; that will work, too.
Will turn this goal into P Q and strip in P below , , . *)
Will turn this goal into P Q and strip in P below , , . *)
Ltac strip_later :=
let rec strip :=
lazymatch goal with
| |- (_ _) _ =>
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_sep);
apply sep_mono; strip
| |- (_ _) _ =>
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_and);
apply sep_mono; strip
| |- (_ _) _ =>
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_or);
apply sep_mono; strip
| |- _ _ => apply later_mono; reflexivity
| |- _ _ => apply later_intro; reflexivity
| |- _ _ => apply later_mono; reflexivity
| |- _ _ => apply later_intro; reflexivity
end
in let rec shape_Q :=
lazymatch goal with
| |- _ (_ _) =>
| |- _ (_ _) =>
(* Force the later on the LHS to be top-level, matching laters
below on the RHS *)
etrans; first (apply equiv_entails, later_sep; reflexivity);
(* Match the arm recursively *)
apply sep_mono; shape_Q
| |- _ (_ _) =>
| |- _ (_ _) =>
etrans; first (apply equiv_entails, later_and; reflexivity);
apply sep_mono; shape_Q
| |- _ (_ _) =>
| |- _ (_ _) =>
etrans; first (apply equiv_entails, later_or; reflexivity);
apply sep_mono; shape_Q
| |- _ _ => apply later_mono; reflexivity
| |- _ _ => apply later_mono; reflexivity
(* We fail if we don't find laters in all branches. *)
end
in intros_revert ltac:(etrans; [|shape_Q];
etrans; last eapply later_mono; first solve [ strip ]).
(** Transforms a goal of the form ..., ?0... ?1 ?2
into True ..., ?0... ?1 ?2, applies tac, and
(** Transforms a goal of the form ..., ?0... ?1 ?2
into True ..., ?0... ?1 ?2, applies tac, and
the moves all the assumptions back. *)
(* TODO: this name may be a big too general *)
Ltac revert_all :=
......@@ -256,20 +256,20 @@ Ltac revert_all :=
on the sort of the argument, which is suboptimal. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
| |- _ _ => apply impl_entails
| |- _ _ => apply impl_entails
end.
(** This starts on a goal of the form ..., ?0... ?1 ?2.
(** This starts on a goal of the form ..., ?0... ?1 ?2.
It applies löb where all the Coq assumptions have been turned into logical
assumptions, then moves all the Coq assumptions back out to the context,
applies [tac] on the goal (now of the form _ _), and then reverts the
applies [tac] on the goal (now of the form _ _), and then reverts the
Coq assumption so that we end up with the same shape as where we started,
but with an additional assumption -ed to the context *)
Ltac löb tac :=
revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
(* We now have a goal for the form True P, with the "original" conclusion
(* We now have a goal for the form True P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
first (apply equiv_entails, left_id, _; reflexivity);
......@@ -278,13 +278,13 @@ Ltac löb tac :=
do the work *)
let rec go :=
lazymatch goal with
| |- _ ( _, _) =>
| |- _ ( _, _) =>
apply forall_intro; let H := fresh in intro H; go; revert H
| |- _ ( _ _) =>
| |- _ ( _ _) =>
apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H
(* This is the "bottom" of the goal, where we see the impl introduced
by uPred_revert_all as well as the from löb_strong and the we added. *)
| |- ?R (?L _) => apply impl_intro_l;
| |- ?R (?L _) => apply impl_intro_l;
trans (L R)%I;
[eapply equiv_entails, always_and_sep_r, _; reflexivity | tac]
end
......
......@@ -19,16 +19,16 @@ Section client.
( f : val, y {q} f n : Z, #> f §n {{ λ v, v = §(n + 42) }})%I.
Lemma y_inv_split q y :
y_inv q y (y_inv (q/2) y y_inv (q/2) y).
y_inv q y (y_inv (q/2) y y_inv (q/2) y).
Proof.
rewrite /y_inv. apply exist_elim=>f.
rewrite -!(exist_intro f). rewrite heap_mapsto_op_split.
ecancel [y {_} _; y {_} _]%I. by rewrite [X in X _]always_sep_dup.
ecancel [y {_} _; y {_} _]%I. by rewrite [X in X _]always_sep_dup.
Qed.
Lemma worker_safe q (n : Z) (b y : loc) :
(heap_ctx heapN recv heapN N b (y_inv q y))
#> worker n (%b) (%y) {{ λ _, True }}.
#> worker n (%b) (%y) {{ λ _, True }}.
Proof.
rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
rewrite comm. apply sep_mono_r. apply wand_intro_l.
......@@ -42,7 +42,7 @@ Section client.
Qed.
Lemma client_safe :
heapN N heap_ctx heapN #> client {{ λ _, True }}.
heapN N heap_ctx heapN #> client {{ λ _, True }}.
Proof.
intros ?. rewrite /client.
(ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y.
......
......@@ -82,7 +82,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
(saved_prop_own i2 R2
saved_prop_own i1 R1 saved_prop_own i Q
(Q - R1 R2) ress P I)
ress P ({[i1]} ({[i2]} (I {[i]}))).
ress P ({[i1]} ({[i2]} (I {[i]}))).
Proof.
intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.