diff --git a/algebra/upred.v b/algebra/upred.v index c576c0cc10588787a61b799df6df0b7e9476e111..d05beaf3f36ee4f3e728306316b48b6afcb5eefd 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -6,8 +6,8 @@ Local Hint Extern 10 (_ ≤ _) => omega. Record uPred (M : ucmraT) : Type := IProp { uPred_holds :> nat → M → Prop; uPred_ne n x1 x2 : uPred_holds n x1 → x1 ≡{n}≡ x2 → uPred_holds n x2; - uPred_weaken n1 n2 x1 x2 : - uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2 + uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼ x2 → uPred_holds n x2; + uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x }. Arguments uPred_holds {_} _ _ _ : simpl never. Add Printing Constructor uPred. @@ -28,10 +28,11 @@ Section cofe. Instance uPred_dist : Dist (uPred M) := uPred_dist'. Program Instance uPred_compl : Compl (uPred M) := λ c, {| uPred_holds n x := c n n x |}. - Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed. + Next Obligation. naive_solver eauto using uPred_ne. Qed. + Next Obligation. naive_solver eauto using uPred_mono. Qed. Next Obligation. - intros c n1 n2 x1 x2 ????; simpl in *. - apply (chain_cauchy c n2 n1); eauto using uPred_weaken. + intros c n1 n2 x ???; simpl in *. + apply (chain_cauchy c n2 n1); eauto using uPred_closed. Qed. Definition uPred_cofe_mixin : CofeMixin (uPred M). Proof. @@ -56,21 +57,14 @@ Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed. Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n). Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed. -Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x : - P1 ≡{n}≡ P2 → ✓{n} x → P1 n x → P2 n x. -Proof. intros HP ?; apply HP; auto. Qed. -Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 : - x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → P n1 x1 → P n2 x2. -Proof. eauto using uPred_weaken. Qed. - (** functor *) Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}. Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed. -Next Obligation. - naive_solver eauto using uPred_weaken, included_preserving, validN_preserving. -Qed. +Next Obligation. naive_solver eauto using uPred_mono, included_preserving. Qed. +Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed. + Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f). Proof. @@ -127,6 +121,8 @@ Inductive uPred_entails {M} (P Q : uPred M) : Prop := Hint Extern 0 (uPred_entails _ _) => reflexivity. Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M). +Hint Resolve uPred_ne uPred_mono uPred_closed : uPred_def. + (** logical connectives *) Program Definition uPred_const_def {M} (φ : Prop) : uPred M := {| uPred_holds n x := φ |}. @@ -140,14 +136,14 @@ Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True). Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∧ Q n x |}. -Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken. +Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed. Definition uPred_and {M} := proj1_sig uPred_and_aux M. Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux. Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∨ Q n x |}. -Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken. +Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed. Definition uPred_or {M} := proj1_sig uPred_or_aux M. Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux. @@ -160,9 +156,10 @@ Next Obligation. destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto. assert (x2' ≡{n2}≡ x2) as Hx2' by (by apply dist_le with n1). assert (✓{n2} x2') by (by rewrite Hx2'); rewrite -Hx2'. - eauto using uPred_weaken, uPred_ne. + eauto using uPred_ne. Qed. Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed. +Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed. Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed. Definition uPred_impl {M} := proj1_sig uPred_impl_aux M. Definition uPred_impl_eq : @@ -170,7 +167,7 @@ Definition uPred_impl_eq : Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M := {| uPred_holds n x := ∀ a, Ψ a n x |}. -Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken. +Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed. Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A. Definition uPred_forall_eq : @@ -178,7 +175,7 @@ Definition uPred_forall_eq : Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M := {| uPred_holds n x := ∃ a, Ψ a n x |}. -Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken. +Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed. Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A. Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux. @@ -196,13 +193,14 @@ Next Obligation. by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy. Qed. Next Obligation. - intros M P Q n1 n2 x y (x1&x2&Hx&?&?) Hxy ??. - assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?). - { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using cmra_included_l. - apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. } - clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |]. - - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l. - - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r. + intros M P Q n x y (x1&x2&Hx&?&?) [z Hy]. + exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_included_l. + by rewrite Hy Hx assoc. +Qed. +Next Obligation. + intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?. + exists x1, x2; cofe_subst; split_and!; + eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r. Qed. Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed. Definition uPred_sep {M} := proj1_sig uPred_sep_aux M. @@ -217,10 +215,11 @@ Next Obligation. by rewrite (dist_le _ _ _ _ Hx). Qed. Next Obligation. - intros M P Q n1 n2 x1 x2 HPQ ??? n3 x3 ???; simpl in *. - apply uPred_weaken with n3 (x1 ⋅ x3); + intros M P Q n x1 x2 HPQ ? n3 x3 ???; simpl in *. + apply uPred_mono with (x1 ⋅ x3); eauto using cmra_validN_included, cmra_preserving_r. Qed. +Next Obligation. naive_solver. Qed. Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed. Definition uPred_wand {M} := proj1_sig uPred_wand_aux M. Definition uPred_wand_eq : @@ -229,10 +228,8 @@ Definition uPred_wand_eq : Program Definition uPred_always_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := P n (core x) |}. Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed. -Next Obligation. - intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (core x1); - eauto using cmra_core_preserving, cmra_core_validN. -Qed. +Next Obligation. naive_solver eauto using uPred_mono, cmra_core_preserving. Qed. +Next Obligation. naive_solver eauto using uPred_closed, cmra_core_validN. Qed. Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed. Definition uPred_always {M} := proj1_sig uPred_always_aux M. Definition uPred_always_eq : @@ -241,8 +238,9 @@ Definition uPred_always_eq : Program Definition uPred_later_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}. Next Obligation. intros M P [|n] ??; eauto using uPred_ne,(dist_le (A:=M)). Qed. +Next Obligation. intros M P [|n] x1 x2; eauto using uPred_mono. Qed. Next Obligation. - intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia. + intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia. Qed. Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed. Definition uPred_later {M} := proj1_sig uPred_later_aux M. @@ -253,9 +251,10 @@ Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M := {| uPred_holds n x := a ≼{n} x |}. Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed. Next Obligation. - intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??. - exists (a' ⋅ x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx. + intros M a n x1 x [a' Hx1] [x2 ->]. + exists (a' ⋅ x2). by rewrite (assoc op) Hx1. Qed. +Next Obligation. naive_solver eauto using cmra_includedN_le. Qed. Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed. Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M. Definition uPred_ownM_eq : @@ -321,7 +320,7 @@ Definition unseal := (uPred_const_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq, uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq, uPred_later_eq, uPred_ownM_eq, uPred_valid_eq). -Ltac unseal := rewrite !unseal. +Ltac unseal := rewrite !unseal /=. Section uPred_logic. Context {M : ucmraT}. @@ -490,7 +489,7 @@ Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed. Lemma impl_intro_r P Q R : (P ∧ Q) ⊢ R → P ⊢ (Q → R). Proof. unseal; intros HQ; split=> n x ?? n' x' ????. - apply HQ; naive_solver eauto using uPred_weaken. + apply HQ; naive_solver eauto using uPred_mono, uPred_closed. Qed. Lemma impl_elim P Q R : P ⊢ (Q → R) → P ⊢ Q → P ⊢ R. Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed. @@ -713,7 +712,7 @@ Qed. Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M). Proof. intros P; unseal; split=> n x Hvalid; split. - - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r. + - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_included_r. - by intros ?; exists (core x), x; rewrite cmra_core_l. Qed. Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M). @@ -735,7 +734,7 @@ Lemma wand_intro_r P Q R : (P ★ Q) ⊢ R → P ⊢ (Q -★ R). Proof. unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto. exists x, x'; split_and?; auto. - eapply uPred_weaken with n x; eauto using cmra_validN_op_l. + eapply uPred_closed with n; eauto using cmra_validN_op_l. Qed. Lemma wand_elim_l' P Q R : P ⊢ (Q -★ R) → (P ★ Q) ⊢ R. Proof. @@ -865,21 +864,18 @@ Lemma sep_forall_r {A} (Φ : A → uPred M) Q : ((∀ a, Φ a) ★ Q) ⊢ (∀ a Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. (* Always *) -Lemma always_const φ : (□ ■ φ) ⊣⊢ (■ φ). +Lemma always_const φ : □ ■ φ ⊣⊢ ■ φ. Proof. by unseal. Qed. Lemma always_elim P : □ P ⊢ P. -Proof. - unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_core. -Qed. +Proof. unseal; split=> n x ? /=; eauto using uPred_mono, cmra_included_core. Qed. Lemma always_intro' P Q : □ P ⊢ Q → □ P ⊢ □ Q. Proof. - unseal=> HPQ. - split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN. + unseal=> HPQ; split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN. by rewrite cmra_core_idemp. Qed. -Lemma always_and P Q : (□ (P ∧ Q)) ⊣⊢ (□ P ∧ □ Q). +Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ (□ P ∧ □ Q). Proof. by unseal. Qed. -Lemma always_or P Q : (□ (P ∨ Q)) ⊣⊢ (□ P ∨ □ Q). +Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ (□ P ∨ □ Q). Proof. by unseal. Qed. Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a). Proof. by unseal. Qed. @@ -895,7 +891,7 @@ Proof. unseal; split=> n x ? [??]; exists (core x), x; simpl in *. by rewrite cmra_core_l cmra_core_idemp. Qed. -Lemma always_later P : (□ ▷ P) ⊣⊢ (▷ □ P). +Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P. Proof. by unseal. Qed. (* Always derived *) @@ -912,26 +908,26 @@ Proof. apply impl_intro_l; rewrite -always_and. apply always_mono, impl_elim with P; auto. Qed. -Lemma always_eq {A:cofeT} (a b : A) : (□ (a ≡ b)) ⊣⊢ (a ≡ b). +Lemma always_eq {A:cofeT} (a b : A) : □ (a ≡ b) ⊣⊢ (a ≡ b). Proof. apply (anti_symm (⊢)); auto using always_elim. apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto. { intros n; solve_proper. } rewrite -(eq_refl a) always_const; auto. Qed. -Lemma always_and_sep P Q : (□ (P ∧ Q)) ⊣⊢ (□ (P ★ Q)). +Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ★ Q). Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed. Lemma always_and_sep_l' P Q : (□ P ∧ Q) ⊣⊢ (□ P ★ Q). Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed. Lemma always_and_sep_r' P Q : (P ∧ □ Q) ⊣⊢ (P ★ □ Q). Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed. -Lemma always_sep P Q : (□ (P ★ Q)) ⊣⊢ (□ P ★ □ Q). +Lemma always_sep P Q : □ (P ★ Q) ⊣⊢ (□ P ★ □ Q). Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed. Lemma always_wand P Q : □ (P -★ Q) ⊢ (□ P -★ □ Q). Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed. -Lemma always_sep_dup' P : (□ P) ⊣⊢ (□ P ★ □ P). +Lemma always_sep_dup' P : □ P ⊣⊢ (□ P ★ □ P). Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed. -Lemma always_wand_impl P Q : (□ (P -★ Q)) ⊣⊢ (□ (P → Q)). +Lemma always_wand_impl P Q : □ (P -★ Q) ⊣⊢ □ (P → Q). Proof. apply (anti_symm (⊢)); [|by rewrite -impl_wand]. apply always_intro', impl_intro_r. @@ -972,16 +968,16 @@ Qed. Lemma later_intro P : P ⊢ ▷ P. Proof. unseal; split=> -[|n] x ??; simpl in *; [done|]. - apply uPred_weaken with (S n) x; eauto using cmra_validN_S. + apply uPred_closed with (S n); eauto using cmra_validN_S. Qed. Lemma löb P : (▷ P → P) ⊢ P. Proof. unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|]. - apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S. + apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S. Qed. -Lemma later_and P Q : (▷ (P ∧ Q)) ⊣⊢ (▷ P ∧ ▷ Q). +Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ (▷ P ∧ ▷ Q). Proof. unseal; split=> -[|n] x; by split. Qed. -Lemma later_or P Q : (▷ (P ∨ Q)) ⊣⊢ (▷ P ∨ ▷ Q). +Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ (▷ P ∨ ▷ Q). Proof. unseal; split=> -[|n] x; simpl; tauto. Qed. Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a). Proof. unseal; by split=> -[|n] x. Qed. @@ -990,7 +986,7 @@ Proof. unseal; by split=> -[|[|n]] x. Qed. Lemma later_exist' `{Inhabited A} (Φ : A → uPred M) : (▷ ∃ a, Φ a)%I ⊢ (∃ a, ▷ Φ a)%I. Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed. -Lemma later_sep P Q : (▷ (P ★ Q)) ⊣⊢ (▷ P ★ ▷ Q). +Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ (▷ P ★ ▷ Q). Proof. unseal; split=> n x ?; split. - destruct n as [|n]; simpl. @@ -1034,14 +1030,11 @@ Proof. by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1) -(assoc op _ a2) (comm op z1) -Hy1 -Hy2. Qed. -Lemma always_ownM_core (a : M) : (□ uPred_ownM (core a)) ⊣⊢ uPred_ownM (core a). +Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a. Proof. - split=> n x; split; [by apply always_elim|unseal; intros [a' Hx]]; simpl. - rewrite -(cmra_core_idemp a) Hx. - apply cmra_core_preservingN, cmra_includedN_l. + split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl. + rewrite -(persistent a). by apply cmra_core_preservingN. Qed. -Lemma always_ownM (a : M) : Persistent a → (□ uPred_ownM a) ⊣⊢ uPred_ownM a. -Proof. intros. by rewrite -(persistent a) always_ownM_core. Qed. Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a. Proof. unseal; split=> n x ??. by exists x; simpl. Qed. Lemma ownM_empty : True ⊢ uPred_ownM ∅. @@ -1081,11 +1074,10 @@ Lemma later_equivI {A : cofeT} (x y : later A) : Proof. by unseal. Qed. (* Discrete *) -Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : - (✓ a) ⊣⊢ (■ ✓ a). +Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : (✓ a) ⊣⊢ ■ ✓ a. Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed. Lemma timeless_eq {A : cofeT} (a b : A) : - Timeless a → (a ≡ b) ⊣⊢ (■ (a ≡ b)). + Timeless a → (a ≡ b) ⊣⊢ ■ (a ≡ b). Proof. unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n). Qed. @@ -1110,7 +1102,7 @@ Proof. move: HP; rewrite /TimelessP; unseal=> /uPred_in_entails /(_ (S n) x). by destruct 1; auto using cmra_validN_S. - move=> HP; rewrite /TimelessP; unseal; split=> -[|n] x /=; auto; left. - apply HP, uPred_weaken with n x; eauto using cmra_validN_le. + apply HP, uPred_closed with n; eauto using cmra_validN_le. Qed. Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I. @@ -1129,7 +1121,7 @@ Qed. Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q). Proof. rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ????; auto. - apply HP, HPQ, uPred_weaken with (S n') x'; eauto using cmra_validN_le. + apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le. Qed. Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q). Proof. @@ -1141,7 +1133,7 @@ Qed. Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q). Proof. rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ???; auto. - apply HP, HPQ, uPred_weaken with (S n') x'; + apply HP, HPQ, uPred_closed with (S n'); eauto 3 using cmra_validN_le, cmra_validN_op_r. Qed. Global Instance forall_timeless {A} (Ψ : A → uPred M) : @@ -1206,7 +1198,7 @@ Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A Proof. destruct mx; apply _. Qed. (* Derived lemmas for persistence *) -Lemma always_always P `{!PersistentP P} : (□ P) ⊣⊢ P. +Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P. Proof. apply (anti_symm (⊢)); auto using always_elim. Qed. Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P. Proof. destruct p; simpl; auto using always_always. Qed. diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v index 9e364ca60c8d843acfb78b7f574c4258ef97fb0c..693dd662b3d2a75bd4d6c2031b3198d5bb68cf73 100644 --- a/program_logic/adequacy.v +++ b/program_logic/adequacy.v @@ -18,7 +18,7 @@ Implicit Types m : iGst Λ Σ. Notation wptp n := (Forall3 (λ e Φ r, uPred_holds (wp ⊤ e Φ) n r)). Lemma wptp_le Φs es rs n n' : ✓{n'} (big_op rs) → wptp n es Φs rs → n' ≤ n → wptp n' es Φs rs. -Proof. induction 2; constructor; eauto using uPred_weaken. Qed. +Proof. induction 2; constructor; eauto using uPred_closed. Qed. Lemma nsteps_wptp Φs k n tσ1 tσ2 rs1 : nsteps step k tσ1 tσ2 → 1 < n → wptp (k + n) (tσ1.1) Φs rs1 → @@ -51,7 +51,8 @@ Proof. { rewrite /option_list right_id_L. apply Forall3_app, Forall3_cons; eauto using wptp_le. rewrite wp_eq. - apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. } + apply uPred_closed with (k + n); + first apply uPred_mono with r2; eauto using cmra_included_l. } by rewrite -Permutation_middle /= big_op_app. Qed. Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 : diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v index 96dfa57f560d05f4aaa62ebd4fdb683f781dba27..a282bdcb2ef013377ba9743941522a208f267841 100644 --- a/program_logic/pviewshifts.v +++ b/program_logic/pviewshifts.v @@ -19,11 +19,12 @@ Next Obligation. apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia. Qed. Next Obligation. - intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst. - destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto. + intros Λ Σ E1 E2 P n r1 r2 HP [r3 ?] rf k Ef σ ?? Hws; setoid_subst. + destruct (HP (r3 ⋅ rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto. exists (r' ⋅ r3); rewrite -assoc; split; last done. - apply uPred_weaken with k r'; eauto using cmra_included_l. + apply uPred_mono with r'; eauto using cmra_included_l. Qed. +Next Obligation. naive_solver. Qed. Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed. Definition pvs := proj1_sig pvs_aux. @@ -62,7 +63,7 @@ Proof. apply ne_proper, _. Qed. Lemma pvs_intro E P : P ⊢ |={E}=> P. Proof. rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done. - apply uPred_weaken with n r; eauto. + apply uPred_closed with n; eauto. Qed. Lemma pvs_mono E1 E2 P Q : P ⊢ Q → (|={E1,E2}=> P) ⊢ (|={E1,E2}=> Q). Proof. @@ -75,7 +76,7 @@ Proof. rewrite pvs_eq uPred.timelessP_spec=> HP. uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia. exists r; split; last done. - apply HP, uPred_weaken with n r; eauto using cmra_validN_le. + apply HP, uPred_closed with n; eauto using cmra_validN_le. Qed. Lemma pvs_trans E1 E2 E3 P : E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊢ (|={E1,E3}=> P). @@ -96,7 +97,7 @@ Proof. destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto. { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. } exists (r' ⋅ r2); split; last by rewrite -assoc. - exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto. + exists r', r2; split_and?; auto. apply uPred_closed with n; auto. Qed. Lemma pvs_openI i P : ownI i P ⊢ (|={{[i]},∅}=> ▷ P). Proof. @@ -105,17 +106,17 @@ Proof. destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto. { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. } exists (rP ⋅ r); split; last by rewrite (left_id_L _ _) -assoc. - eapply uPred_weaken with (S k) rP; eauto using cmra_included_l. + eapply uPred_mono with rP; eauto using cmra_included_l. Qed. Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊢ (|={∅,{[i]}}=> True). Proof. rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia. exists ∅; split; [done|]. rewrite left_id; apply wsat_close with P r. - - apply ownI_spec, uPred_weaken with (S n) r; auto. + - apply ownI_spec, uPred_closed with (S n); auto. - set_solver +HE. - by rewrite -(left_id_L ∅ (∪) Ef). - - apply uPred_weaken with n r; auto. + - apply uPred_closed with n; auto. Qed. Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) : m ~~>: P → ownG m ⊢ (|={E}=> ∃ m', ■ P m' ∧ ownG m'). @@ -131,7 +132,7 @@ Proof. rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal. split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia. destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto. - { apply uPred_weaken with n r; eauto. } + { apply uPred_closed with n; eauto. } exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅). split; [|done]. by exists i; split; rewrite /uPred_holds /=. Qed. diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v index 6d576bd4b57d2399ea17dd0cc8a31a6be5fae1c2..06e0ed3a81cd0cde9c14d0b22d2822d225fcf4b4 100644 --- a/program_logic/weakestpre.v +++ b/program_logic/weakestpre.v @@ -38,17 +38,19 @@ Next Obligation. intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver. Qed. Next Obligation. - intros Λ Σ E e Φ n1 n2 r1 r2; revert Φ E e n2 r1 r2. - induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e n2 r1 r1'. - destruct 1 as [|n1 r1 e1 ? Hgo]. - - constructor; eauto using uPred_weaken. - - intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???]. + intros Λ Σ E e Φ n r1 r2; revert Φ E e r1 r2. + induction n as [n IH] using lt_wf_ind; intros Φ E e r1 r1'. + destruct 1 as [|n r1 e1 ? Hgo]. + - constructor; eauto using uPred_mono. + - intros [rf' Hr]; constructor; [done|intros rf k Ef σ1 ???]. destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep]; rewrite ?assoc -?Hr; auto; constructor; [done|]. intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. exists r2, (r2' ⋅ rf'); split_and?; eauto 10 using (IH k), cmra_included_l. by rewrite -!assoc (assoc _ r2). Qed. +Next Obligation. destruct 1; constructor; eauto using uPred_closed. Qed. + (* Perform sealing. *) Definition wp_aux : { x | x = @wp_def }. by eexists. Qed. Definition wp := proj1_sig wp_aux. @@ -194,7 +196,7 @@ Proof. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. exists (r2 ⋅ rR), r2'; split_and?; auto. - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR). - - apply IH; eauto using uPred_weaken. + - apply IH; eauto using uPred_closed. Qed. Lemma wp_frame_step_r E E1 E2 e Φ R : to_val e = None → E ⊥ E1 → E2 ⊆ E1 → diff --git a/program_logic/weakestpre_fix.v b/program_logic/weakestpre_fix.v index 62cb86f9b64c0d021bf81e121422e2df9a2d4afb..a65ead7f803bf1817ec37dbd3c86707bb23a8e58 100644 --- a/program_logic/weakestpre_fix.v +++ b/program_logic/weakestpre_fix.v @@ -36,18 +36,19 @@ Next Obligation. by rewrite (dist_le _ _ _ _ Hr1); last omega. Qed. Next Obligation. - intros wp E e1 Φ n1 n2 r1 ? Hwp [r2 ?] ?? rf k Ef σ1 ???; setoid_subst. + intros wp E e1 Φ n r1 ? Hwp [r2 ?] rf k Ef σ1 ???; setoid_subst. destruct (Hwp (r2 ⋅ rf) k Ef σ1) as [Hval Hstep]; rewrite ?assoc; auto. split. - intros v Hv. destruct (Hval v Hv) as [r3 [??]]. - exists (r3 ⋅ r2). rewrite -assoc. eauto using uPred_weaken, cmra_included_l. + exists (r3 ⋅ r2). rewrite -assoc. eauto using uPred_mono, cmra_included_l. - intros ??. destruct Hstep as [Hred Hpstep]; auto. split; [done|]=> e2 σ2 ef ?. edestruct Hpstep as (r3&r3'&?&?&?); eauto. exists r3, (r3' ⋅ r2); split_and?; auto. + by rewrite assoc -assoc. - + destruct ef; simpl in *; eauto using uPred_weaken, cmra_included_l. + + destruct ef; simpl in *; eauto using uPred_mono, cmra_included_l. Qed. +Next Obligation. repeat intro; eauto. Qed. Lemma wp_pre_contractive' n E e Φ1 Φ2 r (wp1 wp2 : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp) : diff --git a/program_logic/wsat.v b/program_logic/wsat.v index 77b0de31a55f21699ce1c6ac778c672831debb78..84fb2cde34707659ad42dc27af629784e12090b3 100644 --- a/program_logic/wsat.v +++ b/program_logic/wsat.v @@ -63,7 +63,7 @@ Proof. destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto. { by rewrite HP' -HPiso. } assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto). - exists r'; split; [done|apply HPP', uPred_weaken with n r'; auto]. + exists r'; split; [done|]. apply HPP', uPred_closed with n; auto. Qed. Lemma wsat_valid n E σ r : n ≠ 0 → wsat n E σ r → ✓{n} r. Proof.