diff --git a/algebra/upred.v b/algebra/upred.v index fa14a763278d9ca144f1626f24ea8b4653bcff6e..f234b49b4377e4e5f35698ff194ebae6fa247a67 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -230,6 +230,10 @@ Arguments timelessP {_} _ {_} _ _ _ _. Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P. Arguments always_stable {_} _ {_} _ _ _ _. +Class AlwaysStableL {M} (Ps : list (uPred M)) := + always_stableL : Forall AlwaysStable Ps. +Arguments always_stableL {_} _ {_}. + Module uPred. Section uPred_logic. Context {M : cmraT}. Implicit Types φ : Prop. @@ -823,33 +827,33 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False. Proof. by intros; rewrite ownM_valid valid_elim. Qed. (* Big ops *) -Global Instance uPred_big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M). +Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. -Global Instance uPred_big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M). +Global Instance big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. -Global Instance uPred_big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M). +Global Instance big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M). Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. * by rewrite IH. * by rewrite !associative (commutative _ P). * etransitivity; eauto. Qed. -Global Instance uPred_big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M). +Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M). Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. * by rewrite IH. * by rewrite !associative (commutative _ P). * etransitivity; eauto. Qed. -Lemma uPred_big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I. +Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?associative ?IH. Qed. -Lemma uPred_big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I. +Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?associative ?IH. Qed. -Lemma uPred_big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps). +Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps). Proof. by induction Ps as [|P Ps IH]; simpl; auto. Qed. -Lemma uPred_big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P. +Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P. Proof. induction 1; simpl; auto. Qed. -Lemma uPred_big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P. +Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P. Proof. induction 1; simpl; auto. Qed. (* Timeless *) @@ -911,7 +915,7 @@ Proof. Qed. (* Always stable *) -Notation AS := AlwaysStable. +Local Notation AS := AlwaysStable. Global Instance const_always_stable φ : AS (■ φ : uPred M)%I. Proof. by rewrite /AlwaysStable always_const. Qed. Global Instance always_always_stable P : AS (□ P). @@ -940,6 +944,24 @@ Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) AS P → (∀ x, AS (Q x)) → AS (default P mx Q). Proof. destruct mx; apply _. Qed. +(* Always stable for lists *) +Local Notation ASL := AlwaysStableL. +Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps). +Proof. induction 1; apply _. Qed. +Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps). +Proof. induction 1; apply _. Qed. + +Global Instance nil_always_stable : ASL (@nil (uPred M)). +Proof. constructor. Qed. +Global Instance cons_always_stable P Ps : AS P → ASL Ps → ASL (P :: Ps). +Proof. by constructor. Qed. +Global Instance app_always_stable Ps Ps' : ASL Ps → ASL Ps' → ASL (Ps ++ Ps'). +Proof. apply Forall_app_2. Qed. +Global Instance zip_with_always_stable {A B} (f : A → B → uPred M) xs ys : + (∀ x y, AS (f x y)) → ASL (zip_with f xs ys). +Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. + +(* Derived lemmas for always stable *) Lemma always_always P `{!AlwaysStable P} : (□ P)%I ≡ P. Proof. apply (anti_symmetric (⊑)); auto using always_elim. Qed. Lemma always_intro' P Q `{!AlwaysStable P} : P ⊑ Q → P ⊑ □ Q.