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

algebra/base.v

-From mathcomp.ssreflect Require Export ssreflect.
+From mathcomp Require Export ssreflect.
 From prelude Require Export prelude.
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.

algebra/fin_maps.v

@@ -62,7 +62,7 @@ Proof.
 Qed.
 
 Global Instance map_timeless `{∀ a : A, Timeless a} m : Timeless m.
-Proof. by intros m' ? i; apply (timeless _). Qed.
+Proof. by intros m' ? i; apply: timeless. Qed.
 
 Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
@@ -71,7 +71,7 @@ Proof.
 Qed.
 Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i).
 Proof.
-  intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
+  intros ? [x|] Hx; [|by symmetry; apply: timeless].
   assert (m ≡{0}≡ <[i:=x]> m)
     by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
   by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
@@ -80,8 +80,8 @@ Global Instance map_insert_timeless m i x :
   Timeless x → Timeless m → Timeless (<[i:=x]>m).
 Proof.
   intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
-  { by apply (timeless _); rewrite -Hm lookup_insert. }
-  by apply (timeless _); rewrite -Hm lookup_insert_ne.
+  { by apply: timeless; rewrite -Hm lookup_insert. }
+  by apply: timeless; rewrite -Hm lookup_insert_ne.
 Qed.
 Global Instance map_singleton_timeless i x :
   Timeless x → Timeless ({[ i := x ]} : gmap K A) := _.

algebra/iprod.v

@@ -49,7 +49,7 @@ Section iprod_cofe.
     Definition iprod_lookup_empty  x : ∅ x = ∅ := eq_refl.
     Global Instance iprod_empty_timeless :
       (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B).
-    Proof. intros ? f Hf x. by apply (timeless _). Qed.
+    Proof. intros ? f Hf x. by apply: timeless. Qed.
   End empty.
 
   (** Properties of iprod_insert. *)
@@ -78,7 +78,7 @@ Section iprod_cofe.
     intros ? y ?.
     cut (f ≡ iprod_insert x y f).
     { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
-    by apply (timeless _)=>x'; destruct (decide (x = x')) as [->|];
+    by apply: timeless=>x'; destruct (decide (x = x')) as [->|];
       rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
   Qed.
   Global Instance iprod_insert_timeless f x y :
@@ -86,9 +86,9 @@ Section iprod_cofe.
   Proof.
     intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
     - rewrite iprod_lookup_insert.
-      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert.
+      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert.
     - rewrite iprod_lookup_insert_ne //.
-      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert_ne.
+      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne.
   Qed.
 
   (** Properties of iprod_singletom. *)

algebra/upred.v

@@ -301,7 +301,7 @@ Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
 Global Instance forall_proper A :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A).
 Proof. by intros Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
-Global Instance exists_ne A :
+Global Instance exist_ne A :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
 Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
 Global Instance exist_proper A :

barrier/barrier.v

 From algebra Require Export upred_big_op.
 From program_logic Require Export sts saved_prop.
+From program_logic Require Import hoare.
 From heap_lang Require Export derived heap wp_tactics notation.
 Import uPred.
 
@@ -103,8 +104,8 @@ Section proof.
   Local Notation iProp := (iPropG heap_lang Σ).
 
   Definition waiting (P : iProp) (I : gset gname) : iProp :=
-    (∃ R : gname → iProp, ▷(P -★ Π★{set I} (λ i, R i)) ★
-                             Π★{set I} (λ i, saved_prop_own i (R i)))%I.
+    (∃ Ψ : gname → iProp, ▷(P -★ Π★{set I} (λ i, Ψ i)) ★
+                             Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I.
 
   Definition ress (I : gset gname) : iProp :=
     (Π★{set I} (λ i, ∃ R, saved_prop_own i R ★ ▷R))%I.
@@ -119,13 +120,30 @@ Section proof.
   Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
     (heap_ctx heapN ★ sts_ctx γ N (barrier_inv l P))%I.
 
+  Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
+  Proof.
+    move=>? ? EQ. rewrite /barrier_ctx. apply sep_ne; first done. apply sts_ctx_ne.
+    move=>[p I]. rewrite /barrier_inv. destruct p; last done.
+    rewrite /waiting. by setoid_rewrite EQ.
+  Qed.
+
   Definition send (l : loc) (P : iProp) : iProp :=
     (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.
 
+  Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
+  Proof. (* TODO: This really ought to be doable by an automatic tactic. it is just application of already regostered congruence lemmas. *)
+    move=>? ? EQ. rewrite /send. apply exist_ne=>γ. by rewrite EQ.
+  Qed.
+
   Definition recv (l : loc) (R : iProp) : iProp :=
     (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
         saved_prop_own i Q ★ ▷(Q -★ R))%I.
 
+  Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
+  Proof.
+    move=>? ? EQ. rewrite /send. do 4 apply exist_ne=>?. by rewrite EQ.
+  Qed.
+
   Lemma newchan_spec (P : iProp) (Φ : val → iProp) :
     (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l))
     ⊑ wp ⊤ (newchan '()) Φ.
@@ -229,3 +247,35 @@ Section proof.
   Qed.
 
 End proof.
+
+Section spec.
+  Context {Σ : iFunctorG}.
+  Context `{heapG Σ}.
+  Context `{stsG heap_lang Σ barrier_proto.sts}.
+  Context `{savedPropG heap_lang Σ}.
+
+  Local Notation iProp := (iPropG heap_lang Σ).
+
+  (* TODO: Maybe notation for LocV (and Loc)? *)
+  Lemma barrier_spec (heapN N : namespace) :
+    heapN ⊥ N →
+    ∃ (recv send : loc -> iProp -n> iProp),
+      (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() @ ⊤ {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧
+      (∀ l P, {{ send l P ★ P }} signal (LocV l) @ ⊤ {{ λ _, True }}) ∧
+      (∀ l P, {{ recv l P }} wait (LocV l) @ ⊤ {{ λ _, P }}) ∧
+      (∀ l P Q, {{ recv l (P ★ Q) }} Skip @ ⊤ {{ λ _, recv l P ★ recv l Q }}) ∧
+      (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)).
+  Proof.
+    intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)).
+    split_ands; cbn.
+    - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec.
+      rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l.
+      apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id.
+      done.
+    - intros. apply ht_alt. rewrite -signal_spec; first by rewrite right_id. done.
+    - admit.
+    - admit.
+    - intros. apply recv_strengthen.
+  Abort.
+
+End spec.

