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

heap_lang/heap.v

@@ -84,8 +84,7 @@ Section heap.
     P ⊑ wp E (Load (Loc l)) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros HN Hl Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) id).
-    { eassumption. } { eassumption. }
+    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) id); 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 /=.
@@ -95,9 +94,6 @@ Section heap.
       case _:(hf !! l)=>[[?||]|]; by auto. }
     apply later_mono, wand_intro_l. rewrite left_id const_equiv // left_id.
     by rewrite -later_intro.
-  Unshelve.
-  (* TODO Make it so that this becomes a goal, not shelved. *)
-  { eexists; eauto. }
   Qed.
 
   Lemma wp_load N E γ l v P Q :
@@ -118,8 +114,7 @@ Section heap.
     P ⊑ wp E (Store (Loc l) e) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros HN Hval Hl Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) (alter (λ _, Excl v) l)).
-    { eassumption. } { eassumption. }
+    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 /=.
@@ -147,9 +142,6 @@ Section heap.
       case (hf !! l')=>[[?||]|]; auto; contradiction.
     - rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap !lookup_op !lookup_fmap.
       rewrite lookup_insert_ne //.
-  Unshelve.
-  (* TODO Make it so that this becomes a goal, not shelved. *)
-  { eexists; eauto. }
   Qed.
 
   Lemma wp_store N E γ l e v v' P Q :

program_logic/auth.v

@@ -83,24 +83,28 @@ Section auth.
   (* Notice how the user has to prove that `b⋅a'` is valid at all
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
-  Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
-        L `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
+  Lemma auth_fsa {B} (fsa : FSA Λ (globalF Σ) B) `{!FrameShiftAssertion fsaV fsa}
+       L `{!LocalUpdate Lv L} N E P (Q : B → iPropG Λ Σ) γ a :
+    fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
-    P ⊑ (auth_own AuthI γ a ★ (∀ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') -★
-        FSA (E ∖ nclose N) (λ x, ■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own AuthI γ (L a) -★ Q x)))) →
-    P ⊑ FSA E Q.
+    P ⊑ (auth_own AuthI γ a ★ (∀ a',
+          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          fsa (E ∖ nclose N) (λ x,
+            ■ (Lv a ∧ ✓(L a⋅a')) ★ ▷ φ (L a ⋅ a') ★
+            (auth_own AuthI γ (L a) -★ Q x)))) →
+    P ⊑ fsa E Q.
   Proof.
-    rewrite /auth_ctx=>HN Hinv Hinner.
-    eapply inv_fsa; [eassumption..|]. rewrite Hinner=>{Hinner Hinv P}.
+    rewrite /auth_ctx=>? HN Hinv Hinner.
+    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P}.
     apply wand_intro_l.
     rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
-    apply fsa_strip_pvs; first done. apply exist_elim=>a'.
+    apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     rewrite wand_elim_r fsa_frame_l.
-    apply fsa_mono_pvs; first done. intros x. rewrite comm -!assoc.
+    apply (fsa_mono_pvs fsa)=> x. rewrite comm -!assoc.
     apply const_elim_sep_l=>-[HL Hv].
     rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
     rewrite auth_closing //; []. erewrite pvs_frame_l. apply pvs_mono.

program_logic/invariants.v

@@ -66,22 +66,24 @@ Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
 Proof. by rewrite always_always. Qed.
 
 (** Invariants can be opened around any frame-shifting assertion. *)
-Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
-      E N P (Q : A → iProp Λ Σ) R :
+Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}
+    E N P (Q : A → iProp Λ Σ) R :
+  fsaV →
   nclose N ⊆ E →
   R ⊑ inv N P →
-  R ⊑ (▷P -★ FSA (E ∖ nclose N) (λ a, ▷P ★ Q a)) →
-  R ⊑ FSA E Q.
+  R ⊑ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Q a)) →
+  R ⊑ fsa E Q.
 Proof.
-  move=>HN Hinv Hinner. rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
+  intros ? HN Hinv Hinner.
+  rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
   rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
   rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
-  rewrite -(fsa_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+.
+  rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by solve_elem_of+.
   (* Add this to the local context, so that solve_elem_of finds it. *)
   assert ({[encode i]} ⊆ nclose N) by eauto.
   rewrite (always_sep_dup (ownI _ _)).
   rewrite {1}pvs_openI !pvs_frame_r.
-  apply pvs_mask_frame_mono ; [solve_elem_of..|].
+  apply pvs_mask_frame_mono; [solve_elem_of..|].
   rewrite (comm _ (▷_)%I) -assoc wand_elim_r fsa_frame_l.
   apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
   rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
@@ -95,15 +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. move=>HN ? ?. apply: (inv_fsa pvs_fsa); eassumption. Qed.
+Proof. intros. by apply: (inv_fsa pvs_fsa); try eassumption. 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.
-  move=>He HN ? ?. apply: (inv_fsa (wp_fsa e _)); eassumption. Qed.
+Proof. intros. apply: (inv_fsa (wp_fsa e)); eassumption. 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.

program_logic/pviewshifts.v

@@ -181,59 +181,42 @@ Qed.
 End pvs.
 
 (** * Frame Shift Assertions. *)
-Section fsa.
-Context {Λ : language} {Σ : iFunctor} {A : Type}.
-Implicit Types P : iProp Λ Σ.
-Implicit Types Q : A → iProp Λ Σ.
-
 (* Yes, the name is horrible...
    Frame Shift Assertions take a mask and a predicate over some type (that's
    their "postcondition"). They support weakening the mask, framing resources
    into the postcondition, and composition witn mask-changing view shifts. *)
-Class FrameShiftAssertion (FSA : coPset → (A → iProp Λ Σ) → iProp Λ Σ) := {
-  fsa_mask_frame_mono E1 E2 Q Q' :> E1 ⊆ E2 →
-                                 (∀ a, Q a ⊑ Q' a) → FSA E1 Q ⊑ FSA E2 Q';
-  fsa_trans3 E1 E2 Q : E2 ⊆ E1 →
-                     pvs E1 E2 (FSA E2 (λ a, pvs E2 E1 (Q a))) ⊑ FSA E1 Q;
-  fsa_frame_r E P Q : (FSA E Q ★ P) ⊑ FSA E (λ a, Q a ★ P)
+Notation FSA Λ Σ A := (coPset → (A → iProp Λ Σ) → iProp Λ Σ).
+Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
+  fsa_mask_frame_mono E1 E2 Q Q' :
+    E1 ⊆ E2 → (∀ a, Q a ⊑ Q' a) → fsa E1 Q ⊑ fsa E2 Q';
+  fsa_trans3 E Q : pvs E E (fsa E (λ a, pvs E E (Q a))) ⊑ fsa E Q;
+  fsa_open_close E1 E2 Q :
+    fsaV → E2 ⊆ E1 → pvs E1 E2 (fsa E2 (λ a, pvs E2 E1 (Q a))) ⊑ fsa E1 Q;
+  fsa_frame_r E P Q : (fsa E Q ★ P) ⊑ fsa E (λ a, Q a ★ P)
 }.
 
-Context FSA `{FrameShiftAssertion FSA}.
-Lemma fsa_mono E Q Q' : (∀ a, Q a ⊑ Q' a) → FSA E Q ⊑ FSA E Q'.
+Section fsa.
+Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
+Implicit Types Q : A → iProp Λ Σ.
+
+Lemma fsa_mono E Q Q' : (∀ a, Q a ⊑ Q' a) → fsa E Q ⊑ fsa E Q'.
 Proof. apply fsa_mask_frame_mono; auto. Qed.
