More AlwaysStable stuff.

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.