Merge branch 'master' into gen_proofmode

CHANGELOG.md

@@ -3,6 +3,12 @@ way the logic is used on paper.  We also mention some significant changes in the
 Coq development, but not every API-breaking change is listed.  Changes marked
 `[#]` still need to be ported to the Iris Documentation LaTeX file(s).
 
+## Iris master
+
+Changes in Coq:
+
+* Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
+
 ## Iris 3.1.0 (released 2017-12-19)
 
 Changes in and extensions of the theory:

opam

@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { >= "8.7.1" & < "8.8~" | (= "dev") }
-  "coq-stdpp" { (= "1.1.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-01-13.0") | (= "dev") }
 ]

theories/algebra/deprecated.v

@@ -14,7 +14,7 @@ Local Arguments op _ _ _ !_ /.
 Local Arguments pcore _ _ !_ /.
 
 (* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type := 
+Inductive dec_agree (A : Type) : Type :=
   | DecAgree : A → dec_agree A
   | DecAgreeBot : dec_agree A.
 Arguments DecAgree {_} _.

theories/algebra/dra.v

@@ -22,7 +22,7 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   mixin_dra_core_disjoint_l x : ✓ x → core x ## x;
   mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
   mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_mono x y : 
+  mixin_dra_core_mono x y :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z
 }.
 Structure draT := DraT {
@@ -81,7 +81,7 @@ Section dra_mixin.
   Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
   Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
   Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_mono x y : 
+  Lemma dra_core_mono x y :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z.
   Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
 End dra_mixin.
@@ -209,7 +209,7 @@ Proof.
     assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
     split; first done. exists (to_validity z). split; first split.
     + intros _. simpl. by split_and!.
-    + intros _. setoid_subst. by apply dra_op_valid. 
+    + intros _. setoid_subst. by apply dra_op_valid.
     + intros _. rewrite /= EQ //.
 Qed.
 *)

theories/algebra/functions.v

@@ -8,7 +8,7 @@ Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Instance: Params (@ofe_fun_insert) 5.
 
-Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT} 
+Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT}
   (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
 Instance: Params (@ofe_fun_singleton) 5.
 

theories/algebra/ofe.v

@@ -7,7 +7,7 @@ Set Primitive Projections.
     category, and mathematically speaking, the entire development lives
     in this category. However, we will generally prefer to work with raw
     Coq functions plus some registered Proper instances for non-expansiveness.
-    This makes writing such functions much easier. It turns out that it many 
+    This makes writing such functions much easier. It turns out that it many
     cases, we do not even need non-expansiveness.
 *)
 

theories/algebra/sts.v

@@ -311,7 +311,7 @@ Proof. done. Qed.
 Lemma sts_frag_up_valid s T : ✓ sts_frag_up s T ↔ tok s ## T.
 Proof.
   split.
-  - move=>/sts_frag_valid [H _]. apply H, elem_of_up. 
+  - move=>/sts_frag_valid [H _]. apply H, elem_of_up.
   - intros. apply sts_frag_valid; split. by apply closed_up. set_solver.
 Qed.
 

theories/base_logic/base_logic.v

@@ -140,6 +140,9 @@ Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
 Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 
+Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
+Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+
 Global Instance is_except_0_bupd P : IsExcept0 P → IsExcept0 (|==> P).
 Proof.
   rewrite /IsExcept0=> HP.

theories/base_logic/double_negation.v

@@ -229,7 +229,7 @@ Proof.
   revert P.
   induction k; intros P.
   - rewrite //= ?right_id. apply wand_intro_l.
-    rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r. 
+    rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r.
   - rewrite {2}(nnupd_k_unfold k P).
     apply and_intro.
     * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