-Lemma fsa_mask_weaken E1 E2 Q : E1 ⊆ E2 → FSA E1 Q ⊑ FSA E2 Q.
+Lemma fsa_mask_weaken E1 E2 Q : E1 ⊆ E2 → fsa E1 Q ⊑ fsa E2 Q.
 Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
-Lemma fsa_frame_l E P Q :
-  (P ★ FSA E Q) ⊑ FSA E (λ a, P ★ Q a).
-Proof.
-  rewrite comm fsa_frame_r. apply fsa_mono=>a.
-  by rewrite comm.
-Qed.
-Lemma fsa_strip_pvs E P Q : P ⊑ FSA E Q → pvs E E P ⊑ FSA E Q.
-Proof.
-  move=>->. rewrite -{2}fsa_trans3; last reflexivity.
-  apply pvs_mono, fsa_mono=>a. apply pvs_intro.  
-Qed.
-Lemma fsa_mono_pvs E Q Q' : (∀ a, Q a ⊑ pvs E E (Q' a)) → FSA E Q ⊑ FSA E Q'.
+Lemma fsa_frame_l E P Q : (P ★ fsa E Q) ⊑ fsa E (λ a, P ★ Q a).
+Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
+Lemma fsa_strip_pvs E P Q : P ⊑ fsa E Q → pvs E E P ⊑ fsa E Q.
 Proof.
-  move=>HQ. rewrite -[FSA E Q']fsa_trans3; last reflexivity.
-  rewrite -pvs_intro. by apply fsa_mono.
+  move=>->. rewrite -{2}fsa_trans3.
+  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
 Qed.
-
+Lemma fsa_mono_pvs E Q Q' : (∀ a, Q a ⊑ pvs E E (Q' a)) → fsa E Q ⊑ fsa E Q'.
+Proof. intros. rewrite -[fsa E Q']fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
 End fsa.
 
-(** View shifts are a FSA. *)
-Section pvs_fsa.
-Context {Λ : language} {Σ : iFunctor}.
-Implicit Types P : iProp Λ Σ.
-Implicit Types Q : () → iProp Λ Σ.
-
-Global Instance pvs_fsa : FrameShiftAssertion (λ E Q, pvs E E (Q ())).
+Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Q, pvs E E (Q ()).
+Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
 Proof.
-  split; intros.
-  - apply pvs_mask_frame_mono; auto.
-  - apply pvs_trans3; auto.
-  - apply pvs_frame_r; auto.
+  rewrite /pvs_fsa.
+  split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
 Qed.
-
-End pvs_fsa.

program_logic/weakestpre.v

@@ -231,12 +231,10 @@ Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q.
 Proof. auto using wp_mask_frame_mono. Qed.
 
 (** * Weakest-pre is a FSA. *)
-Global Instance wp_fsa e : atomic e → FrameShiftAssertion (λ E Q, wp E e Q).
+Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e.
+Global Instance wp_fsa_prf : FrameShiftAssertion (atomic e) (wp_fsa e).
 Proof.
-  split; intros.
-  - apply wp_mask_frame_mono; auto.
-  - apply wp_atomic; auto.
-  - apply wp_frame_r; auto.
+  rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic, wp_frame_r.
+  intros E Q. by rewrite -(pvs_wp E e Q) -(wp_pvs E e Q).
 Qed.
-
 End wp.