Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/upred.v

@@ -615,6 +615,10 @@ Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q).
 Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
 Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q).
 Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
+Lemma sep_elim_True_l P Q R : True ⊑ P → (P ★ R) ⊑ Q → R ⊑ Q.
+Proof. by intros HP; rewrite -HP left_id. Qed.
+Lemma sep_elim_True_r P Q R : True ⊑ P → (R ★ P) ⊑ Q → R ⊑ Q.
+Proof. by intros HP; rewrite -HP right_id. Qed.
 Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
 Proof. rewrite comm; apply wand_intro_r. Qed.
 Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.

heap_lang/heap.v

@@ -84,7 +84,7 @@ Section heap.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
     rewrite {1}[(▷ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
-    rewrite -wp_alloc_pst; first (apply sep_mono; first done); try eassumption.
+    rewrite -wp_alloc_pst; first (apply sep_mono; first done); try done; [].
     apply later_mono, forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
     rewrite -(exist_intro l) !left_id. rewrite always_and_sep_l -assoc.
     apply const_elim_sep_l=>Hfresh.
@@ -119,8 +119,10 @@ Section heap.
     P ⊑ (▷ (∀ l, heap_mapsto HeapI γ l v -★ Q (LocV l))) →
     P ⊑ wp E (Alloc e) Q.
   Proof.
-    intros HN ? Hctx HP. rewrite -(right_id True%I (★)%I (P)) (auth_empty γ) pvs_frame_l.
-    apply wp_strip_pvs. eapply wp_alloc_heap with (σ:=∅); try eassumption.
+    intros HN ? Hctx HP. eapply sep_elim_True_r.
+    { eapply (auth_empty γ). }
+    rewrite pvs_frame_l. apply wp_strip_pvs.
+    eapply wp_alloc_heap with (σ:=∅); try done; [|].
     { eauto with I. }
     rewrite HP comm. apply sep_mono.
     - rewrite /heap_own. f_equiv. apply: map_eq=>l. by rewrite lookup_fmap !lookup_empty.
@@ -166,12 +168,13 @@ Section heap.
     P ⊑ wp E (Store (Loc l) e) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros Hl Hval HN Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (λ _:(), alter (λ _, Excl v) l)); simpl; eauto.
+    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _)
+                     (λ _:(), alter (λ _, Excl v) l)); simpl; eauto.
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
     rewrite {1}[(▷ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
-    rewrite -wp_store_pst; first (apply sep_mono; first done); try eassumption; last first.
+    rewrite -wp_store_pst; first (apply sep_mono; first done); try done; last first.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
@@ -189,12 +192,13 @@ Section heap.
       + by rewrite lookup_alter /to_heap !lookup_fmap lookup_insert Hl /=.
       + rewrite lookup_alter_ne // !lookup_fmap lookup_insert_ne //. }
     rewrite !EQ. apply sep_mono; last done.
-    f_equiv. apply: map_eq=>l'. move: (Hv 0%nat l'). destruct (decide (l=l')); simplify_map_equality.
+    f_equiv. apply: map_eq=>l'. move: (Hv 0%nat l').
+    destruct (decide (l=l')); simplify_map_equality.
     - rewrite /from_heap /to_heap lookup_insert lookup_omap !lookup_op.
       rewrite !lookup_fmap lookup_insert Hl.
       case (hf !! l')=>[[?||]|]; auto; contradiction.
-    - rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap !lookup_op !lookup_fmap.
-      rewrite lookup_insert_ne //.
+    - rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap.
+      rewrite !lookup_op !lookup_fmap lookup_insert_ne //.
   Qed.
 
   Lemma wp_store N E γ l v' e v P Q :
@@ -204,7 +208,8 @@ Section heap.
     P ⊑ (heap_mapsto HeapI γ l v' ★ ▷ (heap_mapsto HeapI γ l v -★ Q (LitV LitUnit))) →
     P ⊑ wp E (Store (Loc l) e) Q.
   Proof.
-    rewrite /heap_mapsto=>Hval HN Hctx HP. eapply wp_store_heap; try eassumption; last first.
+    rewrite /heap_mapsto=>Hval HN Hctx HP.
+    eapply wp_store_heap; try done; last first.
     - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
     - by rewrite lookup_insert.
   Qed.
@@ -223,7 +228,7 @@ Section heap.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
     rewrite {1}[(▷ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
-    rewrite -wp_cas_fail_pst; first (apply sep_mono; first done); try eassumption; last first.
+    rewrite -wp_cas_fail_pst; first (apply sep_mono; first done); try done; last first.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
@@ -238,7 +243,7 @@ Section heap.
     P ⊑ (heap_mapsto HeapI γ l v' ★ ▷ (heap_mapsto HeapI γ l v' -★ Q 'false)) →
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
-    rewrite /heap_mapsto=>???. eapply wp_cas_fail_heap; try eassumption.
+    rewrite /heap_mapsto=>???. eapply wp_cas_fail_heap; try done; [].
     by simplify_map_equality.
   Qed.
 
@@ -256,7 +261,7 @@ Section heap.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
     rewrite -assoc. apply const_elim_sep_l=>Hv /=.
     rewrite {1}[(▷ownP _)%I]pvs_timeless !pvs_frame_r. apply wp_strip_pvs.
-    rewrite -wp_cas_suc_pst; first (apply sep_mono; first done); try eassumption; last first.
+    rewrite -wp_cas_suc_pst; first (apply sep_mono; first done); try done; last first.
     { move: (Hv 0%nat l). rewrite lookup_omap lookup_op lookup_fmap Hl /=.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l.
@@ -289,7 +294,7 @@ Section heap.
     P ⊑ (heap_mapsto HeapI γ l v1 ★ ▷ (heap_mapsto HeapI γ l v2 -★ Q 'true)) →
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
-    rewrite /heap_mapsto=>???? HP. eapply wp_cas_suc_heap; try eassumption; last first.
+    rewrite /heap_mapsto=>???? HP. eapply wp_cas_suc_heap; try done; last first.
     - rewrite HP. apply sep_mono; first done. by rewrite insert_singleton.
     - by simplify_map_equality.
   Qed.

program_logic/auth.v

@@ -32,8 +32,8 @@ Section auth.
   Lemma auth_alloc N a :
     ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx AuthI γ N φ ∧ auth_own AuthI γ a).
   Proof.
-    intros Ha. rewrite -(right_id True%I (★)%I (φ _)).
-    rewrite (own_alloc AuthI (Auth (Excl a) a) N) //; [].
+    intros Ha. eapply sep_elim_True_r.
+    { by eapply (own_alloc AuthI (Auth (Excl a) a) N). }
     rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ a)%I.

program_logic/invariants.v

@@ -97,14 +97,14 @@ Lemma pvs_open_close E N P Q R :
   R ⊑ inv N P →
   R ⊑ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q)) →
   R ⊑ pvs E E Q.
-Proof. intros. by apply: (inv_fsa pvs_fsa); try eassumption. Qed.
+Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
 
 Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) R :
   atomic e → nclose N ⊆ E →
   R ⊑ inv N P →
   R ⊑ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)) →
   R ⊑ wp E e Q.
-Proof. intros. apply: (inv_fsa (wp_fsa e)); eassumption. Qed.
+Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 
 Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.