diff --git a/algebra/upred.v b/algebra/upred.v index d05beaf3f36ee4f3e728306316b48b6afcb5eefd..3a46637b316c00c6aa2bc3fddab074324206278c 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -5,8 +5,7 @@ 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_mono n x1 x2 : uPred_holds n x1 → x1 ≼ x2 → uPred_holds n x2; + uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} 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. @@ -28,7 +27,6 @@ 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. naive_solver eauto using uPred_ne. Qed. Next Obligation. naive_solver eauto using uPred_mono. Qed. Next Obligation. intros c n1 n2 x ???; simpl in *. @@ -53,7 +51,9 @@ End cofe. Arguments uPredC : clear implicits. Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n). -Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed. +Proof. + intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx. +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. @@ -61,8 +61,7 @@ Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed. 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_mono, included_preserving. Qed. +Next Obligation. naive_solver eauto using uPred_mono, includedN_preserving. Qed. Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed. Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1) @@ -121,7 +120,7 @@ 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. +Hint Resolve uPred_mono uPred_closed : uPred_def. (** logical connectives *) Program Definition uPred_const_def {M} (φ : Prop) : uPred M := @@ -152,13 +151,10 @@ Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ n' x', x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}. Next Obligation. - intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????. - 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_ne. + intros M P Q n1 x1 x1' HPQ [x2 Hx1'] n2 x3 [x4 Hx3] ?; simpl in *. + rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??. + eapply HPQ; auto. exists (x2 ⋅ x4); by rewrite assoc. 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. @@ -189,12 +185,9 @@ Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux. Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}. -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 n x y (x1&x2&Hx&?&?) [z Hy]. - exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_included_l. + exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_includedN_l. by rewrite Hy Hx assoc. Qed. Next Obligation. @@ -210,14 +203,9 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ n' x', n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}. Next Obligation. - intros M P Q n1 x1 x2 HPQ Hx n2 x3 ???; simpl in *. - rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto. - by rewrite (dist_le _ _ _ _ Hx). -Qed. -Next Obligation. - intros M P Q n x1 x2 HPQ ? n3 x3 ???; simpl in *. + intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *. apply uPred_mono with (x1 ⋅ x3); - eauto using cmra_validN_included, cmra_preserving_r. + eauto using cmra_validN_includedN, cmra_preservingN_r, cmra_includedN_le. Qed. Next Obligation. naive_solver. Qed. Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed. @@ -227,8 +215,7 @@ 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. naive_solver eauto using uPred_mono, cmra_core_preserving. Qed. +Next Obligation. naive_solver eauto using uPred_mono, cmra_core_preservingN. 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. @@ -237,8 +224,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 [|n] x1 x2; eauto using uPred_mono, cmra_includedN_S. +Qed. Next Obligation. intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia. Qed. @@ -249,7 +237,6 @@ Definition uPred_later_eq : 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 n x1 x [a' Hx1] [x2 ->]. exists (a' ⋅ x2). by rewrite (assoc op) Hx1. @@ -488,8 +475,8 @@ Lemma or_elim P Q R : P ⊢ R → Q ⊢ R → (P ∨ Q) ⊢ R. 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_mono, uPred_closed. + unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ; + naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN. 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. @@ -712,7 +699,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_mono, cmra_included_r. + - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_includedN_r. - by intros ?; exists (core x), x; rewrite cmra_core_l. Qed. Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M). @@ -867,7 +854,10 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. Lemma always_const φ : □ ■ φ ⊣⊢ ■ φ. Proof. by unseal. Qed. Lemma always_elim P : □ P ⊢ P. -Proof. unseal; split=> n x ? /=; eauto using uPred_mono, cmra_included_core. Qed. +Proof. + unseal; split=> n x ? /=. + eauto using uPred_mono, cmra_included_core, cmra_included_includedN. +Qed. Lemma always_intro' P Q : □ P ⊢ Q → □ P ⊢ □ Q. Proof. unseal=> HPQ; split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN. diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v index 693dd662b3d2a75bd4d6c2031b3198d5bb68cf73..dbc1f76f3795904f1b8420844ccf14a8ef0de06c 100644 --- a/program_logic/adequacy.v +++ b/program_logic/adequacy.v @@ -52,7 +52,7 @@ Proof. apply Forall3_app, Forall3_cons; eauto using wptp_le. rewrite wp_eq. apply uPred_closed with (k + n); - first apply uPred_mono with r2; eauto using cmra_included_l. } + first apply uPred_mono with r2; eauto using cmra_includedN_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 a282bdcb2ef013377ba9743941522a208f267841..769509e239546350ca51eb8bd5504ef25428111b 100644 --- a/program_logic/pviewshifts.v +++ b/program_logic/pviewshifts.v @@ -15,14 +15,11 @@ Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) → ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}. Next Obligation. - intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *. - apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia. -Qed. -Next Obligation. - intros Λ Σ E1 E2 P n r1 r2 HP [r3 ?] rf k Ef σ ?? Hws; setoid_subst. + intros Λ Σ E1 E2 P n r1 r2 HP [r3 Hr2] rf k Ef σ ??. + rewrite (dist_le _ _ _ _ Hr2); last lia. intros Hws. destruct (HP (r3 ⋅ rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto. exists (r' ⋅ r3); rewrite -assoc; split; last done. - apply uPred_mono with r'; eauto using cmra_included_l. + apply uPred_mono with r'; eauto using cmra_includedN_l. Qed. Next Obligation. naive_solver. Qed. @@ -106,7 +103,7 @@ 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_mono with rP; eauto using cmra_included_l. + eapply uPred_mono with rP; eauto using cmra_includedN_l. Qed. Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊢ (|={∅,{[i]}}=> True). Proof. diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v index 06e0ed3a81cd0cde9c14d0b22d2822d225fcf4b4..74bea5bc88709fd1e10831d43e6ef41c81d28404 100644 --- a/program_logic/weakestpre.v +++ b/program_logic/weakestpre.v @@ -32,11 +32,6 @@ CoInductive wp_pre {Λ Σ} (E : coPset) wp_pre E Φ e1 n r1. Program Definition wp_def {Λ Σ} (E : coPset) (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}. -Next Obligation. - intros Λ Σ E e Φ n r1 r2 Hwp Hr. - destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto. - intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver. -Qed. Next Obligation. 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'. @@ -44,9 +39,9 @@ Next Obligation. - 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|]. + rewrite ?assoc -?(dist_le _ _ _ _ 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. + exists r2, (r2' ⋅ rf'); split_and?; eauto 10 using (IH k), cmra_includedN_l. by rewrite -!assoc (assoc _ r2). Qed. Next Obligation. destruct 1; constructor; eauto using uPred_closed. Qed. diff --git a/program_logic/weakestpre_fix.v b/program_logic/weakestpre_fix.v index a65ead7f803bf1817ec37dbd3c86707bb23a8e58..2e0b3edca5f8d5319ae6fab0c3e7d4c8f8d47dc9 100644 --- a/program_logic/weakestpre_fix.v +++ b/program_logic/weakestpre_fix.v @@ -31,22 +31,18 @@ Program Definition wp_pre wp E e2 Φ k r2 ∧ default True ef (λ ef, wp ⊤ ef (cconst True%I) k r2'))) |}. Next Obligation. - intros wp E e1 Φ n r1 r1' Hwp Hr1 rf k Ef σ1 ???; simpl in *. - destruct (Hwp rf k Ef σ1); auto. - by rewrite (dist_le _ _ _ _ Hr1); last omega. -Qed. -Next Obligation. - 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. + intros wp E e1 Φ n r1 r2 Hwp [r3 Hr2] rf k Ef σ1 ??. + rewrite (dist_le _ _ _ _ Hr2); last lia. intros Hws. + destruct (Hwp (r3 ⋅ 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_mono, cmra_included_l. + - intros v Hv. destruct (Hval v Hv) as [r4 [??]]. + exists (r4 ⋅ r3). rewrite -assoc. eauto using uPred_mono, cmra_includedN_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. + edestruct Hpstep as (r4&r4'&?&?&?); eauto. + exists r4, (r4' ⋅ r3); split_and?; auto. + by rewrite assoc -assoc. - + destruct ef; simpl in *; eauto using uPred_mono, cmra_included_l. + + destruct ef; simpl in *; eauto using uPred_mono, cmra_includedN_l. Qed. Next Obligation. repeat intro; eauto. Qed.