Iterated later modality.

base_logic/big_op.v

@@ -73,6 +73,8 @@ Section cmra.
   Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
   Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
   Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
+  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
+  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
   Global Instance uPred_except_0_homomorphism :
     CMRAHomomorphism uPred_except_0.
   Proof. split. apply _. apply except_0_sep. Qed.
@@ -248,6 +250,10 @@ Section list.
     ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
+  Lemma big_sepL_laterN Φ n l :
+    ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+
   Lemma big_sepL_always Φ l :
     (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
   Proof. apply (big_opL_commute _). Qed.
@@ -380,6 +386,10 @@ Section gmap.
     ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
+  Lemma big_sepM_laterN Φ n m :
+    ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
+  Proof. apply (big_opM_commute _). Qed.
+
   Lemma big_sepM_always Φ m :
     (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
   Proof. apply (big_opM_commute _). Qed.
@@ -513,6 +523,10 @@ Section gset.
   Lemma big_sepS_later Φ X : ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
+  Lemma big_sepS_laterN Φ n X :
+    ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
+  Proof. apply (big_opS_commute _). Qed.
+
   Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
@@ -611,6 +625,10 @@ Section gmultiset.
   Lemma big_sepMS_later Φ X : ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
+  Lemma big_sepMS_laterN Φ n X :
+    ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
+  Proof. apply (big_opMS_commute _). Qed.
+
   Lemma big_sepMS_always Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 

base_logic/derived.v

@@ -5,12 +5,22 @@ Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%
 Instance: Params (@uPred_iff) 1.
 Infix "↔" := uPred_iff : uPred_scope.
 
+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, P at level 20,
+   format "▷^ n  P") : uPred_scope.
+Notation "▷? p P" := (uPred_laterN (Nat.b2n p) P)
+  (at level 20, p at level 9, P at level 20,
+   format "▷? p  P") : uPred_scope.
+
 Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
   (if p then □ P else P)%I.
 Instance: Params (@uPred_always_if) 2.
 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").
+  (at level 20, p at level 9, P at level 20, format "□? p  P").
 
 Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P.
 Notation "◇ P" := (uPred_except_0 P)
@@ -510,6 +520,10 @@ 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.
+
+
 (* Later derived *)
 Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
 Proof. by intros ->. Qed.
@@ -552,6 +566,58 @@ Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
 
+(* Iterated later modality *)
+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 laterN_0 P : ▷^0 P ⊣⊢ P.
+Proof. done. Qed.
+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.
+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_intro n P : P ⊢ ▷^n P.
+Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
+
+Lemma laterN_True n : ▷^n True ⊣⊢ True.
+Proof. apply (anti_symm (⊢)); auto using laterN_intro. 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 `{Inhabited A} n (Φ : A → uPred M) :
+  (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_exist; auto. 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_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_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. 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.
+
 (* Conditional always *)
 Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
 Proof. solve_proper. Qed.
@@ -757,6 +823,8 @@ Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
 Proof. by intros; rewrite /PersistentP always_cmra_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) :

base_logic/double_negation.v

@@ -3,15 +3,6 @@ Import upred.
 
 (* In this file we show that the bupd can be thought of a kind of
    step-indexed double-negation when our meta-logic is classical *)
-
-(* To define this, we need a way to talk about iterated later modalities: *)
-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.
-
 Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
   ∀ n, (P -∗ ▷^n False) -∗ ▷^n False.