Commit 0fd7e635 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Misc big op nitpicks

- The direction of big_sepS_later and big_sepM_later is now like later_sep.
- Do not use generated variables in the proofs.
parent ffb0a675
......@@ -708,10 +708,7 @@ Qed.
Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Lemma later_True : ( True : uPred M)%I True%I.
Proof.
apply (anti_symm ()); first done.
apply later_True'.
Qed.
Proof. apply (anti_symm ()); auto using later_True'. Qed.
Lemma later_impl P Q : (P Q) ( P Q).
Proof.
apply impl_intro_l; rewrite -later_and.
......
......@@ -142,18 +142,15 @@ Section gmap.
Lemma big_sepM_sepM P Q m :
(Π★{map m} (λ i x, P i x Q i x))%I (Π★{map m} P Π★{map m} Q)%I.
Proof.
rewrite /uPred_big_sepM. induction (map_to_list m); simpl;
first by rewrite right_id.
destruct a. rewrite IHl /= -!assoc. apply sep_proper; first done.
rewrite !assoc [(_ Q _ _)%I]comm -!assoc. apply sep_proper; done.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Q _ _)) [(Q _ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepM_later P m :
(Π★{map m} (λ i x, P i x))%I ( Π★{map m} P)%I.
Lemma big_sepM_later P m : ( Π★{map m} P)%I (Π★{map m} (λ i x, P i x))%I.
Proof.
rewrite /uPred_big_sepM. induction (map_to_list m); simpl;
first by rewrite later_True.
destruct a. by rewrite IHl later_sep.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
by rewrite later_sep IH.
Qed.
End gmap.
......@@ -205,18 +202,16 @@ Section gset.
Lemma big_sepS_sepS P Q X :
(Π★{set X} (λ x, P x Q x))%I (Π★{set X} P Π★{set X} Q)%I.
Proof.
rewrite /uPred_big_sepS. induction (elements X); simpl;
first by rewrite right_id.
rewrite IHl -!assoc. apply uPred.sep_proper; first done.
rewrite !assoc [(_ Q a)%I]comm -!assoc. apply sep_proper; done.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Q _)) [(Q _ _)%I]comm -!assoc.
Qed.
Lemma big_sepS_later P X :
(Π★{set X} (λ x, P x))%I ( Π★{set X} P)%I.
Lemma big_sepS_later P X : ( Π★{set X} P)%I (Π★{set X} (λ x, P x))%I.
Proof.
rewrite /uPred_big_sepS. induction (elements X); simpl;
first by rewrite later_True.
by rewrite IHl later_sep.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
by rewrite later_sep IH.
Qed.
End gset.
......
......@@ -203,7 +203,7 @@ Section proof.
(* Now we come to the core of the proof: Updating from waiting to ress. *)
rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Q} Q.
rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
rewrite -big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
rewrite big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
rewrite -(exist_intro (Q i)) comm. done.
Qed.
......
Markdown is supported
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