program_logic/ghost_ownership.v

@@ -80,7 +80,7 @@ Proof.
   by destruct inG_prf.
 Qed.
 Lemma own_valid_r γ a : own γ a ⊑ (own γ a ★ ✓ a).
-Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.
+Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊑ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).

program_logic/hoare.v

@@ -31,7 +31,7 @@ Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
 
 Lemma ht_alt E P Φ e : (P ⊑ wp E e Φ) → {{ P }} e @ E {{ Φ }}.
 Proof.
-  intros; rewrite -{1}always_const. apply (always_intro _ _), impl_intro_l.
+  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
   by rewrite always_const right_id.
 Qed.
 
@@ -43,7 +43,7 @@ Lemma ht_vs E P P' Φ Φ' e :
   ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
   ⊑ {{ P }} e @ E {{ Φ }}.
 Proof.
-  apply (always_intro _ _), impl_intro_l.
+  apply: always_intro. apply impl_intro_l.
   rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
   rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
   rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ); apply pvs_mono, wp_mono=> v.
@@ -55,7 +55,7 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   ((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ ∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊑ {{ P }} e @ E1 {{ Φ }}.
 Proof.
-  intros ??; apply (always_intro _ _), impl_intro_l.
+  intros ??; apply: always_intro. apply impl_intro_l.
   rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
   rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
   rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
@@ -66,7 +66,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
   ({{ P }} e @ E {{ Φ }} ∧ ∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
   ⊑ {{ P }} K e @ E {{ Φ' }}.
 Proof.
-  intros; apply (always_intro _ _), impl_intro_l.
+  intros; apply: always_intro. apply impl_intro_l.
   rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
   rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
   by rewrite (forall_elim v) /ht always_elim impl_elim_r.

program_logic/hoare_lifting.v

@@ -26,7 +26,7 @@ Lemma ht_lift_step E1 E2
     {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})
   ⊑ {{ P }} e1 @ E2 {{ Ψ }}.
 Proof.
-  intros ?? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
+  intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
   rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
   rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
   rewrite always_and_sep_r -assoc; apply sep_mono; first done.
@@ -62,8 +62,8 @@ Proof.
   apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
   apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
   apply and_intro; [|apply and_intro; [|done]].
-  - rewrite -vs_impl; apply (always_intro _ _),impl_intro_l; rewrite and_elim_l.
-    rewrite !assoc; apply sep_mono; last done.
+  - rewrite -vs_impl; apply: always_intro. apply impl_intro_l.
+    rewrite and_elim_l !assoc; apply sep_mono; last done.
     rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
     by repeat apply and_intro; try apply const_intro.
   - apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
@@ -82,7 +82,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
     {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})
   ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
-  intros ? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
+  intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
   rewrite -(wp_lift_pure_step E φ _ e1) //.
   rewrite (later_intro (∀ _, _)) -later_and; apply later_mono.
   apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
@@ -110,11 +110,11 @@ Proof.
   intros ? Hsafe Hdet.
   rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
   apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
-  - apply (always_intro' _ _), impl_intro_l.
+  - apply: always_intro. apply impl_intro_l.
     rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
     by rewrite /ht always_elim impl_elim_r.
   - destruct ef' as [e'|]; simpl; [|by apply const_intro].
-    apply (always_intro _ _), impl_intro_l.
+    apply: always_intro. apply impl_intro_l.
     rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
     by rewrite /= /ht always_elim impl_elim_r.
 Qed.

program_logic/invariants.v

@@ -21,7 +21,7 @@ Implicit Types P Q R : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
 Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
-Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed.
+Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
 
 Global Instance inv_always_stable N P : AlwaysStable (inv N P).
 Proof. rewrite /inv; apply _. Qed.

program_logic/resources.v

@@ -40,7 +40,7 @@ Proof. by destruct 1. Qed.
 Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
 Proof. by destruct 1. Qed.
 Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ Σ A).
-Proof. destruct 1; apply (timeless _), dist_le with n; auto with lia. Qed.
+Proof. destruct 1; apply: timeless; apply dist_le with n; auto with lia. Qed.
 Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ Σ A).
 Proof. by destruct 1; unfold_leibniz. Qed.
 Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
@@ -69,7 +69,7 @@ Qed.
 Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
 Global Instance res_timeless r :
   Timeless (wld r) → Timeless (gst r) → Timeless r.
-Proof. by destruct 3; constructor; try apply (timeless _). Qed.
+Proof. by destruct 3; constructor; try apply: timeless. Qed.
 
 Instance res_op : Op (res Λ Σ A) := λ r1 r2,
   Res (wld r1 ⋅ wld r2) (pst r1 ⋅ pst r2) (gst r1 ⋅ gst r2).
@@ -157,7 +157,7 @@ Lemma lookup_wld_op_r n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
 Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
 Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
-Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
+Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
 
 (** Internalized properties *)
 Lemma res_equivI {M} r1 r2 :

program_logic/viewshifts.v

@@ -24,7 +24,7 @@ Implicit Types N : namespace.
 
 Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P ={E1,E2}=> Q.
 Proof.
-  intros; rewrite -{1}always_const. apply (always_intro _ _), impl_intro_l.
+  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
   by rewrite always_const right_id.
 Qed.
 
@@ -51,7 +51,7 @@ Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
 Lemma vs_transitive E1 E2 E3 P Q R :
   E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊑ (P ={E1,E3}=> R).
 Proof.
-  intros; rewrite -always_and; apply (always_intro _ _), impl_intro_l.
+  intros; rewrite -always_and; apply: always_intro. apply impl_intro_l.
   rewrite always_and assoc (always_elim (P → _)) impl_elim_r.
   by rewrite pvs_impl_r; apply pvs_trans.
 Qed.
@@ -91,7 +91,7 @@ Lemma vs_open_close N E P Q R :
   nclose N ⊆ E →
   (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).
 Proof.
-  intros; apply (always_intro _ _), impl_intro_l.
+  intros; apply: always_intro. apply impl_intro_l.
   rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
   eapply pvs_open_close; [by eauto with I..|].
   rewrite sep_elim_r. apply wand_intro_l.