diff --git a/algebra/upred.v b/algebra/upred.v index a8fe0398abf3342910385840c277f2de42a4863b..878761a858704ccc5acaf0f347f3fafd310b51bc 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -307,6 +307,13 @@ Arguments uPred_always_if _ !_ _/. Notation "□? p P" := (uPred_always_if p P) (at level 20, p at level 0, P at level 20, format "□? p P"). +Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M := + Nat.iter n uPred_later P. +Instance: Params (@uPred_laterN) 2. +Notation "▷^ n P" := (uPred_laterN n P) + (at level 20, n at level 9, right associativity, + format "▷^ n P") : uPred_scope. + Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False). Arguments timelessP {_} _ {_}. @@ -437,7 +444,7 @@ Proof. intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|]. apply (HPQ n'); eauto using cmra_validN_S. Qed. -Global Instance later_proper : +Global Instance later_proper' : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _. Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M). Proof. @@ -460,10 +467,6 @@ Proof. Qed. Global Instance valid_proper {A : cmraT} : Proper ((≡) ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _. -Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). -Proof. unfold uPred_iff; solve_proper. Qed. -Global Instance iff_proper : - Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _. (** Introduction and elimination rules *) Lemma pure_intro φ P : φ → P ⊢ ■ φ. @@ -523,6 +526,11 @@ Proof. Qed. (* Derived logical stuff *) +Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). +Proof. unfold uPred_iff; solve_proper. Qed. +Global Instance iff_proper : + Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _. + Lemma False_elim P : False ⊢ P. Proof. by apply (pure_elim False). Qed. Lemma True_intro P : P ⊢ True. @@ -943,7 +951,10 @@ Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P. Proof. intros; rewrite -always_and_sep_l'; auto. Qed. Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ★ □ Q. Proof. intros; rewrite -always_and_sep_r'; auto. Qed. +Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P. +Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed. +(* Conditional always *) Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p). Proof. solve_proper. Qed. Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p). @@ -1004,6 +1015,9 @@ Proof. Qed. (* Later derived *) +Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q. +Proof. by intros ->. Qed. +Hint Resolve later_mono later_proper. Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M). Proof. intros P Q; apply later_mono. Qed. Global Instance later_flip_mono' : @@ -1012,18 +1026,69 @@ Proof. intros P Q; apply later_mono. Qed. Lemma later_True : ▷ True ⊣⊢ True. Proof. apply (anti_symm (⊢)); auto using later_intro. Qed. Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q. -Proof. - apply impl_intro_l; rewrite -later_and. - apply later_mono, impl_elim with P; auto. -Qed. +Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed. Lemma later_exist `{Inhabited A} (Φ : A → uPred M) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a). Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. Qed. Lemma later_wand P Q : ▷ (P -★ Q) ⊢ ▷ P -★ ▷ Q. -Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed. +Proof. apply wand_intro_r;rewrite -later_sep; eauto using wand_elim_l. Qed. Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q. Proof. by rewrite /uPred_iff later_and !later_impl. Qed. +(* n-times later *) +Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m). +Proof. induction m; simpl. by intros ???. solve_proper. Qed. +Global Instance laterN_proper m : + Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _. + +Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P. +Proof. done. Qed. +Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P. +Proof. induction n; simpl; auto. Qed. +Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P. +Proof. induction n1; simpl; auto. Qed. +Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P. +Proof. induction 1; simpl; by rewrite -?later_intro. Qed. + +Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q. +Proof. induction n; simpl; auto. Qed. +Lemma laterN_intro n P : P ⊢ ▷^n P. +Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed. +Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q. +Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed. +Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q. +Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed. +Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a). +Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed. +Lemma laterN_exist_1 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ (▷^n ∃ a, Φ a). +Proof. induction n as [|n IH]; simpl; rewrite ?later_exist_1; auto. Qed. +Lemma laterN_exist_2 `{Inhabited A} n (Φ : A → uPred M) : + (▷^n ∃ a, Φ a) ⊢ ∃ a, ▷^n Φ a. +Proof. induction n as [|n IH]; simpl; rewrite -?later_exist_2; auto. Qed. +Lemma laterN_sep n P Q : ▷^n (P ★ Q) ⊣⊢ ▷^n P ★ ▷^n Q. +Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed. + +Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@uPred_laterN M n). +Proof. intros P Q; apply laterN_mono. Qed. +Global Instance laterN_flip_mono' n : + Proper (flip (⊢) ==> flip (⊢)) (@uPred_laterN M n). +Proof. intros P Q; apply laterN_mono. Qed. +Lemma laterN_True n : ▷^n True ⊣⊢ True. +Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed. +Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q. +Proof. + apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono. +Qed. +Lemma laterN_exist n `{Inhabited A} (Φ : A → uPred M) : + ▷^n (∃ a, Φ a) ⊣⊢ (∃ a, ▷^n Φ a). +Proof. apply: anti_symm; eauto using laterN_exist_2, laterN_exist_1. Qed. +Lemma laterN_wand n P Q : ▷^n (P -★ Q) ⊢ ▷^n P -★ ▷^n Q. +Proof. + apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono. +Qed. +Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q. +Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed. + (* Own *) Lemma ownM_op (a1 a2 : M) : uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2. @@ -1193,6 +1258,8 @@ Global Instance valid_persistent {A : cmraT} (a : A) : Proof. by intros; rewrite /PersistentP always_valid. Qed. Global Instance later_persistent P : PersistentP P → PersistentP (▷ P). Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed. +Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P). +Proof. induction n; apply _. Qed. Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a). Proof. intros. by rewrite /PersistentP always_ownM. Qed. Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) : diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v index 221ca9b806b725b91727bb981ab7a9d573687ede..4c2617a7f09960df3b8926fb3318df376b1d8b6e 100644 --- a/heap_lang/lib/spawn.v +++ b/heap_lang/lib/spawn.v @@ -80,7 +80,7 @@ Proof. + iPvsIntro; iSplitL "Hl Hγ". { iNext. iExists _; iFrame; eauto. } wp_match. by iApply "Hv". - + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (@own_valid with "Hγ") as %[]. + + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[]. Qed. End proof. diff --git a/program_logic/auth.v b/program_logic/auth.v index 2c169450819a1259c20c058da946a28da790c579..ba098d733e1732ceb6d86d93e095ec1e612d2850 100644 --- a/program_logic/auth.v +++ b/program_logic/auth.v @@ -103,14 +103,14 @@ Section auth. iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own. iInv N as (a') "[Hγ Hφ]". iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ". - iDestruct (@own_valid with "#Hγ") as "Hvalid". + iDestruct (own_valid with "#Hγ") as "Hvalid". iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid". iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'. rewrite ->(left_id _ _) in Ha'; setoid_subst. iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ". { iApply "HΨ"; by iSplit. } iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)". - iPvs (@own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto. + iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto. iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ". iNext. iExists (b ⋅ af). by iFrame. Qed. diff --git a/program_logic/boxes.v b/program_logic/boxes.v index e81180b7981883bb0940fa9cacbb226e59f36fc8..793b69c51a7c49d081b691da5ac2ab3ee86c2a81 100644 --- a/program_logic/boxes.v +++ b/program_logic/boxes.v @@ -69,7 +69,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 : Proof. rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]". iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete. - iApply (@own_update with "Hγ"); apply prod_update; simpl; last reflexivity. + iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity. by apply auth_update_no_frame, option_local_update, exclusive_local_update. Qed. diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v index cd679ccdfbbe142c24487cdc4c060ef39ab91eab..92c4adc27d02c2e6a0f15e21c96fc69cf59ee700 100644 --- a/program_logic/ghost_ownership.v +++ b/program_logic/ghost_ownership.v @@ -82,6 +82,12 @@ Proof. Qed. End global. +Arguments own_valid {_ _ _} [_] _ _. +Arguments own_valid_l {_ _ _} [_] _ _. +Arguments own_valid_r {_ _ _} [_] _ _. +Arguments own_updateP {_ _ _} [_] _ _ _ _ _. +Arguments own_update {_ _ _} [_] _ _ _ _ _. + Section global_empty. Context `{i : inG Λ Σ (A:ucmraT)}. Implicit Types a : A. diff --git a/program_logic/sts.v b/program_logic/sts.v index 7152d178f7a8b05edf7b179e188792cac0a67661..a8180d0e93bc936251dfef5b50a3158fc78a2af6 100644 --- a/program_logic/sts.v +++ b/program_logic/sts.v @@ -102,14 +102,14 @@ Section sts. Proof. iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own. iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ". - iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (@own_valid with "#Hγ") as %Hvalid. + iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid. assert (s ∈ S) by eauto using sts_auth_frag_valid_inv. assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r. iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ". iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ". { iApply "HΨ"; by iSplit. } iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)". - iPvs (@own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth. + iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth. iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]". iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ". iNext; iExists s'; by iFrame. diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v index 36077d52ee263ed97797971fc0777c21f8f99349..97f37f828f7bf005268b7053cab3a29b267f0cb1 100644 --- a/tests/joining_existentials.v +++ b/tests/joining_existentials.v @@ -84,7 +84,7 @@ Proof. iSplitL "HP Hs Hγ"; [|iSplitL "Hr"]. - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"]. iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let. - iPvs (@own_update with "Hγ") as "Hx". + iPvs (own_update with "Hγ") as "Hx". { by apply (cmra_update_exclusive (Shot x)). } iApply signal_spec; iFrame "Hs"; iSplit; last done. iExists x; auto. diff --git a/tests/one_shot.v b/tests/one_shot.v index faaac93142802f4d9b518ff50fa4440cf39bbc83..66479873d92a06b8be0450c81d1574cb3d08357e 100644 --- a/tests/one_shot.v +++ b/tests/one_shot.v @@ -51,7 +51,7 @@ Proof. - iIntros (n) "!". wp_let. iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]". + wp_cas_suc. iSplitL; [|by iLeft]. - iPvs (@own_update with "Hγ") as "Hγ". + iPvs (own_update with "Hγ") as "Hγ". { by apply cmra_update_exclusive with (y:=Shot n). } iPvsIntro; iRight; iExists n; by iSplitL "Hl". + wp_cas_fail. rewrite /one_shot_inv; eauto 10. @@ -72,10 +72,10 @@ Proof. { by wp_match. } wp_match. wp_focus (! _)%E. iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]". - { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (@own_valid with "Hγ") as %?. } + { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. } wp_load; iPvsIntro. iCombine "Hγ" "Hγ'" as "Hγ". - iDestruct (@own_valid with "#Hγ") as %[=->]%dec_agree_op_inv. + iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv. iSplitL "Hl"; [iRight; by eauto|]. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto. Qed.