@@ -292,9 +292,9 @@ Qed.
 End classical.
 
 (* We might wonder whether we can prove an adequacy lemma for nnupd. We could combine
-   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but 
+   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but
    this would rely on the classical axiom we needed to prove the equivalence! Can
-   we establish adequacy without axioms? Unfortunately not, because adequacy for 
+   we establish adequacy without axioms? Unfortunately not, because adequacy for
    nnupd would imply double negation elimination, which is classical: *)
 
 Lemma nnupd_dne φ: (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I.
@@ -327,7 +327,7 @@ Proof.
     intros Hf3. eapply Hf3; eauto.
     intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
     assert (n' < S k ∨ n' = S k) as [|] by omega.
-    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall. 
+    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
       eapply Hsmall; eauto.
     * subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
   - intros k P x Hx. rewrite ?Nat_iter_S_r.

theories/base_logic/lib/fancy_updates.v

@@ -204,17 +204,18 @@ Section proofmode_classes.
   Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
   Proof. rewrite /FromModal. apply fupd_intro. Qed.
 
-  (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
-     it is not taken when the first parameter is not specified (in
-     spec. patterns). *)
   Global Instance elim_modal_bupd_fupd E1 E2 P Q :
-    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
+    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
   Proof.
     by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
   Qed.
   Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
     ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
+
+  Global Instance add_modal_fupd E1 E2 P Q :
+    AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
 Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.

theories/base_logic/lib/namespaces.v

@@ -84,7 +84,7 @@ End namespace.
 
 (* The hope is that registering these will suffice to solve most goals
 of the forms:
-- [N1 ## N2] 
+- [N1 ## N2]
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Create HintDb ndisj.

theories/base_logic/lib/sts.v

@@ -82,7 +82,7 @@ Section sts.
     sts_own γ s1 T ==∗ sts_own γ s2 T.
   Proof.
     intros ??. apply own_update, sts_update_frag_up; [|done..].
-    intros Hdisj. apply sts.closed_up. done. 
+    intros Hdisj. apply sts.closed_up. done.
   Qed.
 
   Lemma sts_own_weaken_tok γ s T1 T2 :

theories/bi/tactics.v

@@ -62,7 +62,7 @@ Module bi_reflection. Section bi_reflection.
     match e with
     | EEmp => None
     | EVar n' => if decide (n = n') then Some EEmp else None
-    | ESep e1 e2 => 
+    | ESep e1 e2 =>
        match cancel_go n e1 with
        | Some e1' => Some (ESep e1' e2)
        | None => ESep e1 <$> cancel_go n e2

theories/heap_lang/lang.v

@@ -276,7 +276,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
-  | StoreLCtx e2 => Store e e2 
+  | StoreLCtx e2 => Store e e2
   | StoreRCtx v1 => Store (of_val v1) e
   | CasLCtx e1 e2 => CAS e e1 e2
   | CasMCtx v0 e2 => CAS (of_val v0) e e2
@@ -365,11 +365,11 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
      head_step (App (Rec f x e1) e2) σ e' σ []
   | UnOpS op e v v' σ :
      to_val e = Some v →
-     un_op_eval op v = Some v' → 
+     un_op_eval op v = Some v' →
      head_step (UnOp op e) σ (of_val v') σ []
   | BinOpS op e1 e2 v1 v2 v' σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     bin_op_eval op v1 v2 = Some v' → 
+     bin_op_eval op v1 v2 = Some v' →
      head_step (BinOp op e1 e2) σ (of_val v') σ []
   | IfTrueS e1 e2 σ :
      head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []

theories/heap_lang/lib/counter.v

@@ -55,7 +55,7 @@ Section mono_proof.
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_valid_discrete_2.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply auth_update, (mnat_local_update _ _ (S c)); auto. } 
+      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
       wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.

theories/heap_lang/lib/ticket_lock.v

@@ -94,7 +94,7 @@ Section proof.
       + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
         iModIntro. wp_let. wp_op. case_bool_decide; [|done].
-        wp_if. 
+        wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
@@ -129,7 +129,7 @@ Section proof.
       iModIntro. wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
-      + by iNext. 
+      + by iNext.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }

theories/heap_lang/proofmode.v

@@ -10,7 +10,7 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
 
-Ltac wp_expr_eval t :=
+Tactic Notation "wp_expr_eval" tactic(t) :=
   try iStartProof;
   try (eapply tac_wp_expr_eval; [t; reflexivity|]).
 
@@ -33,7 +33,10 @@ Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
 
-Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
+Ltac wp_value_head :=
+  eapply tac_wp_value;
+    [apply _
+    |iEval (lazy beta; simpl of_val)].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;

theories/program_logic/weakestpre.v

@@ -236,7 +236,7 @@ Proof.
   iSplitL "He2"; first by iApply ("IH" with "He2"). iClear "Hred Hstep".
   induction efs as [|ef efs IH]; first by iApply big_sepL_nil.
   rewrite !big_sepL_cons. iDestruct "Hefs" as "(Hef & Hefs)".
-  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH. 
+  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH.
 Qed.
 
 Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
@@ -392,10 +392,13 @@ Section proofmode_classes.
     ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
     ElimModal (|={E1,E2}=> P) P
-            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
+
+  Global Instance add_modal_fupd_wp s E e P Φ :
+    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 End proofmode_classes.

theories/proofmode/base.v

@@ -27,7 +27,7 @@ Definition ascii_beq (x y : ascii) : bool :=
     beq x5 y5 && beq x6 y6 && beq x7 y7 && beq x8 y8.
 
 Fixpoint string_beq (s1 s2 : string) : bool :=
-  match s1, s2 with 
+  match s1, s2 with
   | "", "" => true
   | String a1 s1, String a2 s2 => ascii_beq a1 a2 && string_beq s1 s2
   | _, _ => false

theories/proofmode/class_instances.v

@@ -706,7 +706,7 @@ Proof.
   rewrite /ElimModal=> H. apply wand_intro_r.
   by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
 Qed.
-Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → PROP) :
+Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → PROP) :
   (∀ x, ElimModal P P' (Φ x) (Ψ x)) → ElimModal P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
@@ -716,6 +716,19 @@ Proof.
   rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
+(* AddModal *)
+Global Instance add_modal_wand P P' Q R :
+  AddModal P P' Q → AddModal P P' (R -∗ Q).
+Proof.
+  rewrite /AddModal=> H. apply wand_intro_r.
+  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
+Qed.
+Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
+Proof.
+  rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
+Qed.
+
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
 Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.