### Use symbol ∗ for separating conjunction.

```The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to
conventional practise and matches the symbol we use on paper.```
parent 6cb76aaa
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -13,14 +13,14 @@ Notation "▷^ n P" := (uPred_laterN n P) format "▷^ n P") : uPred_scope. Definition uPred_nnupd {M} (P: uPred M) : uPred M := ∀ n, (P -★ ▷^n False) -★ ▷^n False. ∀ n, (P -∗ ▷^n False) -∗ ▷^n False. Notation "|=n=> Q" := (uPred_nnupd Q) (at level 99, Q at level 200, format "|=n=> Q") : uPred_scope. Notation "P =n=> Q" := (P ⊢ |=n=> Q) (at level 99, Q at level 200, only parsing) : C_scope. Notation "P =n=★ Q" := (P -★ |=n=> Q)%I (at level 99, Q at level 200, format "P =n=★ Q") : uPred_scope. Notation "P =n=∗ Q" := (P -∗ |=n=> Q)%I (at level 99, Q at level 200, format "P =n=∗ Q") : uPred_scope. (* Our goal is to prove that: (1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris ... ... @@ -62,9 +62,9 @@ Qed. are used throughout Iris hold for nnupd. In fact, the first three properties that follow hold for any modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation here is slightly different, because nnupd is of the form ∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly. ∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly. *) ... ... @@ -77,7 +77,7 @@ Proof. rewrite /uPred_nnupd (forall_elim n). apply wand_elim_r. Qed. Lemma nnupd_frame_r P R : (|=n=> P) ★ R =n=> P ★ R. Lemma nnupd_frame_r P R : (|=n=> P) ∗ R =n=> P ∗ R. Proof. apply forall_intro=>n. apply wand_intro_r. rewrite (comm _ P) -wand_curry. ... ... @@ -106,7 +106,7 @@ Qed. (* However, the transitivity property seems to be much harder to prove. This is surprising, because transitivity does hold for modalities of the form (- -★ Q) -★ Q. What goes wrong when we quantify modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify now over n? *) ... ... @@ -115,7 +115,7 @@ Proof. rewrite /uPred_nnupd. apply forall_intro=>a. apply wand_intro_l. rewrite (forall_elim a). rewrite (nnupd_intro (P -★ _)). rewrite (nnupd_intro (P -∗ _)). rewrite /uPred_nnupd. (* Oops -- the exponents of the later modality don't match up! *) Abort. ... ... @@ -123,9 +123,9 @@ Abort. (* Instead, we will need to prove this in the model. We start by showing that nnupd is the limit of a the following sequence: (- -★ False) - ★ False, (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, (- -★ ▷^2 False) - ★ ▷^2 False ∧ (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, (- -∗ False) - ∗ False, (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False, (- -∗ ▷^2 False) - ∗ ▷^2 False ∧ (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False, ... Then, it is easy enough to show that each of the uPreds in this sequence ... ... @@ -134,7 +134,7 @@ Abort. (* The definition of the sequence above: *) Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M := ((P -★ ▷^k False) -★ ▷^k False) ∧ ((P -∗ ▷^k False) -∗ ▷^k False) ∧ match k with O => True | S k' => uPred_nnupd_k k' P ... ... @@ -155,7 +155,7 @@ Proof. rewrite (forall_elim (S k)) //=. Qed. Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ★ (P -★ (▷^n False)) ⊢ (▷^n False))%I. Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ∗ (P -∗ (▷^n False)) ⊢ (▷^n False))%I. Proof. induction k. - inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l. ... ... @@ -165,10 +165,10 @@ Proof. Qed. Lemma nnupd_k_unfold k P: (|=n=>_(S k) P) ⊣⊢ ((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P). (|=n=>_(S k) P) ⊣⊢ ((P -∗ (▷^(S k) False)) -∗ (▷^(S k) False)) ∧ (|=n=>_k P). Proof. done. Qed. Lemma nnupd_k_unfold' k P n x: (|=n=>_(S k) P)%I n x ↔ (((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x. (|=n=>_(S k) P)%I n x ↔ (((P -∗ (▷^(S k) False)) -∗ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x. Proof. done. Qed. Lemma nnupd_k_weaken k P: (|=n=>_(S k) P) ⊢ |=n=>_k P. ... ... @@ -238,13 +238,13 @@ 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. rewrite nnupd_k_unfold. rewrite and_elim_l. apply wand_intro_l. rewrite {1}(nnupd_k_intro (S k) (P -★ ▷^(S k) (False)%I)). rewrite {1}(nnupd_k_intro (S k) (P -∗ ▷^(S k) (False)%I)). rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r. * do 2 rewrite nnupd_k_weaken //. Qed. ... ...
 ... ... @@ -21,7 +21,7 @@ Section definitions. Definition auth_own (a : A) : iProp Σ := own γ (◯ a). Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ := (∃ t, own γ (● f t) ★ φ t)%I. (∃ t, own γ (● f t) ∗ φ t)%I. Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ := inv N (auth_inv f φ). ... ... @@ -69,7 +69,7 @@ Section auth. Implicit Types t u : T. Implicit Types γ : gname. Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b. Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ∗ auth_own γ b. Proof. by rewrite /auth_own -own_op auth_frag_op. Qed. Global Instance from_sep_auth_own γ a b1 b2 : ... ... @@ -92,7 +92,7 @@ Section auth. Proof. intros a1 a2. apply auth_own_mono. Qed. Lemma auth_alloc_strong N E t (G : gset gname) : ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. iIntros (?) "Hφ". rewrite /auth_own /auth_ctx. iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done. ... ... @@ -103,19 +103,19 @@ Section auth. Qed. Lemma auth_alloc N E t : ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. iIntros (?) "Hφ". iMod (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto. Qed. Lemma auth_empty γ : True ==★ auth_own γ ∅. Lemma auth_empty γ : True ==∗ auth_own γ ∅. Proof. by rewrite /auth_own -own_empty. Qed. Lemma auth_acc E γ a : ▷ auth_inv γ f φ ★ auth_own γ a ={E}=★ ∃ t, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b. ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t, ■ (a ≼ f t) ∗ ▷ φ t ∗ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ∗ ▷ φ u ={E}=∗ ▷ auth_inv γ f φ ∗ auth_own γ b. Proof. iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own. iDestruct "Hinv" as (t) "[>Hγa Hφ]". ... ... @@ -129,9 +129,9 @@ Section auth. Lemma auth_open E N γ a : nclose N ⊆ E → auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=★ ∃ t, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b. auth_ctx γ N f φ ∗ auth_own γ a ={E,E∖N}=∗ ∃ t, ■ (a ≼ f t) ∗ ▷ φ t ∗ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ∗ ▷ φ u ={E∖N,E}=∗ auth_own γ b. Proof. iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose". (* The following is essentially a very trivial composition of the accessors ... ...
 ... ... @@ -22,15 +22,15 @@ Section box_defs. own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))). Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ := (∃ b, box_own_auth γ (● Excl' b) ★ box_own_prop γ P ★ if b then P else True)%I. (∃ b, box_own_auth γ (● Excl' b) ∗ box_own_prop γ P ∗ if b then P else True)%I. Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ := inv N (slice_inv γ P). Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ := (∃ Φ : slice_name → iProp Σ, ▷ (P ≡ [★ map] γ ↦ b ∈ f, Φ γ) ★ [★ map] γ ↦ b ∈ f, box_own_auth γ (◯ Excl' b) ★ box_own_prop γ (Φ γ) ★ ▷ (P ≡ [∗ map] γ ↦ b ∈ f, Φ γ) ∗ [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯ Excl' b) ∗ box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I. End box_defs. ... ... @@ -55,22 +55,22 @@ Global Instance slice_persistent γ P : PersistentP (slice N γ P). Proof. apply _. Qed. Lemma box_own_auth_agree γ b1 b2 : box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2. box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2. Proof. rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_l. by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete. Qed. Lemma box_own_auth_update γ b1 b2 b3 : box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ==★ box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3). box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ==∗ box_own_auth γ (● Excl' b3) ∗ box_own_auth γ (◯ Excl' b3). Proof. rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done. by apply auth_update, option_local_update, exclusive_local_update. Qed. Lemma box_own_agree γ Q1 Q2 : (box_own_prop γ Q1 ★ box_own_prop γ Q2) ⊢ ▷ (Q1 ≡ Q2). (box_own_prop γ Q1 ∗ box_own_prop γ Q2) ⊢ ▷ (Q1 ≡ Q2). Proof. rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r. rewrite option_validI /= agree_validI agree_equivI later_equivI /=. ... ... @@ -86,8 +86,8 @@ Proof. Qed. Lemma box_insert f P Q : ▷ box N f P ={N}=★ ∃ γ, f !! γ = None ★ slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). ▷ box N f P ={N}=∗ ∃ γ, f !! γ = None ∗ slice N γ Q ∗ ▷ box N (<[γ:=false]> f) (Q ∗ P). Proof. iDestruct 1 as (Φ) "[#HeqP Hf]". iMod (own_alloc_strong (● Excl' false ⋅ ◯ Excl' false, ... ... @@ -100,17 +100,17 @@ Proof. iModIntro; iExists γ; repeat iSplit; auto. iNext. iExists (<[γ:=Q]> Φ); iSplit. - iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'. - rewrite (big_sepM_fn_insert (λ _ _ P', _ ★ _ _ P' ★ _ _ (_ _ P')))%I //. - rewrite (big_sepM_fn_insert (λ _ _ P', _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //. iFrame; eauto. Qed. Lemma box_delete f P Q γ : f !! γ = Some false → slice N γ Q ★ ▷ box N f P ={N}=★ ∃ P', ▷ ▷ (P ≡ (Q ★ P')) ★ ▷ box N (delete γ f) P'. slice N γ Q ∗ ▷ box N f P ={N}=∗ ∃ P', ▷ ▷ (P ≡ (Q ∗ P')) ∗ ▷ box N (delete γ f) P'. Proof. iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iExists ([★ map] γ'↦_ ∈ delete γ f, Φ γ')%I. iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I. iInv N as (b) "(Hγ & #HγQ &_)" "Hclose". iApply fupd_trans_frame; iFrame "Hclose"; iModIntro; iNext. iDestruct (big_sepM_delete _ f _ false with "Hf") ... ... @@ -125,7 +125,7 @@ Qed. Lemma box_fill f γ P Q : f !! γ = Some false → slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=★ ▷ box N (<[γ:=true]> f) P. slice N γ Q ∗ ▷ Q ∗ ▷ box N f P ={N}=∗ ▷ box N (<[γ:=true]> f) P. Proof. iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]". iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose". ... ... @@ -143,7 +143,7 @@ Qed. Lemma box_empty f P Q γ : f !! γ = Some true → slice N γ Q ★ ▷ box N f P ={N}=★ ▷ Q ★ ▷ box N (<[γ:=false]> f) P. slice N γ Q ∗ ▷ box N f P ={N}=∗ ▷ Q ∗ ▷ box N (<[γ:=false]> f) P. Proof. iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose". ... ... @@ -160,7 +160,7 @@ Proof. iFrame; eauto. Qed. Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=★ box N (const true <\$> f) P. Lemma box_fill_all f P Q : box N f P ∗ ▷ P ={N}=∗ box N (const true <\$> f) P. Proof. iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iExists Φ; iSplitR; first by rewrite big_sepM_fmap. ... ... @@ -177,11 +177,11 @@ Qed. Lemma box_empty_all f P Q : map_Forall (λ _, (true =)) f → box N f P ={N}=★ ▷ P ★ box N (const false <\$> f) P. box N f P ={N}=∗ ▷ P ∗ box N (const false <\$> f) P. Proof. iDestruct 1 as (Φ) "[#HeqP Hf]". iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★ box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]". iAssert ([∗ map] γ↦b ∈ f, ▷ Φ γ ∗ box_own_auth γ (◯ Excl' false) ∗ box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]". { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf". iAlways; iIntros (γ b ?) "(Hγ' & #\$ & #\$)". assert (true = b) as <- by eauto. ... ...
 ... ... @@ -32,19 +32,19 @@ Section proofs. Proof. rewrite /cinv; apply _. Qed. Lemma cinv_own_op γ q1 q2 : cinv_own γ q1 ★ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2). cinv_own γ q1 ∗ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2). Proof. by rewrite /cinv_own own_op. Qed. Lemma cinv_own_half γ q : cinv_own γ (q/2) ★ cinv_own γ (q/2) ⊣⊢ cinv_own γ q. Lemma cinv_own_half γ q : cinv_own γ (q/2) ∗ cinv_own γ (q/2) ⊣⊢ cinv_own γ q. Proof. by rewrite cinv_own_op Qp_div_2. Qed. Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ★ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp. Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ∗ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp. Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed. Lemma cinv_own_1_l γ q : cinv_own γ 1 ★ cinv_own γ q ⊢ False. Lemma cinv_own_1_l γ q : cinv_own γ 1 ∗ cinv_own γ q ⊢ False. Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed. Lemma cinv_alloc E N P : ▷ P ={E}=★ ∃ γ, cinv N γ P ★ cinv_own γ 1. Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1. Proof. rewrite /cinv /cinv_own. iIntros "HP". iMod (own_alloc 1%Qp) as (γ) "H1"; first done. ... ... @@ -52,7 +52,7 @@ Section proofs. Qed. Lemma cinv_cancel E N γ P : nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=★ ▷ P. nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ 1 ={E}=∗ ▷ P. Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto. ... ... @@ -61,7 +61,7 @@ Section proofs. Lemma cinv_open E N γ p P : nclose N ⊆ E → cinv N γ P ⊢ cinv_own γ p ={E,E∖N}=★ ▷ P ★ cinv_own γ p ★ (▷ P ={E∖N,E}=★ True). cinv N γ P ⊢ cinv_own γ p ={E,E∖N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖N,E}=∗ True). Proof. rewrite /cinv. iIntros (?) "#Hinv Hγ". iInv N as "[\$|>Hγ']" "Hclose". ... ...
 ... ... @@ -13,13 +13,13 @@ Module savedprop. Section savedprop. Context (sprop : Type) (saved : sprop → iProp → iProp). Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P). Hypothesis sprop_alloc_dep : ∀ (P : sprop → iProp), True ==★ (∃ i, saved i (P i)). ∀ (P : sprop → iProp), True ==∗ (∃ i, saved i (P i)). Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q). (** A bad recursive reference: "Assertion with name [i] does not hold" *) Definition A (i : sprop) : iProp := ∃ P, ¬ P ★ saved i P. Definition A (i : sprop) : iProp := ∃ P, ¬ P ∗ saved i P. Lemma A_alloc : True ==★ ∃ i, saved i (A i). Lemma A_alloc : True ==∗ ∃ i, saved i (A i). Proof. by apply sprop_alloc_dep. Qed. Lemma saved_NA i : saved i (A i) ⊢ ¬ A i. ... ... @@ -63,7 +63,7 @@ Module inv. Section inv. Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P. Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q. Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P. Hypothesis fupd_frame_l : ∀ E P Q, P ★ fupd E Q ⊢ fupd E (P ★ Q). Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q). Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P. (** We have invariants *) ... ... @@ -71,7 +71,7 @@ Module inv. Section inv. Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P). Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P). Hypothesis inv_open : ∀ i P Q R, (P ★ Q ⊢ fupd M0 (P ★ R)) → (inv i P ★ Q ⊢ fupd M1 R). ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R). (* We have tokens for a little "two-state STS": [start] -> [finish]. state. [start] also asserts the exact state; it is only ever owned by the ... ... @@ -88,15 +88,15 @@ Module inv. Section inv. Hypothesis sts_alloc : True ⊢ fupd M0 (∃ γ, start γ). Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ). Hypothesis finished_not_start : ∀ γ, start γ ★ finished γ ⊢ False. Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False. Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ. Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ. (** We assume that we cannot update to false. *) Hypothesis consistency : ¬ (True ⊢ fupd M1 False). (** Some general lemmas and proof mode compatibility. *) Lemma inv_open' i P R : inv i P ★ (P -★ fupd M0 (P ★ fupd M1 R)) ⊢ fupd M1 R. Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R. Proof. iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first. { iSplit; first done. iExact "HP". } ... ... @@ -110,7 +110,7 @@ Module inv. Section inv. intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono. Qed. Lemma fupd_frame_r E P Q : (fupd E P ★ Q) ⊢ fupd E (P ★ Q). Lemma fupd_frame_r E P Q : (fupd E P ∗ Q) ⊢ fupd E (P ∗ Q). Proof. by rewrite comm fupd_frame_l comm. Qed. Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q). ... ... @@ -130,18 +130,18 @@ Module inv. Section inv. (** Now to the actual counterexample. We start with a weird form of saved propositions. *) Definition saved (γ : gname) (P : iProp) : iProp := ∃ i, inv i (start γ ∨ (finished γ ★ □ P)). ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)). Global Instance saved_persistent γ P : PersistentP (saved γ P) := _. Lemma saved_alloc (P : gname → iProp) : True ⊢ fupd M1 (∃ γ, saved γ (P γ)). Proof. iIntros "". iMod (sts_alloc) as (γ) "Hs". iMod (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi". iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi". { auto. } iApply fupd_intro. by iExists γ, i. Qed. Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ fupd M1 (□ Q). Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q). Proof. iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". iApply (inv_open' i). iSplit; first done. ... ... @@ -162,8 +162,8 @@ Module inv. Section inv. Qed. (** And now we tie a bad knot. *) Notation "¬ P" := (□ (P -★ fupd M1 False))%I : uPred_scope. Definition A i : iProp := ∃ P, ¬P ★ saved i P. Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope. Definition A i : iProp := ∃ P, ¬P ∗ saved i P. Global Instance A_persistent i : PersistentP (A i) := _. Lemma A_alloc : True ⊢ fupd M1 (∃ i, saved i (A i)). ... ...
 ... ... @@ -9,7 +9,7 @@ Import uPred. Program Definition fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ := (wsat ★ ownE E1 ==★ ◇ (wsat ★ ownE E2 ★ P))%I. (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I. Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed. Definition fupd := proj1_sig fupd_aux. Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux. ... ... @@ -19,19 +19,19 @@ Instance: Params (@fupd) 4. Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) (at level 99, E1, E2 at level 50, Q at level 200, format "|={ E1 , E2 }=> Q") : uPred_scope. Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I (at level 99, E1,E2 at level 50, Q at level 200, format "P ={ E1 , E2 }=★ Q") : uPred_scope. Notation "P ={ E1 , E2 }=★ Q" := (P ⊢ |={E1,E2}=> Q) format "P ={ E1 , E2 }=∗ Q") : uPred_scope. Notation "P ={ E1 , E2 }=∗ Q" := (P ⊢ |={E1,E2}=> Q) (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope. Notation "|={ E }=> Q" := (fupd E E Q) (at level 99, E at level 50, Q at level 200, format "|={ E }=> Q") : uPred_scope. Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I (at level 99, E at level 50, Q at level 200, format "P ={ E }=★ Q") : uPred_scope. Notation "P ={ E }=★ Q" := (P ⊢ |={E}=> Q) format "P ={ E }=∗ Q") : uPred_scope. Notation "P ={ E }=∗ Q" := (P ⊢ |={E}=> Q) (at level 99, E at level 50, Q at level 200, only parsing) : C_scope. Section fupd. ... ... @@ -50,26 +50,26 @@ Proof. by iIntros "\$ (\$ & \$ & HE) !> !> [\$ \$] !> !>" . Qed. Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=★ P. Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P. Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed. Lemma bupd_fupd E P : (|==> P) ={E}=★ P. Lemma bupd_fupd E P : (|==> P) ={E}=∗ P. Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [\$ \$] !> !>". Qed. Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=★ Q. Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=∗ Q. Proof. rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP". Qed. Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=★ P. Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=∗ P. Proof. rewrite fupd_eq /fupd_def. iIntros "HP HwE". iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame. Qed. Lemma fupd_mask_frame_r' E1 E2 Ef P : E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=★ P. E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P. Proof. intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)". iMod ("Hvs" with "[Hw HE1]") as ">(\$ & HE2 & HP)"; first by iFrame. ... ... @@ -77,7 +77,7 @@ Proof. iIntros "!> !>". by iApply "HP". Qed. Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q. Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q. Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP \$]". Qed. (** * Derived rules *) ... ... @@ -87,50 +87,50 @@ Global Instance fupd_flip_mono' E1 E2 : Proper (flip (⊢) ==> flip (⊢)) (@fupd Σ _ E1 E2). Proof. intros P Q; apply fupd_mono. Qed. Lemma fupd_intro E P : P ={E}=★ P. Lemma fupd_intro E P : P ={E}=∗ P. Proof. iIntros "HP". by iApply bupd_fupd. Qed. Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True. Proof. exact: fupd_intro_mask. Qed. Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=★ P. Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P. Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed. Lemma fupd_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=★ P ★ Q. Lemma fupd_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ={E1,E2}=∗ P ∗ Q. Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed. Lemma fupd_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=★ Q. Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q. Proof. by rewrite fupd_frame_l wand_elim_l. Qed. Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=★ Q. Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q. Proof. by rewrite fupd_frame_r wand_elim_r. Qed. Lemma fupd_trans_frame E1 E2 E3 P Q : ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=★ P. ((Q ={E2,E3}=∗ True) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P. Proof. rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r. by rewrite fupd_frame_r left_id fupd_trans. Qed. Lemma fupd_mask_frame_r E1 E2 Ef P : E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=★ P. E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P. Proof. iIntros (?) "H". iApply fupd_mask_frame_r'; auto. iApply fupd_wand_r; iFrame "H"; eauto. Qed. Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=★ P. Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=∗ P. Proof. intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r. Qed. Lemma fupd_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=★ P ★ Q. Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q. Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed. Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) : ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=★ [★ map] k↦x ∈ m, Φ k x. ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x. Proof. apply (big_opM_forall (λ P Q, P ={E}=★ Q)); auto using fupd_intro. apply (big_opM_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP H